Mechanism-level routing failure in LLMs over Lean-verified algebraic structures

• URL: http://arxiv.org/abs/2607.04534v1
• Date: Sun, 05 Jul 2026 22:45:49 GMT
• Title: Mechanism-level routing failure in LLMs over Lean-verified algebraic structures
• Abstract summary: We study structural routing failure in large language models (LLMs) over a formally verified algebraic corpus.<n>Our central finding is a mechanism-level routing ceiling.<n>A cross-model dissociation in Llama is notable.
• Score: 3.8048003898069975
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  A research idea may be novel, coherent, and scientifically plausible, yet its proposed method may remain insufficiently specified for faithful implementation.<n>We study the codification readiness of implementation-facing research-method specifications, defined by whether they provide sufficient methodological information for a competent implementer or coding agent to construct the intended method without unsupported assumptions.<n>We introduce IdeaAMBIG, a benchmark of 660 evidence-grounded instances: 163 real-world gaps from reports and GitHub issues, and 497 controlled synthetic gaps injected into codification-ready references.
  arXiv  Detail & Related papers  (2026-09-09T17:59:04Z)
• Routing Ceilings Are Domain-Independent: Structural Prior Injection in Code Security Vulnerability Detection [0.0]
  Large language models (LLMs) exhibit a well-documented gap between latent capability and consistent activation.<n>Prior work reports that structural priors raise in-distribution performance dramatically, yet collapse below the zero-shot baseline out-of-distribution.<n>We test whether this phenomenon is cross-domain by reproducing the SAIR design in source-code security vulnerability detection.
  arXiv  Detail & Related papers  (2026-07-16T06:45:08Z)
• Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
  We describe our PointArena 2026 solution, which achieves 77.2% overall accuracy and ranks second on the benchmark.<n>The ap proach targets three failure modes. First, agent-driven syn thesis builds large semantic and anchor-relative candidate pools.<n>Second, a determinis tic steerable-data pipeline creates a verified 10,000-sample main set, plus reserve samples, using masks, templates, and path verification.
  arXiv  Detail & Related papers  (2026-06-29T06:39:03Z)
• Mat-Pref: Verifiable-Reward Training Improves Compositional Reasoning in Inorganic Materials [2.102846336724103]
  Mat-Pref is a benchmark of 10,837 ionic-substitution questions across 11 inorganic structure families.<n>Four zero-shot frontier models remain in the 33-54% range on every split, confirming that scale alone does not resolve the compositional chemical reasoning this task demands.
  arXiv  Detail & Related papers  (2026-06-20T01:46:41Z)
• Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
  Proving Shannon-type entropy inequalities is a fundamental task in information theory.<n>We investigate whether small-scale large language models, fine-tuned on atomic proof steps, can automate this process.<n>We show that GPT-5.5 solves 1.7% samples under zero-shot prompting while Psitip solves 33.3% samples.
  arXiv  Detail & Related papers  (2026-06-04T05:43:12Z)
• Agentic Proving for Program Verification [44.663012714194025]
  Agentic systems have emerged as state-of-the-art approaches for automated theorem proving in formal mathematics.<n>We evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation.
  arXiv  Detail & Related papers  (2026-05-22T15:41:27Z)
• Amplifying, Not Learning: Fine-Tuned AI Text Detectors Amplify a Pretrained Direction [51.56484100374058]
  Text detectors amplify a pretrained typicality axis; they do not construct an AI-vs-human boundary.<n>On raw encoders before any task supervision, projecting onto centroid(AI)-centroid(HC3) achieves NYT-vs-HC3 AUROC 0.806/0.944/0.834 across three architectures.<n>On RoBERTa-base, raw projection exceeds fine-tuning; on RoBERTa-base, full fine-tuning reduces discrimination below raw on both fluent-formal populations tested.
  arXiv  Detail & Related papers  (2026-05-20T19:08:38Z)
• Decodable but Not Corrected by Fixed Residual-Stream Linear Steering: Evidence from Medical LLM Failure Regimes [4.738949927143789]
  We investigate whether linearly decodable failure signals in hidden states can be leveraged to correct those failures.<n>We find that decodable failure structure supports post-generation reliability estimation even when the fixed linear steering family cannot exploit it for correction.
  arXiv  Detail & Related papers  (2026-05-07T05:58:38Z)
• Post-Cut Metadata Inference Attacks on Quantum Circuit Cutting Pipelines [3.9890357781493595]
  Quantum circuit cutting enables near-term quantum devices to execute workloads exceeding their qubit capacity by decomposing circuits into runnable fragments.<n>This creates a previously unexplored confidentiality surface: the fragment-level execution transcript observable by a semi-honest cloud provider.<n>We formalise this surface and demonstrate that post-cut transcripts constitute a practical metadata side channel.
  arXiv  Detail & Related papers  (2026-04-12T11:51:05Z)
• Validated Intent Compilation for Constrained Routing in LEO Mega-Constellations [1.0152838128195467]
  We present an end-to-end system for translating high-level operator intents into low-level routing constraints.<n>Our system bridges the semantic gap between operator intent and network configuration while maintaining the safety guarantees required for operational deployment.
  arXiv  Detail & Related papers  (2026-04-08T16:29:25Z)
• Hierarchy-Guided Topology Latent Flow for Molecular Graph Generation [44.50339042016925]
  We propose a planner-executor model that generates bond graphs with 3D coordinates using a latent multi-scale plan for global context.<n>HLTF achieves 98.8% atom stability and 92.9% valid-and-unique, improving PoseBusters validity to 94.0% (+0.9 over the strongest reported baseline)<n>On GEOM-DRUGS, HLTF attains 85.5%/85.0% validity/valid-unique-novel without post-processing and 92.2%/91.2% after standardized relaxation.
  arXiv  Detail & Related papers  (2026-03-28T03:48:13Z)
• LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning [46.294745464571456]
  LongCat-Flash-Prover is an open-source MoE model for agentic tool-integrated reasoning.<n>It sets a new state-of-the-art for open-weights models in both auto-formalization and theorem proving.<n>It achieves a 97.1% pass rate on MiniF2F-Test using only 72 inference budget per problem.
  arXiv  Detail & Related papers  (2026-03-22T05:16:09Z)
• When Does Content-Based Routing Work? Representation Requirements for Selective Attention in Hybrid Sequence Models [0.0]
  We identify a routing paradox in hybrid recurrent-attention architectures.<n>We show that content-based routing requires exactly the pairwise computation that routing is designed to avoid.
  arXiv  Detail & Related papers  (2026-03-22T01:04:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.