論文の概要: Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
- arxiv url: http://arxiv.org/abs/2609.11319v1
- Date: Thu, 10 Sep 2026 09:48:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-11 23:53:35.297037
- Title: Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
- Title（参考訳）: Magenta: 数学的推論とリーン検証のループを閉じる
- Abstract要約: リーンシグナルを推論プロセスに統合することで、非公式な推論と公式な推論のギャップを埋めます。
トレーニング不要のエージェントパイプラインであるMagentaを紹介します。これは、自然言語の問題のみを与えられた上で、回答を生成し、Lean 4ステートメントとして表現し、マシンチェックされた証明を構築します。
- 参考スコア（独自算出の注目度）: 13.942115092285697
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof. A statement judge verifies whether the formalisation preserves the original problem, while an error-attribution judge routes failed attempts either to mathematical re-derivation or local Lean repair. Magenta achieves 100% accuracy across all evaluated olympiad benchmarks, including AIME 2025, AIME 2026, and HMMT February 2026. When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems. Our analysis shows that statement adjudication is essential for preventing false certificates and that feedback-guided correction outperforms independent resampling on difficult problems.
- Abstract（参考訳）: 数学の知識の大部分は、数学と自然言語の非公式な使用を通じて伝達されてきた。
大規模言語モデル(LLM)は、自然言語の使用に非常に適しており、非公式な数学的推論において、性能は高いが完璧ではない。
LLMを非公式な推論に制限することは、マシンがマシンチェック可能な証明を通じて提供する個別の検証能力を使用する機会を逃す。
本稿では,リーン信号を非公式な推論プロセスに統合することにより,形式的推論と形式的推論のギャップを埋める。
トレーニング不要のエージェントパイプラインであるMagentaを紹介します。これは、自然言語の問題のみを与えられた上で、回答を生成し、Lean 4ステートメントとして表現し、マシンチェックされた証明を構築します。
声明裁判官は、形式化が元の問題を保存しているかどうかを検証し、エラー帰属判事は、数学的導出または局所的なリーン修復の試みを失敗する。
Magentaは、AIME 2025、AIME 2026、HMMT 2026を含む全ての評価されたオリンピックベンチマークで100%の精度を実現している。
オープンウェイトなK2-Horizon-7B推論器と組み合わせると、6つのIMO 2026問題を全て解決する。
本分析は, 誤証明の防止には文の弁証が不可欠であり, フィードバック誘導補正は, 難解な問題に対する独立した再サンプリングよりも優れていることを示す。
関連論文リスト
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs [32.234133057592935]
Hermesはツール支援エージェントで、リーンシステムにおける検証段階と非公式な推論をインターリーブする。
パラメータスケールの異なる LLM を用いて,Hermes を4つの挑戦的数学的推論ベンチマークで評価する。
論文 参考訳（メタデータ） (2025-11-24T04:50:18Z) - Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-29T15:30:31Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
大規模言語モデル(LLM)は、驚くべき数学的推論能力を示しているが、そのソリューションには自動検証できないエラーが含まれていることが多い。
非公式な推論と形式的検証の相補的な強みを組み合わせたエージェントフレームワークであるHilbertを紹介する。
我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。
論文 参考訳（メタデータ） (2025-09-26T18:24:23Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Intermediate Languages Matter: Formal Choice Drives Neurosymbolic LLM Reasoning [50.99811144731619]
形式言語の選択は構文的および意味論的推論能力の両方に影響を及ぼすことを示す。
平均的な文脈認識エンコーディングはLCMの推論に役立つが、コメントやマークダウン構文を使うことによる明らかな影響はない、と結論付けている。
論文 参考訳（メタデータ） (2025-02-24T14:49:52Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。
実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-06-20T06:42:27Z) - Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization [45.439933713342256]
大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。
LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。
これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
論文 参考訳（メタデータ） (2024-03-26T22:01:13Z) - Maieutic Prompting: Logically Consistent Reasoning with Recursive
Explanations [71.2950434944196]
ノイズや一貫性のない言語モデルでさえも問題に対する正しい答えを推測するMaieutic Promptingを開発する。
Maieutic Promptingは最先端のプロンプト法よりも最大20%精度が高い。
論文 参考訳（メタデータ） (2022-05-24T06:36:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。