HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

要約

正式な方法は、厳格な数学的証拠を通じて重要なシステムの信頼性を検証するために極めて重要です。
ただし、その採用は、労働集約的なマニュアルプルーフと定理プロバーを使用するために必要な専門知識によって妨げられています。
大規模な言語モデル（LLMS）の最近の進歩は、自動定理証明のための新しい機会を提供します。
2つの有望なアプローチは、段階的に戦術を生成し、LLMで直接的な証明を生成することです。
ただし、既存の作業は、2つのアプローチを組み合わせることを試みません。
この作業では、戦術に基づく生成と総合的な合成を組み合わせて、両方のアプローチの利点を活用するデュアルモデル証明合成フレームワークであるハイブリッドプロバーを紹介します。
HybridProverは、評価のために直接証明候補全体を生成し、それらの候補者から証明スケッチを抽出します。
次に、自動化されたツールを統合して段階的な改良を介してスケッチを完成させる戦術ベースの生成モデルを使用します。
最適化されたIsabelleデータセットに、Isabelle Theorem ProverのハイブリッドプロバーとLLMSを微調整します。
MINIF2Fデータセットの評価は、ハイブリッドプロバーの有効性を示しています。
MINIF2Fで59.4％の成功率を達成し、以前のSOTAは56.1％です。
私たちのアブレーション研究は、このSOTAの結果が、根本的な世代と戦術に基づく世代を組み合わせることに起因することを示しています。
さらに、データセットの品質、トレーニングパラメーター、およびサンプリングの多様性が、LLMSで証明する自動定理中の最終結果にどのように影響するかを示します。
すべてのコード、データセット、およびLLMはオープンソースです。

要約(オリジナル)

Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theorem provers. Recent advancements in large language models (LLMs) offer new opportunities for automated theorem proving. Two promising approaches are generating tactics step by step and generating a whole proof directly with an LLM. However, existing work makes no attempt to combine the two approaches. In this work, we introduce HybridProver, a dual-model proof synthesis framework that combines tactic-based generation and whole-proof synthesis to harness the benefits of both approaches. HybridProver generates whole proof candidates for evaluation directly, then extracts proof sketches from those candidates. It then uses a tactic-based generation model that integrates automated tools to complete the sketches via stepwise refinement. We implement HybridProver for the Isabelle theorem prover and fine-tune LLMs on our optimized Isabelle datasets. Evaluation on the miniF2F dataset illustrates HybridProver’s effectiveness. We achieve a 59.4% success rate on miniF2F, where the previous SOTA is 56.1%. Our ablation studies show that this SOTA result is attributable to combining whole-proof and tactic-based generation. Additionally, we show how the dataset quality, training parameters, and sampling diversity affect the final result during automated theorem proving with LLMs. All of our code, datasets, and LLMs are open source.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google