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

• arxiv url: http://arxiv.org/abs/2505.05758v3
• Date: Wed, 06 Aug 2025 01:58:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-07 15:43:08.590009
• 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の推論能力を組み合わせた、モデルに依存しないパイプラインである。 エージェントのセットが証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定します。 修理されたサブステイストは再結合され、再検証され、ユーザ制御された最大試行回数まで反復される。
• 参考スコア（独自算出の注目度）: 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 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, modelagnostic pipeline that combines the strengths of the Lean compiler with an LLM's reasoning abilities to achieve better proofgeneration 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 sublemmas, utilize automated solvers, and invoke an LLM on each remaining goal with a low budget. The repaired subproofs are recombined and reverified, iterating up to a usercontrolled maximum number of attempts. On the miniF2F benchmark, we establish a new stateoftheart accuracy of 84.9% among sub 8Bparameter models while keeping the sampling budget below one hundred. Moreover, Apollo raises the stateoftheart accuracy for GoedelProverSFT to 65.6% while cutting sample complexity from 25,600 to a few hundred. Generalpurpose models (o3mini, o4mini) jump from 3-7% to over 40% accuracy. Our results demonstrate that targeted, compilerguided repair of LLM outputs yields dramatic gains in both efficiency and correctness, suggesting a general paradigm for scalable automated theorem proving. The codebase is available at https://github.com/aziksh-ospanov/APOLLO
• Abstract（参考訳）: 形式的推論と自動定理証明は機械学習の挑戦的なサブフィールドであり、機械はリーンのような形式言語を使って数学的定理を証明している。 形式的検証システムは、形式的証明がほぼ瞬時に正しいかどうかを確認することができるが、LLMで完全に正しい形式的証明を生成することは、恐ろしい作業である。 文献における通常のアプローチは、生成した証明の1つが検証システムを通過するまで、LCMに何回も(数千まで)促すことである。 本稿では,LLMによるAPOLLO(Automated PrOof repair via LLM and Lean cOllaboration)について紹介する。 Apollo氏は、LLMが定理の証明を生成する完全に自動化されたプロセス、エージェントのセットが証明を分析し、構文上のエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動解法を利用し、残りの目標に対して低予算でLCMを起動する。 修理されたサブステイストは再結合され、再検証され、ユーザ制御された最大試行回数まで反復される。 miniF2Fベンチマークでは,サンプリング予算を100以下に抑えつつ,サブ8Bparameterモデルの84.9%の精度を新たに確立した。 さらにアポロは、サンプルの複雑さを25,600から数百に削減しながら、GoedelProverSFTの最先端の精度を65.6%に引き上げている。 汎用モデル(o3mini、o4mini)は37%から40%以上の精度に向上する。 この結果から,LLM 出力のターゲット的,コンパイラ誘導的修復は効率と正確性の両方において劇的に向上し,拡張性のある自動定理証明のパラダイムが示唆された。 コードベースはhttps://github.com/aziksh-ospanov/APOLLOで公開されている。

関連論文リスト

• HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement [7.702809989052384]
  HybridProverは、戦術ベースの生成と全防御合成を組み合わせたデュアルモデル証明フレームワークである。 最適化されたデータセット上にIsabelle定理証明器とファインチューンLPMにHybridProverを実装した。
  論文  参考訳（メタデータ） (2025-05-21T16:45:43Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• 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)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• 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)

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

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