DafnyBench: A Benchmark for Formal Software Verification

要約

正式なソフトウェア検証のための機械学習システムのトレーニングと評価を行うための、この種の最大のベンチマークである DafnyBench を紹介します。
GPT-4 や Claude 3 などの LLM が、Dafny 形式検証エンジンが約 53,000 行のコードで 750 以上のプログラムを正常に検証するのに十分なヒントを自動生成する機能をテストします。
最良のモデルとプロンプト スキームは 68% の成功率を達成しました。エラー メッセージのフィードバックを使用して再試行するとこの率がどのように向上するか、また必要なコードとヒントの量に応じてどのように低下​​するかを定量化します。
LLM と検証技術の品質が向上するにつれて、DafnyBench によってこのベースラインからの急速な改善が可能になることを期待しています。

要約(オリジナル)

We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough hints for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and hints. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google