FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

要約

形式検証 (FV) は、進化する大規模言語モデル (LLM) による現在の新たなプログラム合成により重要性が高まっています。
しかし、現在の正式な検証は主に記号的な検証子や手作りのルールに頼っており、広範囲かつ柔軟な検証には限界があります。
一方、厳密な検証のもう 1 つの系統として、Isabelle などの自動定理証明用の形式言語は、包括的なルールと定理で維持されています。
この論文では、LLM を使用した対話型の形式検証環境である FVEL を提案します。
具体的には、FVEL は与えられた検証対象コードを Isabelle に変換し、LLM によるニューラル自動定理証明により検証を行います。
結合されたパラダイムは、Isabelle の厳密かつ豊富に定式化および組織化されたルールを活用しており、最先端の LLM の導入および調整にも便利です。
この目標を達成するために、大規模な FVELER3 を抽出します。
FVELER データセットには、Isabelle で定式化されたコードの依存関係と検証プロセスが含まれており、詳細な依存関係を持つ合計 758 の理論、29,125 の補題、および 200,646 の証明ステップが含まれています。
まず FVELER で LLM を微調整し、次に Code2Inv と SV-COMP で評価することにより、FVEL 環境で FVELER のベンチマークを行います。
結果は、SV-COMP において、FVELER で微調整された Llama3-8B を使用した FVEL は 17.39% (69 -> 81) 多くの問題を解決し、Mistral-7B は 12% (75 -> 84) 多くの問題を解決することを示しています。
そして証明ミスの割合も減ります。
プロジェクトページ: https://fveler.github.io/。

要約(オリジナル)

Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs). However, current formal verification mainly resorts to symbolic verifiers or hand-craft rules, resulting in limitations for extensive and flexible verification. On the other hand, formal languages for automated theorem proving, such as Isabelle, as another line of rigorous verification, are maintained with comprehensive rules and theorems. In this paper, we propose FVEL, an interactive Formal Verification Environment with LLMs. Specifically, FVEL transforms a given code to be verified into Isabelle, and then conducts verification via neural automated theorem proving with an LLM. The joined paradigm leverages the rigorous yet abundant formulated and organized rules in Isabelle and is also convenient for introducing and adjusting cutting-edge LLMs. To achieve this goal, we extract a large-scale FVELER3. The FVELER dataset includes code dependencies and verification processes that are formulated in Isabelle, containing 758 theories, 29,125 lemmas, and 200,646 proof steps in total with in-depth dependencies. We benchmark FVELER in the FVEL environment by first fine-tuning LLMs with FVELER and then evaluating them on Code2Inv and SV-COMP. The results show that FVEL with FVELER fine-tuned Llama3- 8B solves 17.39% (69 -> 81) more problems, and Mistral-7B 12% (75 -> 84) more problems in SV-COMP. And the proportion of proof errors is reduced. Project page: https://fveler.github.io/.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google