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

• arxiv url: http://arxiv.org/abs/2411.02318v2
• Date: Tue, 05 Nov 2024 07:13:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-06 15:01:48.202015
• Title: Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
• Title（参考訳）: VeriFastにおける検証可能な仕様を生成するための大規模言語モデルの有効性の評価
• Authors: Marilyn Rego, Wen Fan, Xin Hu, Sanya Dod, Zhaorui Ni, Danning Xie, Jenna DiVincenzo, Lin Tan,
• Abstract要約: 大規模言語モデル(LLM)は、多くのソフトウェアエンジニアリング活動において有望であることを示している。 本稿では,分離論理に基づく仕様生成におけるOpenAIのGPTモデルの有効性について検討する。
• 参考スコア（独自算出の注目度）: 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 the effectiveness of large language models (LLMs), specifically OpenAI's GPT models, in generating fully correct specifications based on separation logic for static verification of human-written programs in VeriFast. Our first experiment employed traditional prompt engineering and the second used Chain-of-Thought (CoT) Prompting to identify and address common errors generated across the GPT models. The results indicate that GPT models can successfully generate specifications for verifying heap manipulating code with VeriFast. Furthermore, while CoT prompting significantly reduces syntax errors generated by the GPT models, it does not greatly improve verification error rates compared to prompt engineering.
• Abstract（参考訳）: 静的検証はソフトウェアの品質を高めるための強力な方法だが、人的労力とリソースを必要とする。 これは、オーナシップロジックを使用したヒープ操作プログラムの理由となる静的検証に特に当てはまる。 LLMは、コード生成、テスト生成、定理証明器の証明生成、静的検証器の仕様生成など、多くのソフトウェアエンジニアリング活動において有望であることを示した。 しかし、以前の研究では、LLMが分離ロジックのようなオーナシップロジックに基づいた仕様生成をどの程度うまく実行できるかは明らかにされていない。 このギャップに対処するため,本研究では,大言語モデル,特に OpenAI の GPT モデルの有効性について検討する。 最初の実験では、従来のプロンプトエンジニアリングと、2つ目の実験では、GPTモデル全体で発生する一般的なエラーを特定し、対処するために、Chain-of-Thought (CoT) Promptingを使用しました。 その結果、GPTモデルはVeriFastでヒープ操作コードを検証するための仕様をうまく生成できることが示唆された。 さらに、CoTプロンプトはGPTモデルによって生成される構文エラーを著しく低減するが、プロンプトエンジニアリングに比べて検証エラー率を大幅に改善するわけではない。

関連論文リスト

• 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)
• 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)
• 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)

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

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