論文の概要: Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
- arxiv url: http://arxiv.org/abs/2606.06468v1
- Date: Thu, 04 Jun 2026 17:54:44 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-05 22:39:45.021599
- Title: Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
- Title（参考訳）: Goedel-Architect: Blueprint生成とリファインメントによる形式理論の合理化
- Authors: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora,
- Abstract要約: 私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。
Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。
これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
- 参考スコア（独自算出の注目度）: 69.77146194380488
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the main theorem. First, Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies. This blueprint is optionally guided by a natural language proof. Then, a tool-equipped Lean prover component closes each open lemma node in parallel using relevant dependencies. Failed lemmas in turn drive refinement of the global blueprint. This strategy contrasts with other mainstream approaches which use recursive lemma decomposition, and can inefficiently loop on dead-end strategies. Using the open-weight DeepSeek-V4-Flash (284B-A13B) as the backbone, Goedel-Architect attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench. With an optional natural-language proof seeding the initial blueprint on the harder problems, we additionally close the remaining two MiniF2F-test problems (reaching 100%), lift PutnamBench to 88.8% (597/672), and solve 4/6 on IMO 2025, 11/12 on Putnam 2025, and 3/6 on USAMO 2026. This represents state-of-the-art performance for an open-source pipeline at a price point up to 500x less than comparable open-source pipelines.
- Abstract（参考訳）: Goedel-Architectは、リーン4で証明された形式的定理のためのエージェントフレームワークで、青写真の生成と洗練を主眼にしています。
ブループリント(英: blueprint)とは、定義と補題の依存グラフであり、主定理を成す。
まず、Goedel-Architectは宣言された依存関係とともに、公式に定義された定義と補題の青写真を生成する。
この青写真は、自然言語の証明によって任意に導かれる。
次に、ツールを備えたLean proverコンポーネントが、関連する依存関係を使用して、各オープンなlemmaノードを並行してクローズする。
失敗に終わった補題は、世界的な青写真の改良に繋がる。
この戦略は、再帰的な補題分解を使い、デッドエンド戦略に非効率にループできる他の主流のアプローチとは対照的である。
オープンウェイトなDeepSeek-V4-Flash(284B-A13B)をバックボーンとして、Goedel-ArchitectはMiniF2F-testで99.2% pass@1、PatnamBenchで75.6% pass@1を達成した。
厳密な問題に対して初期ブループリントをシードする任意の自然言語証明により、残りの2つのMiniF2Fテスト問題(100%)を閉じ、PutnamBenchを88.8%(597/672)に引き上げ、IMO 2025では4/6、Putnam 2025では11/12、USAMO 2026では3/6に解いた。
これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
関連論文リスト
- 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) - Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 [1.2816802110958607]
これは、一度精巧な証明状態をキャプチャし、Lean 4言語サーバーへの小さな拡張を通じてブランチ間で再利用します。
48のミニF2F-v2問題に対して,本手法は標準的なフォールバックよりも5.6～50倍の高速化を実現する。
論文 参考訳（メタデータ） (2026-05-25T08:12:26Z) - Gödel's Poetry [0.0]
本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。
分解せずにMiniF2Fの90.4%のパスレートを達成する。
重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
論文 参考訳（メタデータ） (2025-12-16T10:00:01Z) - ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization [10.021930888250546]
現在のアプローチでは、オリジナルの人間による議論の意味的意味と論理的構造を保存できない。
本稿では,構造的忠実度を主目的とする新しいパイプラインであるProofFlowを紹介する。
我々は184人の学部レベルの問題に対して,ステップバイステップのソリューションを手動でアノテートした新しいベンチマークを提示する。
また,構文的正しさ,意味的忠実度,構造的忠実度を評価するための新しい合成指標ProofScoreを導入する。
論文 参考訳（メタデータ） (2025-10-13T10:20:11Z) - Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving [44.5694120006447]
決定論的マルコフ決定過程として,問題解決の原理的定式化を提案する。
また,既存のFTP環境を利用してプロセス検証問題解決を行う新しいフレームワークFPSを提案する。
我々は, MATH500ベンチマークのサブセットの形式化であるFormalMath500, MiniF2F-Solving, PutnamBench-Solving, FTPベンチマークのMiniF2FとPutnamBenchの適応の3つのベンチマークを構築した。
論文 参考訳（メタデータ） (2025-05-07T16:02:14Z) - 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) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。