Fugu-MT 論文翻訳(概要): When Does Structured Knowledge Help Neural Theorem Proving?

論文の概要: When Does Structured Knowledge Help Neural Theorem Proving?

arxiv url: http://arxiv.org/abs/2609.34460v1
Date: Mon, 28 Sep 2026 07:17:43 GMT
ステータス: 翻訳完了
システム内更新日: 2026-10-03 13:24:32.273873
Title: When Does Structured Knowledge Help Neural Theorem Proving?
Title（参考訳）: 構造化知識は神経理論の証明に役立つか?
Abstract要約: MathKGは364のMathlibsと9,434の型付きセマンティックエッジを接続する。我々は4つの拡張モード(文脈、知識グラフコンテキスト、Mathlib、両方)と5つのモデルで制御されたアブレーションを実行する。
参考スコア（独自算出の注目度）: 0.03110995905282905
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries such as Mathlib encode 285,000+ verified theorems with syntactic dependencies, but the semantic layer mathematicians rely on for discovery (analogies, generalizations, cross-domain bridges) remains implicit. We introduce MathAgent, which builds this layer as a knowledge graph, MathKG, and uses it to augment LLM theorem provers. MathKG connects 364 Mathlib theorems and definitions by 9,434 typed semantic edges inferred via LLM-based relation extraction anchored to verified Mathlib declarations. We run a controlled ablation across four augmentation modes (no context, knowledge-graph context, Mathlib retrieval, both) and five models: Qwen3-8B/32B, their Lean-specialized derivatives Goedel-Prover-V2-8B/32B, and Claude Sonnet 4.6, on miniF2F, plus PutnamBench and MathOlympiadBench for Sonnet. Three findings emerge. (i) Specialization dominates augmentation: Lean fine-tuning adds 33-38 percentage points of solve rate in every mode, and a specialized 8B model beats a $4\times$ larger general one by 29-35 points, while no augmentation mode improves solve rate by more than 3 points. (ii) Augmentation is capability-conditioned: knowledge-graph context helps small models but hurts large ones, with the specialized model gaining more relative to its general base at every scale. (iii) Yet the augmentation modes solve different problems: an oracle selecting the best mode per problem solves 6% to 58% more than the unaugmented prover, a complementarity effect that strengthens on harder problems (32% more on PutnamBench). These results motivate adaptive strategies that select augmentation by model capability and problem. Code, data, and artifacts are available at https://github.com/sarehnabi/mathagent
Abstract（参考訳）: 構造化された数学的知識は、LLMがLean 4の定理を証明するのに役立つか? もしそうなら、どのモデルで、答えは問題によって異なりますか? マトリブのような形式的なライブラリは、構文的依存関係を持つ285,000以上の証明済み定理を符号化するが、意味層数学者は発見(アナロジー、一般化、クロスドメインブリッジ)に頼っている。この層を知識グラフMathKGとして構築するMathAgentを導入する。 MathKGは、364のMathlib定理と9,434の型付きセマンティックエッジで定義する。我々は4つの拡張モード(文脈、知識グラフコンテキスト、Mathlib検索なし)と5つのモデル(Qwen3-8B/32B、そのリーン特殊化微分であるGoedel-Prover-V2-8B/32B、miniF2F上のClaude Sonnet 4.6、およびPutnamBenchとMathOlympiadBench for Sonnet)で制御されたアブレーションを実行する。 3つの発見がある。一リーン微調整は各モードで33～38ポイントの解率を加算し、特化8Bモデルは一般の解率を29～35ポイント上回り、増減モードでは解率を3ポイント以上改善する。知識グラフのコンテキストは小さなモデルでは役立ちますが、大きなモデルには問題があります。 3) 増補モードは, 問題ごとの最良のモードを選択するオラクルが, 未解決の証明者よりも6%から58%多く解き, パットナムベンチでは32%高くなる。これらの結果は、モデル能力と問題による拡張を選択する適応戦略を動機付けている。コード、データ、アーティファクトはhttps://github.com/sarehnabi/mathagent.comで入手できる。

論文の概要: When Does Structured Knowledge Help Neural Theorem Proving?

関連論文リスト