ドラフト、スケッチ、そして証明：非形式的証明による形式的定理証明者の誘導

既存の数学的証明を形式化するプロセスは、かつてないほど困難である。長年にわたり自動化および証明支援ツールに関する研究が進められてきたが、形式的証明の作成は依然として重労働であり、少数の専門家にしかアクセスできない状況が続いている。これまでの形式化の自動化に関する研究は、強力な探索アルゴリズムの開発に注力してきたが、利用可能な非形式的証明を活用する試みは行われてこなかった。本研究では、非形式的証明を形式的証明のスケッチに変換し、そのスケッチをもとに自動証明器の探索をより容易な部分問題へと導く「ドラフト、スケッチ、証明（Draft, Sketch, and Prove; DSP）」という手法を提案する。本研究では、非形式的証明が人間によって記述された場合と、言語モデルによって生成された場合の2つの設定を検討した。実験およびアブレーション研究の結果、大規模言語モデルが非形式的証明と同一の推論手順を踏む良好な構造を持つ形式的スケッチを生成できることを示した。このようなスケッチを用いて自動証明器をガイドすることで、数学コンペティション問題の集合において、証明成功率が20.9％から39.3％へと向上した。