发现大模型在代数证明机制选择上存在认知瓶颈，暴露线索后准确率显著提升。
Mechanism-level routing failure in LLMs over Lean-verified algebraic structures
- 用形式化验证的代数结构测试模型机制选择能力，通过引入证明线索观察性能变化。
- 无提示下GPT-OSS-120B准确率80.3%，暴露线索后升至90.9%，提升10.6个百分点。
- 揭示模型真值判断与证明机制分类是独立能力，适合形式化推理研究者参考。
我们对大型语言模型（LLMs）在形式化验证代数语料上的结构化路由失败进行了实证研究。任务要求从固定模板集中为来自Lean 4中FiberRing形式化的紧凑数学对象选择正确的证明机制标签，每个对象关联一个经过验证的Lean实体并分配对应证书族标签。核心发现是机制级路由上限：在盲测条件下，gpt-oss-120b在22个FiberRing条目上（n=66；temperature=0，seed=0）达到80.3%模板准确率，而Llama 3.3 70B为68.2%。暴露带有机制信息的Lean证明结论/见证线索（条件A2）后，准确率分别提升至90.9%和81.8%，提升幅度分别为+10.6和+13.6个百分点，称为线索诱导的路由增益。主要失败模式为CRT到环等价的误路由：gpt-oss-120b在盲测中将12个CRT条目中的7个（58.3%）错误路由，而在A2条件下为0。在Llama中出现跨模型分离现象：证明结论准确率在两种条件下均为95.5%，但模板准确率提升13.6个百分点，证实真值推断与证明机制分类是可分离的能力。跨语料扩展（集合B；6个POM/CollisionKernel条目，共72次评估）提供小规模模块间验证：CRT粒度压缩现象再现且标签不同，同时出现反向跨模型分离。这些发现将路由器假说（Cazares 2026）拓展至形式化代数结构。完整流程、清单与结果见https://github.com/bytepro-ai/fiber-routing-eval。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。