論文の概要: APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

• arxiv url: http://arxiv.org/abs/2505.05758v2
• Date: Mon, 12 May 2025 08:03:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-13 14:13:13.058094
• Title: APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
• Title（参考訳）: APOLLO: 高度な形式推論のための自動LLMとリーンコラボレーション
• Authors: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh,
• Abstract要約: APOLLOは、Leanコンパイラの強みとLLMの推論能力を組み合わせた、モデルに依存しないパイプラインである。 miniF2Fベンチマークでは、新しい最先端精度75.0%が確立されている。
• 参考スコア（独自算出の注目度）: 8.056359341994941
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal reasoning and automated theorem proving constitute a challenging subfield of machine learning, in which machines are tasked with proving mathematical theorems using formal languages like Lean. A formal verification system can check whether a formal proof is correct or not almost instantaneously, but generating a completely correct formal proof with large language models (LLMs) remains a formidable task. The usual approach in the literature is to prompt the LLM many times (up to several thousands) until one of the generated proofs passes the verification system. In this work, we present APOLLO (Automated PrOof repair via LLM and Lean cOllaboration), a modular, model-agnostic pipeline that combines the strengths of the Lean compiler with an LLM's reasoning abilities to achieve better proof-generation results at a low sampling budget. Apollo directs a fully automated process in which the LLM generates proofs for theorems, a set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean, isolate failing sub-lemmas, utilize automated solvers, and invoke an LLM on each remaining goal with a low top-K budget. The repaired sub-proofs are recombined and reverified, iterating up to a user-controlled maximum number of attempts. On the miniF2F benchmark, we establish a new state-of-the-art accuracy of 75.0% among 7B-parameter models while keeping the sampling budget below one thousand. Moreover, Apollo raises the state-of-the-art accuracy for Goedel-Prover-SFT to 65.6% while cutting sample complexity from 25,600 to a few hundred. General-purpose models (o3-mini, o4-mini) jump from 3-7% to over 40% accuracy. Our results demonstrate that targeted, compiler-guided repair of LLM outputs yields dramatic gains in both efficiency and correctness, suggesting a general paradigm for scalable automated theorem proving.
• Abstract（参考訳）: 形式的推論と自動定理証明は機械学習の挑戦的なサブフィールドであり、機械はリーンのような形式言語を使って数学的定理を証明している。 形式的検証システムは、形式的証明がほぼ瞬時に正しいかどうかを確認することができるが、大きな言語モデル(LLM)で完全に正しい形式的証明を生成することは、恐ろしい作業である。 文献における通常のアプローチは、生成した証明の1つが検証システムを通過するまで、LCMに何回も(数千まで)促すことである。 本稿では,LLMによるAPOLLO(Automated PrOof repair via LLM and Lean cOllaboration)について紹介する。 Apollo氏は、LLMが定理の証明を生成する完全自動化プロセス、エージェントのセット、証明の分析、構文エラーの修正、リーンを使用した証明の誤りの特定、失敗するサブレムマの分離、自動解法の利用、各目標のLCMの実行を、トップK予算を低く抑える。 修復されたサブプロテクションは再結合され、再検証され、ユーザ制御された最大試行回数まで反復される。 miniF2Fベンチマークでは, サンプリング予算を1000以下に抑えながら, 7Bパラメータモデルのうち75.0%の精度を新たに確立した。 さらにアポロは、サンプルの複雑さを25,600から数百に削減しながら、Goedel-Prover-SFTの最先端の精度を65.6%に引き上げている。 汎用モデル(o3-mini、o4-mini)は3-7%から40%以上まで向上する。 この結果から,LLM出力の目標とするコンパイラ誘導型修復は効率と正確性の両方で劇的に向上し,拡張性のある自動定理証明のパラダイムが示唆された。

関連論文リスト

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
  大規模言語モデル(LLM)は、無数のタスクにまたがって印象的な機能を示してきたが、時には望ましくない出力が得られる。 本稿では LLM とプロセスベースの検証器を組み合わせた新しいフレームワーク LLM2 を紹介する。 LLMs2は妥当な候補を生成するのに責任を持ち、検証者は望ましい出力と望ましくない出力を区別するためにタイムリーなプロセスベースのフィードバックを提供する。
  論文  参考訳（メタデータ） (2024-12-29T06:32:36Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Laurel: Unblocking Automated Verification with Large Language Models [2.6942525604796366]
  大規模言語モデルを用いてアサーションを自動的に生成するツールであるLaurellを提案する。 実世界の3つのDafnysから抽出した複雑な補題のデータセットであるDafnyGymを、新しいベンチマークで評価した。
  論文  参考訳（メタデータ） (2024-05-27T03:26:01Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• MiniCheck: Efficient Fact-Checking of LLMs on Grounding Documents [62.02920842630234]
  GPT-4レベルの性能を持つが400倍の低コストでファクトチェックモデルを構築する方法を示す。 GPT-4を用いて合成トレーニングデータを構築することで,現実的かつ困難な事実エラーの事例を生成する。 評価のために, ファクトチェックとグラウンドグラウンド化に関する最近の研究から得られたデータセットを, 新たなベンチマーク LLM-AggreFact に統一する。
  論文  参考訳（メタデータ） (2024-04-16T17:59:10Z)

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

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