定理証明における大規模言語モデルの共操縦者としての進展

定理証明は大規模言語モデル（LLM）にとって重要な課題です。正式な証明はLeanなどの証明補助ツールによって厳密にチェックされ、幻覚の余地がありません。既存のLLMベースの証明器は、人間の介入なしに完全自律モードで定理を証明しようとします。このモードでは、人間の洞察が重要である新しい挑戦的な定理に苦しんでいます。本論文では、定理証明を支援する共操縦者としてのLLMを探ります。LLM推論をLeanで実行するためのフレームワークであるLean Copilotを導入します。これにより、プログラマーはLeanユーザーのワークフローにシームレスに統合されたさまざまなLLMベースの証明自動化ツールを構築できます。Lean Copilotを使用することで、LLMを用いた証明ステップの提案（戦術提案）、中間証明目標の完了（証明検索）、および関連する前提の選択（前提選択）を行うツールを構築します。ユーザーは、ローカル（GPUありまたはなし）またはクラウド上で実行される自前のモデルを使用するか、学習済みモデルを使用できます。実験結果は、既存のルールベースの証明自動化と比較して、人類を支援し、定理証明プロセスを自動化する方法の効果を示しています。さらなる研究を促進するために、全てのコードを許可されたMITライセンスの下でオープンソース化します。