論文の概要: FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

• arxiv url: http://arxiv.org/abs/2406.14408v1
• Date: Thu, 20 Jun 2024 15:31:05 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-21 13:03:05.454825
• Title: FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
• Title（参考訳）: FVEL: 定理証明による大規模言語モデルを用いた対話型形式検証環境
• Authors: Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, Xiaodan Liang,
• Abstract要約: 大規模言語モデル(LLM)を用いた対話型形式検証環境FVELを提案する。 FVELは、検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。 FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップが含まれている。
• 参考スコア（独自算出の注目度）: 53.43068330741449
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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/.
• Abstract（参考訳）: 形式的検証(FV)は、進化する大規模言語モデル(LLM)による現在のプログラム合成において、重要性が増しているのを目撃している。 しかし、現在の公式な検証は主に記号的検証や手技規則に頼っており、その結果、広範囲かつ柔軟な検証の限界が生じる。 一方、イザベルのような自動定理証明のための形式言語は厳密な検証の別の行として、包括的な規則と定理で維持される。 本稿では,LLMを用いた対話型形式検証環境であるFVELを提案する。 具体的には、FVELは検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。 結合されたパラダイムは、イザベルの厳密な定式化と組織化された規則を活用し、最先端のLCMの導入と調整にも便利である。 この目的を達成するために、我々は大規模なFVELER3を抽出する。 FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップと詳細な依存関係が含まれている。 まずFVELERを用いてFVELERを微調整し,それをCode2InvおよびSV-COMP上で評価することにより,FVEL環境におけるFVELERのベンチマークを行う。 その結果, FVELERで微調整したLlama3-8Bでは17.39% (69 ->81) の問題を解き, Mistral-7Bでは12% (75 ->84) の問題をSV-COMPで解いた。 そして、証明エラーの割合は減少する。 プロジェクトページ: https://fveler.github.io/.com

関連論文リスト

• Open-domain Implicit Format Control for Large Language Model Generation [52.83173553689678]
  大規模言語モデル(LLM)における制御生成のための新しいフレームワークを提案する。 本研究では、LLMがオープンドメイン、ワンショット制約に従う能力と、サンプル回答の形式を再現する能力について検討する。 また、出力品質を劣化させることなく、LLMのオープンドメインフォーマット制御を強化する教師付き微調整のためのデータセット収集手法を開発した。
  論文  参考訳（メタデータ） (2024-08-08T11:51:45Z)
• DARG: Dynamic Evaluation of Large Language Models via Adaptive Reasoning Graph [70.79413606968814]
  本稿では,適応推論グラフ展開(DARG)によるLCMの動的評価を導入し,複雑性と多様性を制御した現在のベンチマークを動的に拡張する。 具体的には、まず現在のベンチマークでデータポイントの推論グラフを抽出し、それから推論グラフを摂動させて新しいテストデータを生成する。 このような新しく生成されたテストサンプルは、元のベンチマークと同様の言語的多様性を維持しながら、複雑さのレベルが異なる可能性がある。
  論文  参考訳（メタデータ） (2024-06-25T04:27:53Z)
• CaLM: Contrasting Large and Small Language Models to Verify Grounded Generation [76.31621715032558]
  グラウンデッドジェネレーションは、言語モデル(LM)に、より信頼性が高く説明可能な応答を生成する能力を持たせることを目的としている。 本稿では,新しい検証フレームワークであるCaLMを紹介する。 我々のフレームワークは、より少ないパラメトリックメモリに依存する小さなLMを有効活用し、より大きなLMの出力を検証する。
  論文  参考訳（メタデータ） (2024-06-08T06:04:55Z)
• CheckEmbed: Effective Verification of LLM Solutions to Open-Ended Tasks [15.60762281287532]
  大きな言語モデル(LLM)は様々なドメインに革命をもたらしていますが、その答えを検証することは大きな課題です。 本研究では,精度が高く,スケーラブルで,シンプルなLCM検証手法であるCheckEmbedを提案する。 CheckEmbedは、GPT Text Embedding Largeのようなモデルで得られた回答レベルの埋め込みを比較。
  論文  参考訳（メタデータ） (2024-06-04T17:42:21Z)
• LLMDFA: Analyzing Dataflow in Code with Large Language Models [8.92611389987991]
  本稿では,コンパイル不要でカスタマイズ可能なデータフロー解析フレームワークLLMDFAを提案する。 問題をいくつかのサブタスクに分解し、一連の新しい戦略を導入する。 LLMDFAは平均87.10%の精度と80.77%のリコールを達成し、F1スコアを最大0.35に向上させた。
  論文  参考訳（メタデータ） (2024-02-16T15:21:35Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• Hint-enhanced In-Context Learning wakes Large Language Models up for knowledge-intensive tasks [54.153914606302486]
  大規模言語モデル(LLM)の規模拡大に伴い、インコンテキスト学習(ICL)能力が出現した。 我々は、オープンドメイン質問応答におけるICLのパワーを探るため、Hint-enhanced In-Context Learning(HICL)と呼ばれる新しいパラダイムを提案する。
  論文  参考訳（メタデータ） (2023-11-03T14:39:20Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。 思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。 また,LLMにも同様な自己検証能力があることを示す。
  論文  参考訳（メタデータ） (2022-12-19T15:51:52Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。