論文の概要: Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification

• arxiv url: http://arxiv.org/abs/2404.00762v2
• Date: Tue, 2 Apr 2024 05:44:02 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-04 01:51:24.324647
• Title: Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
• Title（参考訳）: 静的解析とプログラム検証を用いた大規模言語モデルによるプログラム仕様生成の自動化
• Authors: Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, Cong Tian,
• Abstract要約: AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
• 参考スコア（独自算出の注目度）: 15.686651364655958
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems. Yet, constructing specifications for the full proof relies on domain expertise and non-trivial manpower. In view of such needs, an automated approach for specification synthesis is desired. While existing automated approaches are limited in their versatility, i.e., they either focus only on synthesizing loop invariants for numerical programs, or are tailored for specific types of programs or invariants. Programs involving multiple complicated data types (e.g., arrays, pointers) and code structures (e.g., nested loops, function calls) are often beyond their capabilities. To help bridge this gap, we present AutoSpec, an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It is driven by static analysis and program verification, and is empowered by large language models (LLMs). AutoSpec addresses the practical challenges in three ways: (1) driving \name by static analysis and program verification, LLMs serve as generators to generate candidate specifications, (2) programs are decomposed to direct the attention of LLMs, and (3) candidate specifications are validated in each round to avoid error accumulation during the interaction with LLMs. In this way, AutoSpec can incrementally and iteratively generate satisfiable and adequate specifications. The evaluation shows its effectiveness and usefulness, as it outperforms existing works by successfully verifying 79% of programs through automatic specification synthesis, a significant improvement of 1.592x. It can also be successfully applied to verify the programs in a real-world X509-parser project.
• Abstract（参考訳）: 形式的検証は、ソフトウェアシステムの正確性と信頼性を保証するための厳密で体系的なアプローチを提供する。 しかし、完全な証明のための仕様の構築は、ドメインの専門知識と非自明なマンパワーに依存します。 このようなニーズを考慮すると、仕様合成のための自動アプローチが望まれる。 既存の自動化アプローチは汎用性に制限があるが、例えば、数値プログラムのループ不変量の合成にのみ焦点をあてるか、特定の種類のプログラムや不変量の調整を行う。 複数の複雑なデータ型(例:配列、ポインタ)とコード構造(例:ネストループ、関数呼び出し)を含むプログラムは、その能力を超えることが多い。 このギャップを埋めるために,自動プログラム検証のための仕様を自動生成するAutoSpecを提案する。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 静的解析とプログラム検証によって駆動され、大きな言語モデル(LLM)によって強化される。 AutoSpec は,(1) 静的解析とプログラム検証により \name を駆動し,(2) 候補仕様を生成するジェネレータとして機能し,(2) プログラムを分解して LLM の注意を向け,(3) 候補仕様を各ラウンドで検証し,LLM との相互作用におけるエラーの蓄積を回避する。 このように、AutoSpecは段階的に、かつ反復的に、満足できる適切な仕様を生成できます。 この評価は, 自動仕様合成によるプログラムの79%の検証に成功し, 1.592倍の大幅な改善を達成し, 既存の作業より優れていることを示す。 また、現実世界のX509パーサプロジェクトにおけるプログラムの検証にも成功している。

関連論文リスト

• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。 SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
  論文  参考訳（メタデータ） (2024-01-16T20:13:50Z)
• Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
  実世界の産業レベルのマイクロカーネルであるseL4をベースとした,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。 GPT-3.5-turbo や GPT-4 のような先進的な大規模言語モデル (LLM) による実験結果から, 自動証明生成領域における LLM の機能を強調した。
  論文  参考訳（メタデータ） (2024-01-15T13:08:38Z)
• Fine-Tuning Language Models Using Formal Methods Feedback [53.24085794087253]
  我々は、自律システムにおけるアプリケーションのための、微調整済み言語モデルに対して、完全に自動化されたアプローチを提案する。 本手法は,自然言語タスク記述による事前学習モデルから自動制御器を合成する。 その結果、コントローラが満たした仕様の割合が60%から90%に改善したことが示唆された。
  論文  参考訳（メタデータ） (2023-10-27T16:24:24Z)
• Lemur: Integrating Large Language Models in Automated Program Verification [10.221822902660458]
  自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。 本稿では,音声自動検証手法として計算をインスタンス化し,一連の合成および競合ベンチマークの実践的改善を実証する。
  論文  参考訳（メタデータ） (2023-10-07T16:44:53Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Synthesis of Mathematical programs from Natural Language Specifications [0.0]
  様々なビジネス領域で遭遇する決定問題は、数学的なプログラム、すなわち最適化問題としてモデル化することができる。 このようなモデリングを行うプロセスは、しばしばオペレーション研究や高度なアルゴリズムで訓練された専門家の関与を必要とする。 本研究は,データ拡張とビーム後処理によるCodeT5の有効性を評価する。 これらの拡張により、CodeT5baseは実行精度0.73となり、ChatGPTでは0.41、Codexでは0.36より大幅に向上した。
  論文  参考訳（メタデータ） (2023-03-30T06:10:00Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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