論文の概要: 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 22:50:04.155454
- 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: http://creativecommons.org/licenses/by/4.0/
- 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で公開されています。
関連論文リスト
- Reasoning with Reinforced Functional Token Tuning [70.96651128307985]
本稿では,大規模言語モデル(LLM)に自己学習能力を持たせるためにRFTT(Reinforced Functional Token Tuning)を提案する。
RFTTは、学習可能な関数トークンの豊富なセットをモデル語彙に直接埋め込んで、多様な人間のような推論行動によるチェーン・オブ・思想の構築を可能にする。
論文 参考訳(メタデータ) (2025-02-19T02:59:42Z) - Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。
我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。
この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
論文 参考訳(メタデータ) (2025-02-16T06:20:39Z) - Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。
最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。
我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
論文 参考訳(メタデータ) (2024-10-25T19:25:00Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳(メタデータ) (2024-10-21T08:04:21Z) - Bypass Back-propagation: Optimization-based Structural Pruning for Large Language Models via Policy Gradient [57.9629676017527]
大規模言語モデルを用いた最適化に基づく構造解析手法を提案する。
我々は,プルーニングモデルの損失を最適化することにより,確率空間におけるプルーニングマスクを直接学習する。
A100 GPUで13Bモデルに対して約35GBのメモリで2.7時間動作させる。
論文 参考訳(メタデータ) (2024-06-15T09:31:03Z) - 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) - 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) - 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) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳(メタデータ) (2023-03-08T22:00:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。