基于精益验证代数结构的大语言模型中的机制级路由失败
Mechanism-level routing failure in LLMs over Lean-verified algebraic structures
AI总结：
研究大语言模型在形式验证代数语料库中的结构路由失败，通过在固定模板集选正确证明机制标签任务，发现机制级路由上限，揭示主导失败类型及模型差异，扩展了路由器假设。
摘要：
我们展示了一项关于大语言模型（LLMs）在形式验证代数语料库上结构路由失败的实证研究。任务要求从固定封闭模板集中为来自Lean 4中FiberRing形式化的紧凑数学对象选择正确的证明机制标签……这些发现将路由器假设（Cazares 2026）扩展到形式代数结构。完整管道、清单和结果见此https链接。
英文摘要：
We present an empirical study of structural routing failure in large language models (LLMs) over a formally verified algebraic corpus. The task requires selecting the correct proof-mechanism label from a fixed closed template set for compact mathematical objects drawn from the FiberRing formalization in Lean 4, where each item is anchored to a Lean-verified artifact and assigned a label from the corresponding certificate family. Our central finding is a mechanism-level routing ceiling: under blind conditions, gpt-oss-120b achieves 80.3% template accuracy on 22 FiberRing items (n=66; temperature=0, seed=0), while Llama 3.3 70B reaches 68.2%. Exposing a mechanism-bearing Lean verdict/witness cue (Condition A2) raises accuracy to 90.9% and 81.8% -- gaps of +10.6 and +13.6 pp termed cue-induced routing uplift. The dominant failure is a CRT-to-ring-equivalence misroute: gpt-oss-120b misroutes 7 of 12 CRT items (58.3%) blind, zero under A2. A cross-model dissociation in Llama is notable: verdict accuracy is identical in both conditions (95.5%), while template accuracy improves 13.6 pp -- confirming that truth inference and proof-mechanism classification are separable capacities. A cross-corpus extension (Set B; 6 POM/CollisionKernel items, 72 evaluations) provides a small cross-module check: CRT-granularity compression reappears with different labels, and an inverse cross-model dissociation emerges. These findings extend the router hypothesis (Cazares 2026) to formal algebraic structures. The full pipeline, manifest, and results are at https://github.com/bytepro-ai/fiber-routing-eval.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
