論文の概要: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis

• arxiv url: http://arxiv.org/abs/2501.18310v1
• Date: Thu, 30 Jan 2025 12:37:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-31 15:12:44.434951
• Title: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
• Title（参考訳）: きめ細かな証明構造解析による効率的なニューラルネットワーク理論の証明
• Authors: Haoxiong Liu, Jiacheng Sun, Zhenguo Li, Andrew C Yao,
• Abstract要約: 本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
• 参考スコア（独自算出の注目度）: 50.020850767257095
• License:
• Abstract: The synergy between deep learning models and traditional automation tools plays a pivotal role in developing robust neural theorem provers (NTPs). However, for proof synthesis with LLMs, previous work applies automation tools either only when the model explicitly calls the method, or only at a single granularity level, failing to fully exploit the power of built-in tactics and off-the-shelf automated theorem provers. In this work, we propose ProofAug, a novel theorem proving method that enjoys superior sample efficiency through equipping proof-generation LLMs with automation methods in different granularities via fine-grained structure analysis of model-generated proof proposals. Furthermore, ProofAug serves as a versatile plug-and-play module that seamlessly integrates with any tree-search algorithm, enabling our construction of an efficient recursive proving (ERP) module to further enhance performance. The superiority of our method is validated on the miniF2F-test benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant. Notably, by additionally employing a mixed prompting strategy, we achieve a cumulative pass rate of 66.0% after curation of the dataset (61.9% for the original version), setting a new SOTA across all proof languages with a total sample budget of only 2100. Our code is available at https://github.com/haoxiongliu/ProofAug.
• Abstract（参考訳）: ディープラーニングモデルと従来の自動化ツールの相乗効果は、堅牢なニューラルネットワーク定理プロバー(NTP)の開発において重要な役割を果たす。 しかし、LLMを用いた証明合成では、モデルが明示的にメソッドを呼び出す場合にのみ自動化ツールを適用するか、あるいは単一の粒度レベルでのみ適用し、組込み戦術とオフザシェルフ自動定理プローバーのパワーを完全に活用することができない。 本研究では, モデル生成した証明提案の微細構造解析を通じて, 異なる粒度の自動化手法を用いて, より優れたサンプル効率を示す新しい定理証明手法ProofAugを提案する。 さらにProofAugは,任意の木探索アルゴリズムとシームレスに統合可能な汎用的なプラグイン・アンド・プレイモジュールとして機能し,効率的な再帰的証明(ERP)モジュールの構築により,パフォーマンスをさらに向上する。 本手法の優位性を,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。 特に、混合プロンプト戦略を用いることで、データセットのキュレーション後の累積パスレート66.0%(原版は61.9%)を達成し、全証明言語に新しいSOTAを設定し、総サンプル予算は2100である。 私たちのコードはhttps://github.com/haoxiongliu/ProofAug.comで公開されています。

関連論文リスト

• CorrectBench: Automatic Testbench Generation with Functional Self-Correction using LLMs for HDL Design [6.414167153186868]
  機能的自己検証と自己補正を備えた自動テストベンチ生成フレームワークであるCorrectBenchを提案する。 提案手法は, 88.85%の成功率で生成したテストベンチの正当性を検証できる。 作業性能は, 従来よりも62.18%高く, 直接手法のパス比の約5倍である。
  論文  参考訳（メタデータ） (2024-11-13T10:45:19Z)
• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• Monte Carlo Tree Search Boosts Reasoning via Iterative Preference Learning [55.96599486604344]
  本稿では,Large Language Models (LLMs) の推論能力向上を目的とした,反復的な選好学習プロセスによるアプローチを提案する。 我々は、MCTS(Monte Carlo Tree Search)を用いて好みデータを反復的に収集し、そのルックアヘッド機能を利用して、インスタンスレベルの報酬をよりきめ細かいステップレベルの信号に分解する。 提案アルゴリズムはDPO(Direct Preference Optimization)を用いて,新たに生成されたステップレベルの優先度データを用いてLCMポリシーを更新する。
  論文  参考訳（メタデータ） (2024-05-01T11:10:24Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• A Simple Approach to Case-Based Reasoning in Knowledge Bases [56.661396189466664]
  我々は,古典人工知能(AI)におけるケースベース推論を想起させる,アンフノトレーニングを必要とする知識グラフ(KG)における推論に対する驚くほど単純かつ正確なアプローチを提案する。 ソースエンティティとバイナリ関係が与えられたターゲットエンティティを見つけるタスクを考えてみましょう。 我々の非パラメトリックなアプローチは、与えられた関係を通して類似したソースエンティティを接続する複数のテキストトグラフパスパターンを見つけることによって、クエリ毎にクレープな論理ルールを導出します。
  論文  参考訳（メタデータ） (2020-06-25T06:28:09Z)

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

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