Lyra: Orchestrating Dual Correction in Automated Theorem Proving

要約

大規模言語モデル (LLM) は、形式定理証明の分野における探索のための興味深い手段を提供します。
それにもかかわらず、特に幻覚の軽減や証明者エラー メッセージによる洗練に関して、その可能性を最大限に発揮できるかどうかは、まだ十分に研究されていない領域です。
現場での LLM の有効性を高めるために、ツール修正 (TC) と推測修正 (CC) という 2 つの異なる修正メカニズムを採用する新しいフレームワークである Lyra を導入します。
正式な証明の後処理でツール修正を実装するには、事前の知識を活用して、事前に定義された証明者ツール (Sledgehammer など) を利用して、誤ったツールの置き換えをガイドします。
ツール修正は幻覚の軽減に大きく貢献し、それによって証明の全体的な精度が向上します。
さらに、証明者と対話して証明者のエラー メッセージを使用して形式的な証明予想を改良するように設計されたエラー フィードバック メカニズムである予想修正を導入します。
以前の改良フレームワークと比較して、提案された推測修正は命令を使用して生成を改良しますが、ペアになった (生成、エラー、および改良) プロンプトを収集しません。
私たちの手法は、miniF2F 検証 (48.0% -> 55.3%) とテスト (45.5% -> 51.2%) の両方で最先端 (SOTA) パフォーマンスを達成しました。
Lyra によって解決された 3 つの IMO 問題も紹介します。
私たちは、ツール補正 (幻覚軽減のための後プロセス) と推測補正 (環境との相互作用からのサブゴール調整) が、この分野の将来の研究に有望な手段を提供できると信じています。

要約(オリジナル)

Large Language Models (LLMs) present an intriguing avenue for exploration in the field of formal theorem proving. Nevertheless, their full potential, particularly concerning the mitigation of hallucinations and refinement through prover error messages, remains an area that has yet to be thoroughly investigated. To enhance the effectiveness of LLMs in the field, we introduce the Lyra, a new framework that employs two distinct correction mechanisms: Tool Correction (TC) and Conjecture Correction (CC). To implement Tool Correction in the post-processing of formal proofs, we leverage prior knowledge to utilize predefined prover tools (e.g., Sledgehammer) for guiding the replacement of incorrect tools. Tool Correction significantly contributes to mitigating hallucinations, thereby improving the overall accuracy of the proof. In addition, we introduce Conjecture Correction, an error feedback mechanism designed to interact with prover to refine formal proof conjectures with prover error messages. Compared to the previous refinement framework, the proposed Conjecture Correction refines generation with instruction but does not collect paired (generation, error & refinement) prompts. Our method has achieved state-of-the-art (SOTA) performance on both miniF2F validation (48.0% -> 55.3%) and test (45.5% -> 51.2%). We also present 3 IMO problems solved by Lyra. We believe Tool Correction (post-process for hallucination mitigation) and Conjecture Correction (subgoal adjustment from interaction with environment) could provide a promising avenue for future research in this field.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google