Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

要約

Coq などの証明アシスタントを使用した形式的検証により、高品質のソフトウェアの作成が可能になります。
ただし、検証プロセスには、かなりの専門知識と証明を書くための手作業が必要です。
最近の研究では、機械学習と大規模言語モデル (LLM) を使用した証明合成の自動化が検討されています。
この研究は、補題や定義などの関連する前提を特定することが統合に役立つことを示しました。
Rango は、Coq 用の完全に自動化された証明合成ツールであり、現在のプロジェクトから関連する前提と同様の証明を自動的に識別し、合成中にそれらを使用します。
Rango は証明のすべてのステップで検索拡張を使用して、微調整された LLM のコンテキストにどの証明と前提を含めるかを自動的に決定します。
このようにして、ランゴはプロジェクトと証明の進化する状態に適応します。
私たちは、GitHub から 2,226 個のオープンソース Coq プロジェクトと 196,929 個の定理を含む新しいデータセット CoqStoq を作成します。これには、トレーニング データと、適切に管理されたプロジェクトの厳選された評価ベンチマークの両方が含まれます。
このベンチマークでは、Rango は定理の 32.0% の証明を合成します。これは、以前の最先端ツールである Tactician よりも 29% 多い定理です。
私たちの評価では、Rango がコンテキストに関連する証明を追加すると、証明される定理の数が 47% 増加することもわかりました。

要約(オリジナル)

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google