文脈学習エージェントによる形式的定理証明

LeanやCoqなどの環境における形式的定理証明のための、文脈内学習（in-context learning）型エージェントを提案する。現在の最先端モデルは、環境固有の証明データ上でファインチューニングされている。これに対して、本研究で提案する手法であるCOPRAは、状態を保持するバックトラッキング探索の内部から、高容量かつ汎用的な大規模言語モデル（GPT-4）にタクティクの適用を繰り返し提案させる。提案されたタクティクは、下位の証明環境で実行され、その実行結果をもとに、次のモデルクエリ用のプロンプトが構築される。この際、探索履歴から選択された情報および外部データベースから取得した補題が、プロンプトに組み込まれる。COPRAの実装は、Lean向けのminiF2FベンチマークおよびCompCertプロジェクトから抽出されたCoqタスクセットにおいて評価された。これらのベンチマークにおいて、COPRAはGPT-4のフェイショット（few-shot）呼び出しを大幅に上回る性能を示した。また、ファインチューニングに基づくアプローチと比較しても優れた結果を示し、Leanにおける最先端のファインチューニング手法であるReProverを、pass@1指標において上回った。本研究のコードおよびデータは、https://github.com/trishullab/copra にて公開されている。