論文の概要: Mechanism-level routing failure in LLMs over Lean-verified algebraic structures
- arxiv url: http://arxiv.org/abs/2607.04534v1
- Date: Sun, 05 Jul 2026 22:45:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-07 22:26:29.973209
- Title: Mechanism-level routing failure in LLMs over Lean-verified algebraic structures
- Title（参考訳）: リーン検証代数構造上のLLMにおける機構レベルルーティング障害
- Authors: Manuel Israel Cázares, Wenlin Zhang, Haobo Ma,
- Abstract要約: 本研究では,大規模言語モデル (LLM) における構造的ルーティング障害を,形式的に検証された代数的コーパス上で検討する。
私たちの中心的な発見はメカニズムレベルのルーティング天井です。
ラマにおけるクロスモデル解離は注目に値する。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 本稿では,大規模言語モデル(LLM)における構造的ルーティング障害に関する実証的研究を,形式的に検証された代数的コーパス上で行った。
このタスクは、Lean 4のFiberRing形式化から引き出されたコンパクトな数学的オブジェクトのための固定された閉じたテンプレートセットから正しい証明機構のラベルを選択し、各アイテムをリーン認定アーティファクトに固定し、対応する証明書ファミリーからラベルを割り当てる。
盲目状態では、gpt-oss-120bは22のFiberRingアイテム(n=66, temperature=0, seed=0)に対して80.3%のテンプレート精度を達成し、Llama 3.3 70Bは68.2%に達する。
メカニズムを具体化するリーン検証/知性キュー(Condition A2)は、精度を90.9%と81.8%に向上させ、+10.6と+13.6ppのギャップをキューによるルーティングアップリフトと呼ぶ。
gpt-oss-120bは12個のCRTアイテムのうち7個(58.3%)が盲目で、A2は0である。
検証精度は両方の条件(95.5%)で同一であり、テンプレート精度は13.6ppで改善され、真理推論と証明力学の分類が分離可能な能力であることが確認される。
クロスコーパス拡張(Set B; 6 POM/CollisionKernelItems, 72 Evaluations)は、小さなクロスモジュールチェックを提供する。
これらの結果は、ルータ仮説(カザレス2026)を形式的代数構造へと拡張する。
完全なパイプライン、マニフェスト、結果はhttps://github.com/bytepro-ai/fiber-routing-eval.comにある。
関連論文リスト
- Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
PointArena 2026は77.2%の精度でベンチマークで2位である。
ap proachは3つの障害モードをターゲットにしている。第一に、エージェント駆動のシンセシスは大きなセマンティクスとアンカー相対的な候補プールを構築する。
次に、determinis tic steerable-dataパイプラインは、認証された10,000サンプルのメインセットと、マスク、テンプレート、パス検証を使用するリザーブサンプルを生成する。
論文 参考訳（メタデータ） (2026-06-29T06:39:03Z) - Mat-Pref: Verifiable-Reward Training Improves Compositional Reasoning in Inorganic Materials [2.102846336724103]
Mat-Prefは、11の無機構造体ファミリーにわたる10,837のイオン置換質問のベンチマークである。
4つのゼロショットフロンティアモデルは、すべての分割において33-54%の範囲に留まっており、スケールだけでは、このタスク要求の合成化学的理由を解決していないことを確認している。
論文 参考訳（メタデータ） (2026-06-20T01:46:41Z) - Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
シャノン型エントロピーの不等式を証明することは情報理論の基本的な課題である。
我々は,原子実証のステップを微調整した小規模大規模言語モデルがこのプロセスを自動化することができるか検討する。
GPT-5.5は0ショットプロンプトで1.7%のサンプルを解き、Psitipは33.3%のサンプルを解いた。
論文 参考訳（メタデータ） (2026-06-04T05:43:12Z) - Agentic Proving for Program Verification [44.663012714194025]
エージェントシステムは、形式数学における自動定理証明のための最先端のアプローチとして登場した。
検証可能なコード生成のためのLean 4ベンチマークであるCLEVERのエージェント証明フレームワークでClaude Codeを評価した。
論文 参考訳（メタデータ） (2026-05-22T15:41:27Z) - Amplifying, Not Learning: Fine-Tuned AI Text Detectors Amplify a Pretrained Direction [51.56484100374058]
テキスト検出器は、事前訓練された典型軸を増幅する。
タスク監督前の生エンコーダでは、3つのアーキテクチャでNYT-vs-HC3 AUROC 0.806/0.944/0.834を達成する。
RoBERTaベースでは、生のプロジェクションは微調整を超えるが、RoBERTaベースでは、フル微調整は、試験された流線型人口の双方で生よりも識別を小さくする。
論文 参考訳（メタデータ） (2026-05-20T19:08:38Z) - Decodable but Not Corrected by Fixed Residual-Stream Linear Steering: Evidence from Medical LLM Failure Regimes [4.738949927143789]
隠れ状態における線形デオード可能な故障信号が、それらの故障を修正するために活用できるかどうかを検討する。
固定されたリニアステアリングファミリーが修正に利用できない場合でも、デオード可能な故障構造がポストジェネレーションの信頼性評価をサポートすることがわかった。
論文 参考訳（メタデータ） (2026-05-07T05:58:38Z) - Post-Cut Metadata Inference Attacks on Quantum Circuit Cutting Pipelines [3.9890357781493595]
量子回路切断により、回路を実行可能なフラグメントに分解することで、量子ビット容量を超えるワークロードを、短期的な量子デバイスで実行することができる。
フラグメントレベルの実行トランスクリプトは、半最高級のクラウドプロバイダによって監視可能である。
我々はこの表面を定式化し、ポストカットされた文字起こしが実用的なメタデータ側チャネルを構成することを示す。
論文 参考訳（メタデータ） (2026-04-12T11:51:05Z) - Validated Intent Compilation for Constrained Routing in LEO Mega-Constellations [1.0152838128195467]
本稿では,高レベルな演算子の意図を低レベルなルーティング制約に変換するエンドツーエンドシステムを提案する。
我々のシステムは,運用運用に必要な安全保証を維持しつつ,オペレータ意図とネットワーク構成のセマンティックなギャップを埋める。
論文 参考訳（メタデータ） (2026-04-08T16:29:25Z) - Hierarchy-Guided Topology Latent Flow for Molecular Graph Generation [44.50339042016925]
本稿では,グローバルコンテキストに対する潜在的マルチスケールプランを用いた3次元座標を用いた結合グラフを生成するプランナー・エグゼクタモデルを提案する。
HLTFは98.8%の原子安定性と92.9%の有効・均一性を達成し、PoseBustersの妥当性は94.0%(+0.9)に向上した。
GEOM-DRUGSでは、HLTFは後処理なしで85.5%/85.0%の妥当性/バリッド・ユニク・ノーベル、標準化された緩和後の92.2%/91.2%を達成している。
論文 参考訳（メタデータ） (2026-03-28T03:48:13Z) - LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning [46.294745464571456]
LongCat-Flash-Proverはエージェントツール統合推論のためのオープンソースのMoEモデルである。
これは、自己形式化と定理証明の両方において、オープンウェイトモデルのための新しい最先端状態を設定する。
MiniF2F-Testのパスレートは97.1%で、72の推論予算しか使用していない。
論文 参考訳（メタデータ） (2026-03-22T05:16:09Z) - When Does Content-Based Routing Work? Representation Requirements for Selective Attention in Hybrid Sequence Models [0.0]
ハイブリッドリカレントアテンションアーキテクチャにおけるルーティングパラドックスを同定する。
コンテンツベースのルーティングは、ルーティングが避けるように設計されたペアワイズな計算を必要とすることを示す。
論文 参考訳（メタデータ） (2026-03-22T01:04:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。