論文の概要: Maestro: Agentic Formal Proof Development by Coordination

• arxiv url: http://arxiv.org/abs/2610.25920v1
• Date: Mon, 19 Oct 2026 07:21:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 03:42:19.335886
• Title: Maestro: Agentic Formal Proof Development by Coordination
• Title（参考訳）: Maestro: コーディネーションによるエージェント形式証明の開発
• Abstract要約: Maestroは、グローバルな調整を通じて障害を処理するリーンの証明ハーネスです。 エージェントが飽和していないすべてのベンチマークにおいて、各モデルのネイティブコーディングエージェントよりも多くのターゲットを証明している。 また、共有するベンチマークで発行されたすべての証明システムよりも優れています。
• 参考スコア（独自算出の注目度）: 21.09901199432239
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Lean is increasingly used to verify mathematical proofs and software produced by LLM agents, but writing formal proofs remains hard. Existing prover systems take a divide-and-conquer approach that recursively decomposes hard proof obligations into easier lemmas and splits again any lemma that resists proof. However, a lemma can resist proof for different reasons, including insufficient guidance, a false statement, or a flaw in the decomposition that produced it. Existing systems cannot tell these apart as a failed attempt reports little beyond its failure, and responses are confined to the failing node without considering the rest of the proof or revising the plan above it. The system may thus keep decomposing obligations along a flawed proof direction until the budget runs out, causing the whole proof attempt to fail. We introduce Maestro, a Lean prover harness that handles failures through global coordination. Provers report why they failed, not just that they failed, and a coordinator that sees the whole proof chooses an appropriate response, such as guiding a stuck prover, correcting a false lemma, or retracting a flawed subtree and replanning it. The same harness extends to verified code synthesis, where a checked counterexample sends the code back for repair. We evaluate Maestro with four frontier LLMs on seven mathematics and three software verification benchmarks. It proves more targets than each model's native coding agent (Claude Code or Codex) on every benchmark the agent has not already saturated, with the largest gains on research-level mathematics. With Claude Opus 5, it discovers its own proofs of 34 of the 48 theorems in the June 2026 release of arXivLean, against 19 for the native agent. It also outperforms all published prover systems on every benchmark they share, solving 669/672 PutnamBench, 59/60 Lean-IMO-Bench, and 6/6 IMO 2026.
• Abstract（参考訳）: リーンは、LLMエージェントによって生成される数学的証明とソフトウェアを検証するためにますます使われていますが、公式な証明を書くことは難しいままです。 既存の証明システムでは、ハード証明義務を再帰的に分解し、より簡単な補題に分解し、証明に抵抗するあらゆる補題を再び分割する分割・対決方式を採用している。 しかし、補題は、十分なガイダンス、虚言、あるいはそれを生成した分解の欠陥など、様々な理由で証明に抵抗することができる。 既存のシステムでは、失敗した試行が失敗をほとんど報告していないため、これらを区別することはできない。 したがって、システムは、予算が切れるまで、欠陥のある証明方向に沿って義務を分解し続け、すべての証明試みが失敗する可能性がある。 マエストロ(Maestro)は、グローバルな調整を通じて障害を処理するリーンの証明ハーネスである。 証明者はなぜ失敗したのかを報告し、証明全体を見るコーディネーターは、立ち往生した証明者の指導、偽の補題の修正、欠陥のあるサブツリーの取り消し、そしてそれを再設計するなど、適切な反応を選択する。 同じハーネスは検証済みのコード合成にまで拡張され、チェックされた反例が修復のためにコードを返送する。 マエストロを7つの数学と3つのソフトウェア検証ベンチマークで4つのフロンティア LLM で評価した。 これは、各モデルのネイティブコーディングエージェント(Claude CodeまたはCodex)よりも、エージェントがまだ飽和していないベンチマークで多くのターゲットを証明し、研究レベルの数学で最大の利益を得ている。 Claude Opus 5では、2026年6月のarXivLeanリリースにおいて、ネイティブエージェントの19に対して、48の定理のうち34の証明を発見した。 また、共有するベンチマークのすべてで、パットナムベンチ669/672、リーン-IMO-ベンチ59/60、IMO 2026の6/6を解決している。

関連論文リスト

• Long-horizon autoformalization of a core theorem underlying MIP* = RE [2.596570510945053]
  本稿では,人間の監督下でAI証明エージェントを協調するシステムであるFormalFlowを紹介する。 共有ブループリントを使用して、ネストした計画、証明、レビューループをガイドする。 我々は,古典的低次検定の量子音響性の,マシンチェックによるLean 4証明を完成させた。
  論文  参考訳（メタデータ） (2026-09-17T07:26:49Z)
• Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
  大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。 Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。 このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
  論文  参考訳（メタデータ） (2026-08-05T21:29:12Z)
• Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
  大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。 このような戦略を課すことは不要で制限的であることを示す。 レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
  論文  参考訳（メタデータ） (2026-07-07T14:39:59Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。 我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
  論文  参考訳（メタデータ） (2026-06-03T20:09:39Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Mathematics with large language models as provers and verifiers [1.1029146548022293]
  ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
  論文  参考訳（メタデータ） (2025-10-11T20:35:25Z)
• 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)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。