要約
人間は、高度な論理的推論と問題固有の洞察に依存して定理を証明します。証明アシスタントは、人間の数学的推論に類似した形式を提供し、定理を高階論理で表現し、証明を高レベルの戦術として表します。しかし、人間の専門家が証明アシスタントに入力する戦術を手動で構築する必要があります。本稿では、機械学習を使用して証明アシスタントとの相互作用を自動化する問題について研究しています。私たちは、Coq証明アシスタントで開発された123のプロジェクトから71,000件の人間が書いた証明を集めた大規模なデータセットおよび学習環境であるCoqGymを開発しました。また、抽象構文木（AST）の形でプログラムとして戦術を生成する深層学習ベースのモデルであるASTacticを開発しました。実験結果によると、CoqGymで訓練されたASTacticは効果的な戦術を生成でき、自動方法では以前に証明できなかった新しい定理を証明するために使用できることが示されました。コードは https://github.com/princeton-vl/CoqGym で利用可能です。