{"ID":5937820,"CreatedAt":"2026-07-07T03:14:33.014478982Z","UpdatedAt":"2026-07-08T22:40:00.334127079Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.04534","arxiv_id":"2607.04534","title":"Mechanism-level routing failure in LLMs over Lean-verified algebraic structures","abstract":"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.","short_abstract":"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 e...","url_abs":"https://arxiv.org/abs/2607.04534","url_pdf":"https://arxiv.org/pdf/2607.04534v1","authors":"[\"Manuel Israel Cázares\",\"Wenlin Zhang\",\"Haobo Ma\"]","published":"2026-07-05T22:45:49Z","proceeding":"cs.CL","tasks":"[\"cs.CL\"]","methods":"[\"Large Language Model\",\"Language Model\"]","has_code":false,"code_links":[{"ID":613988,"CreatedAt":"2026-07-07T03:14:33.014478982Z","UpdatedAt":"2026-07-07T03:14:33.014478982Z","DeletedAt":null,"paper_id":5937820,"paper_url":"https://arxiv.org/abs/2607.04534","paper_title":"Mechanism-level routing failure in LLMs over Lean-verified algebraic structures","repo_url":"https://github.com/bytepro-ai/fiber-routing-eval","is_official":false,"mentioned_in_paper":false,"mentioned_in_github":true,"github_stars":0}]}