論文の概要: 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 15:10:31.019377
• 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:
• 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で生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。 仕様が検証されたら、冗長性を含む。 パフォーマンスを改善するために今後の方向性について議論する。

関連論文リスト

• A Systematic Approach for Assessing Large Language Models' Test Case Generation Capability [0.8287206589886879]
  大規模言語モデル (LLM) を評価するために,制御フロー構造と可変利用構成 (GBCV) から生成したベンチマークを提案する。 基本的な制御フロー構造と変数使用量を活用することで、GBCVは、単純なプログラムから複雑なプログラムの範囲を作成する柔軟なフレームワークを提供する。 以上の結果から,GPT-4oは複雑なプログラム構造において優れた性能を示し,全てのモデルが単純な条件下で境界値を効果的に検出するが,算術計算では問題に直面することが示唆された。
  論文  参考訳（メタデータ） (2025-02-05T03:51:44Z)
• 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を紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• 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)
• 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)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  ソフトウェア自然性仮説(Software Naturalness hypothesis)は、自然言語処理で使用されるのと同じ手法でプログラミング言語を理解することができると主張している。 この仮説は,事前学習されたトランスフォーマーベース言語モデルを用いて,コード解析タスクを実行することによって検討する。
  論文  参考訳（メタデータ） (2020-06-22T21:56:14Z)

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

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