LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

要約

数学的推論は、幻覚のために大規模な言語モデル（LLMS）にとって重要な課題のままです。
リーンのような正式な証明アシスタントと組み合わせると、これらの幻覚は厳密な検証によって排除され、定理が信頼できることを証明することができます。
しかし、正式な検証があっても、LLMは依然として長い証拠と複雑な数学的な形式化に苦労しています。
LENMSを使用してLLMSは、補題の取得、戦術の生成、さらには完全な証拠にさえ貴重な支援を提供しますが、重要な能力が欠けています。証明の進歩の感覚を提供します。
この制限は、特に大規模な形式化プロジェクトの全体的な開発効率に影響を与えます。
LeanProgressを紹介します。これは、証明の進捗を予測する方法です。
Lean Workbook PlusとMathlib4からのリーンプルーフの大規模なコーパスで作成されたモデルのトレーニングと評価、およびそれを完了するためのステップ数は、データの前処理とバランスのテクニックを使用して、歪んだ長さの分布を処理します。
私たちの実験は、LeanProgressが進行量、したがって残りのステップ数を予測する際に75.1 \％の全体的な予測精度を達成することを示しています。
リプバーを使用して最良の検索フレームワークに統合すると、特に長い証拠の場合、41.2 \％のベースライン性能と比較して、Mathlib4の3.8 \％の改善が示されています。
これらの結果は、証明進行の予測が自動化されたインタラクティブ定理とインタラクティブな定理の両方を強化する方法を示しており、ユーザーが証明戦略についてより多くの情報に基づいた決定を下すことができるようにします。

要約(オリジナル)

Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucinations can be eliminated through rigorous verification, making theorem proving reliable. However, even with formal verification, LLMs still struggle with long proofs and complex mathematical formalizations. While Lean with LLMs offers valuable assistance with retrieving lemmas, generating tactics, or even complete proofs, it lacks a crucial capability: providing a sense of proof progress. This limitation particularly impacts the overall development efficiency in large formalization projects. We introduce LeanProgress, a method that predicts the progress in the proof. Training and evaluating our models made on a large corpus of Lean proofs from Lean Workbook Plus and Mathlib4 and how many steps remain to complete it, we employ data preprocessing and balancing techniques to handle the skewed distribution of proof lengths. Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1\% in predicting the amount of progress and, hence, the remaining number of steps. When integrated into a best-first search framework using Reprover, our method shows a 3.8\% improvement on Mathlib4 compared to baseline performances of 41.2\%, particularly for longer proofs. These results demonstrate how proof progress prediction can enhance both automated and interactive theorem proving, enabling users to make more informed decisions about proof strategies.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google