SMT支援型証明指向プログラミングのための神経合成に向けて

証明指向プログラムは、計算コンテンツとプログラムの正しさの証明を組み合わせています。しかし、F*などの言語で証明を自動化するためにSatisfiability Modulo Theories (SMT) ソルバーを使用しても、プログラミングと証明に関わる人間の努力は依然として大きいです。AIを使用して証明指向プログラムの構築を自動化する研究を促進することを目指して、私たちは600K行のオープンソースF*プログラムと証明のデータセットをキュレーションしました。これには、WindowsやLinuxからPythonやFirefoxに至るまで、プロダクションシステムで使用されるソフトウェアが含まれています。私たちのデータセットには、各々が型指向プログラムと証明合成問題を表す約32KのトップレベルF*定義が含まれており、F*型として表現された形式的仕様に基づいて定義を生成します。候補解の正確性をチェックするためにF*にクエリを送信するプログラム断片チェッカーを提供しています。これは、SMT支援プログラム証明の最大のコーパスであり、再現可能なプログラム断片チェッカーと組み合わさっています。このデータセットに基づいて、AIを使用してF*でプログラムとその証明を合成することを調査し、有望な結果を得ています。私たちの主な発見は、微調整された小型言語モデル（Phi-2やStarCoderなど）の性能が、大型言語モデル（GPT-4など）と比較して有利であり、はるかに低い計算コストであるということです。また、さまざまなタイプベースの検索強化技術を特定し、それによって性能が顕著に向上することを発見しました。詳細なエラー分析と事例研究を通じて、モデルや技術の潜在的な強みと弱みを特定し、今後の改善の方向性を提案します。