要約
基礎的検証により、プログラマーはさまざまな重要な分野において高い信頼性が実証されたソフトウェアを構築できるようになる。しかし、基礎的検証を施したソフトウェアを生産するコストは、ほとんどのプロジェクトにとって依然として過剰に高く、高度に訓練された専門家による膨大な手作業を要するためである。本論文では、機械学習技術を用いた証明探索システム「Proverbot9001」を提案する。このシステムは、対話型定理証明器（interactive theorem provers）におけるソフトウェア正当性の証明を生成することを目的としている。我々は、実用的な大規模証明プロジェクトである「CompCert検証済みCコンパイラ」から得られた証明義務（proof obligations）に対してProverbot9001を適用し、従来手動で行われていた証明の自動化が効果的に実現できることを示した。特に、ソルバベースのツールと組み合わせた場合、テストデータセットにおける定理記述の27.5％について自動的に証明を生成できた。さらに、追加のソルバを用いない状況でも、Coqにおける証明生成に関する従来の最先端機械学習モデルと比較して、証明完了率が4倍の向上を達成した。