ライラ：自動定理証明における二重補正のオーケストレーション

大規模言語モデル（LLMs）は、形式的定理証明の分野において興味深い探求の対象である。しかし、特に幻覚（hallucination）の低減や証明器からのエラーメッセージを用いた精緻化に関するその潜在能力は、まだ十分に調査されていない。本研究では、LLMsの効果を向上させるため、二つの異なる補正機構を採用する新規フレームワーク「Lyra」を提案する。これらの機構は、ツール補正（Tool Correction, TC）と仮説補正（Conjecture Correction, CC）である。証明の後処理においてツール補正を実装する際、事前知識を活用し、既定の証明器ツール（例：Sledgehammer）を用いて誤ったツールの置換を誘導する。このツール補正は幻覚の低減に顕著な貢献をし、証明全体の正確性を向上させる。さらに、証明器からのエラーメッセージを活用して、形式的証明の仮説を精緻化するための誤差フィードバック機構として、仮説補正を導入した。従来の精緻化フレームワークと比較して、本研究で提案する仮説補正は、指示（instruction）に基づいて生成を精緻化するが、対応する（生成、エラー、修正）プロンプトのペアを収集しない点が特徴である。本手法は、miniF2Fの検証データセット（48.0% → 55.3%）およびテストデータセット（45.5% → 51.2%）において、最先端（SOTA）の性能を達成した。また、Lyraによって解決された国際数学オリンピック（IMO）問題が3問存在することも示した。我々は、ツール補正（幻覚の低減のための後処理）および仮説補正（環境とのインタラクションによる部分目標の調整）が、本分野における今後の研究にとって有望な道筋を提供するものと確信している。