要約
証明指向のプログラムは、プログラムの正しさの証明と計算内容が混在している。しかし、F*のような言語では、証明の自動化のためにSMT（Satisfiability Modulo Theories）ソルバーが使用されているにもかかわらず、プログラミングと証明に関わる人間の労力は依然として相当なものである。 AIを使って証明指向プログラムの構築を自動化する研究に拍車をかけるべく、WindowsやLinuxからPythonやFirefoxに至るまで、実稼働システムで使用されているソフトウェアを含む、オープンソースのF*プログラムと証明の60万行のデータセットをキュレーションする。このデータセットには約32KのトップレベルのF*定義が含まれており、それぞれが型指向のプログラムと証明の合成問題を表している。F*型として表現された形式的な仕様から定義を生成するというものである。我々は、F*型に問い合わせを行い、解の候補の正しさをチェックするプログラム断片チェッカーを提供している。これは、再現可能なプログラムフラグメントチェッカーと組み合わされたSMT支援プログラム証明の最大のコーパスであると信じている。 このデータセットに基づき、F*におけるプログラムとその証明を合成するためにAIを使用することを調査し、有望な結果を得た。Phi-2やStarCoderのような細かく調整された小さな言語モデルの性能は、GPT-4のような大きな言語モデルよりもはるかに低い計算コストで優れている。また、様々な型ベースの検索補強技術を特定し、それらが性能を大幅に向上させることを発見した。詳細なエラー解析とケーススタディにより、モデルや手法の潜在的な長所と短所を明らかにし、今後の改善の方向性を提案する。
要約(オリジナル)
Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to automate proofs in languages such as F*. Seeking to spur research on using AI to automate the construction of proof-oriented programs, we curate a dataset of 600K lines of open-source F* programs and proofs, including software used in production systems ranging from Windows and Linux, to Python and Firefox. Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem — producing a definition given a formal specification expressed as an F* type. We provide a program-fragment checker that queries F* to check the correctness of candidate solutions. We believe this is the largest corpus of SMT-assisted program proofs coupled with a reproducible program-fragment checker. Grounded in this dataset, we investigate the use of AI to synthesize programs and their proofs in F*, with promising results. Our main finding in that the performance of fine-tuned smaller language models (such as Phi-2 or StarCoder) compare favorably with large language models (such as GPT-4), at a much lower computational cost. We also identify various type-based retrieval augmentation techniques and find that they boost performance significantly. With detailed error analysis and case studies, we identify potential strengths and weaknesses of models and techniques and suggest directions for future improvements.
arxiv情報
| 著者 | Saikat Chakraborty,Gabriel Ebner,Siddharth Bhat,Sarah Fakhoury,Sakina Fatima,Shuvendu Lahiri,Nikhil Swamy |
| 発行日 | 2024-09-03 17:11:31+00:00 |
| arxivサイト | arxiv_id(pdf) |