論文の概要: Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast

• arxiv url: http://arxiv.org/abs/2411.02318v3
• Date: Fri, 03 Jan 2025 02:19:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-06 14:47:14.98926
• Title: Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
• Title（参考訳）: VeriFastにおける検証可能な仕様を生成するための大規模言語モデルの有効性の評価
• Authors: Wen Fan, Marilyn Rego, Xin Hu, Sanya Dod, Zhaorui Ni, Danning Xie, Jenna DiVincenzo, Lin Tan,
• Abstract要約: 本稿では,VeriFast で検証可能な C プログラムの仕様作成における OpenAI の GPT-4o モデルの有効性について検討する。 以上の結果から,GPT-4oで生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。
• 参考スコア（独自算出の注目度）: 5.019791860882564
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Static verification is a powerful method for enhancing software quality, but it demands significant human labor and resources. This is particularly true of static verifiers that reason about heap manipulating programs using an ownership logic. LLMs have shown promise in a number of software engineering activities, including code generation, test generation, proof generation for theorem provers, and specification generation for static verifiers. However, prior work has not explored how well LLMs can perform specification generation for specifications based in an ownership logic, such as separation logic. To address this gap, this paper explores OpenAI's GPT-4o model's effectiveness in generating specifications on C programs that are verifiable with VeriFast, a separation logic based static verifier. Our experiment employs three different types of user inputs as well as basic and Chain-of-Thought (CoT) prompting to assess GPT's capabilities. Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable. When the specifications are verifiable they contain redundancies. Future directions are discussed to improve the performance.
• Abstract（参考訳）: 静的検証はソフトウェアの品質を高めるための強力な方法だが、人的労力とリソースを必要とする。 これは、オーナシップロジックを使用したヒープ操作プログラムの理由となる静的検証に特に当てはまる。 LLMは、コード生成、テスト生成、定理証明器の証明生成、静的検証器の仕様生成など、多くのソフトウェアエンジニアリング活動において有望であることを示した。 しかし、以前の研究では、LLMが分離ロジックのようなオーナシップロジックに基づいた仕様生成をどの程度うまく実行できるかは明らかにされていない。 このギャップに対処するために,分離論理に基づく静的検証器であるVeriFastで検証可能なCプログラムの仕様を生成する上で,OpenAIのGPT-4oモデルの有効性について検討する。 実験では,3種類のユーザ入力と基本およびチェーン・オブ・ソート(CoT)を用いて,GPTの能力を評価する。 以上の結果から,GPT-4oで生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。 仕様が検証されたら、冗長性を含む。 パフォーマンスを改善するために今後の方向性について議論する。

関連論文リスト

• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.4779196219827508]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• Scoring Verifiers: Evaluating Synthetic Verification for Code and Reasoning [59.25951947621526]
  本稿では,既存の符号化ベンチマークをスコアとランキングデータセットに変換して,合成検証の有効性を評価する手法を提案する。 我々は4つの新しいベンチマーク(HE-R, HE-R+, MBPP-R, MBPP-R+)を公表し, 標準, 推論, 報酬に基づくLCMを用いて合成検証手法を解析した。 実験の結果, 推論はテストケースの生成を著しく改善し, テストケースのスケーリングによって検証精度が向上することがわかった。
  論文  参考訳（メタデータ） (2025-02-19T15:32:11Z)
• Automated Refactoring of Non-Idiomatic Python Code: A Differentiated Replication with LLMs [54.309127753635366]
  本研究は, GPT-4の有効性について検討し, 慣用行動の推奨と示唆について検討した。 この結果から,従来は複雑なコード解析に基づくレコメンデータの実装が求められていた,LCMの課題達成の可能性が浮き彫りになった。
  論文  参考訳（メタデータ） (2025-01-28T15:41:54Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Insights from Benchmarking Frontier Language Models on Web App Code Generation [1.7268889851975326]
  本稿では,WebApp1Kベンチマークによる16のフロンティア大言語モデル(LLM)の評価から得られた知見について述べる。 結果は、全てのモデルが類似した知識を持っているが、それらの性能は、それらが犯した誤りの頻度によって区別されることを示している。
  論文  参考訳（メタデータ） (2024-09-08T18:24:26Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  検証や報酬モデルはしばしば、大きな言語モデル(LLM)の推論性能を高めるために使われる。 本研究では,ユビキタスな次世代予測目標を用いて,検証とソリューション生成を併用したトレーニング検証手法を提案する。 GenRMは差別的, DPO 検証, LLM-as-a-Judge に優れていた。
  論文  参考訳（メタデータ） (2024-08-27T17:57:45Z)
• Understanding Defects in Generated Codes by Language Models [0.669087470775851]
  本研究では,大規模言語モデルによって生成されたコードスニペットの367の欠陥を分類,解析する。 エラーカテゴリは、LLMが頻繁に失敗する重要な領域を示し、目標とする改善の必要性を強調している。 本稿では,スクラッチパッド・プロンプト・プログラム・オブ・ソート・プロンプト・チェーン・オブ・ソート・プロンプト・チェーン・オブ・ソート・プロンプト・ストラクテッド・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・オブ・ソート・プロンプト・プロンプト・アンド・ストラクテッド・オブ・フォーンティング(Structued Chain-of-Thought Prompting)の5つの迅速な技術技術
  論文  参考訳（メタデータ） (2024-08-23T21:10:09Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。 AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
  論文  参考訳（メタデータ） (2024-06-26T14:47:28Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• Test-Case-Driven Programming Understanding in Large Language Models for Better Code Generation [15.166827643436346]
  muFiXは、大きな言語モデル(LLM)のコード生成性能を改善する新しいプロンプト技術である。 まず、テストケース分析を利用して仕様の理解を得、自己改善プロセスを可能にする。 muFiXはさらに、提供された理解と実際の理解の間のギャップを減らす方向に向けた仕様理解を修正している。
  論文  参考訳（メタデータ） (2023-09-28T02:58:07Z)
• How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
  大規模言語モデル(LLM)は多くのソフトウェア工学(SE)タスクにうまく適用されている。 ソフトウェアコメントやドキュメンテーションからソフトウェア仕様を生成するためのLCMの能力を評価するための、最初の実証的研究を行う。
  論文  参考訳（メタデータ） (2023-06-06T00:28:39Z)
• Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
  Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。 このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
  論文  参考訳（メタデータ） (2023-05-24T01:46:07Z)
• CodeRL: Mastering Code Generation through Pretrained Models and Deep Reinforcement Learning [92.36705236706678]
  CodeRLは、事前訓練されたLMと深層強化学習によるプログラム合成タスクのための新しいフレームワークである。 推論中、我々は重要なサンプリング戦略を持つ新しい生成手順を導入する。 モデルバックボーンについては,CodeT5のエンコーダデコーダアーキテクチャを拡張し,学習目標を拡張した。
  論文  参考訳（メタデータ） (2022-07-05T02:42:15Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  ソフトウェア自然性仮説(Software Naturalness hypothesis)は、自然言語処理で使用されるのと同じ手法でプログラミング言語を理解することができると主張している。 この仮説は,事前学習されたトランスフォーマーベース言語モデルを用いて,コード解析タスクを実行することによって検討する。
  論文  参考訳（メタデータ） (2020-06-22T21:56:14Z)

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

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