ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis

要約

ディープラーニングモデルと、プルーフアシスタントの組み込み戦術や既製の自動定理プロバーなどの従来の自動化ツールとの相乗効果は、堅牢で効率的な神経定理プロバー（NTP）を開発する上で重要な役割を果たします。
ただし、LLMSを使用したプルーフ合成の場合、以前の作業は、モデルによって明示的に呼び出された場合、または単一の粒度レベルでのみ、自動化ツールを適用します。
この問題を解決するために、モデル生成された証明提案の細粒構造分析を通じて、LLMSにさまざまな粒度に自動化方法を装備する手順であるProofAugを提案します。
Proofaugは、任意のツリー検索アルゴリズムとシームレスに統合する汎用性の高いプラグアンドプレイモジュールとしても機能し、効率的な再帰証明（ERP）モジュールの構築を可能にして、パフォーマンスをさらに強化します。
この方法の優位性は、オープンソースのdeepseek-math-7bベースモデルとイザベルプルーフアシスタントを使用して、minif2fベンチマークで検証されます。
特に、混合プロンプト戦略をさらに採用することにより、データセットのキュレーション後に66.0％の累積パス率（元のバージョンの61.9％）を達成します。
また、Minif2F-TestでKimina-Prover-Preview-Distill-1.5Bのパス@1パフォーマンスを44.3％から50.4％に改善できるLEAN 4バージョンのProofAugも実装しています。
私たちのコードは、https：//github.com/haoxiongliu/proofaugで入手できます。

要約(オリジナル)

The synergy between deep learning models and traditional automation tools, such as built-in tactics of the proof assistant and off-the-shelf automated theorem provers, plays a crucial role in developing robust and efficient neural theorem provers(NTPs). However, for proof synthesis with LLMs, previous work applies automation tools either only when explicitly invoked by the model or at a single granularity level, failing to fully exploit their power. To solve this issue, we propose ProofAug, a procedure that equips LLMs with automation methods at various granularities through fine-grained structure analysis of model-generated proof proposals. ProofAug also 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 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) with 2100 queries to the model per problem (In contrast, the previous SOTA in Isabelle, Subgoal-XL, only achieves 56.1% using 16384 queries per problem). We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-Preview-Distill-1.5B from 44.3% to 50.4% on miniF2F-test. Our code is available at https://github.com/haoxiongliu/ProofAug.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google