論文の概要: FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
- arxiv url: http://arxiv.org/abs/2502.15217v1
- Date: Fri, 21 Feb 2025 05:20:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-02-24 16:11:49.799503
- Title: FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
- Title(参考訳): FormalSpecCpp: LLMを使って作成されたC++形式仕様のデータセット
- Authors: Madhurima Chakraborty, Peter Pirkelbauer, Qing Yi,
- Abstract要約: FormalSpecCppは、C++プログラムの正式な仕様を検証するための標準ベンチマークのギャップを埋めるために設計されたデータセットである。
仕様推論ツールの評価と、生成された仕様の正確性をテストするための構造化ベンチマークを提供する。
- 参考スコア(独自算出の注目度): 0.3277163122167433
- License:
- Abstract: FormalSpecCpp is a dataset designed to fill the gap in standardized benchmarks for verifying formal specifications in C++ programs. To the best of our knowledge, this is the first comprehensive collection of C++ programs with well-defined preconditions and postconditions. It provides a structured benchmark for evaluating specification inference tools and testing theaccuracy of generated specifications. Researchers and developers can use this dataset to benchmark specification inference tools,fine-tune Large Language Models (LLMs) for automated specification generation, and analyze the role of formal specifications in improving program verification and automated testing. By making this dataset publicly available, we aim to advance research in program verification, specification inference, and AI-assisted software development. The dataset and the code are available at https://github.com/MadhuNimmo/FormalSpecCpp.
- Abstract(参考訳): FormalSpecCppは、C++プログラムの正式な仕様を検証するための標準ベンチマークのギャップを埋めるために設計されたデータセットである。
私たちの知る限りでは、これは、明確に定義された前提条件と後条件を持つC++プログラムの包括的なコレクションとしては初めてのものです。
仕様推論ツールの評価と、生成された仕様の正確性をテストするための構造化ベンチマークを提供する。
研究者や開発者はこのデータセットを使用して、仕様推論ツールのベンチマーク、自動仕様生成のためのファインチューンな大規模言語モデル(LLM)、プログラム検証と自動テストの改善における正式な仕様の役割を分析することができる。
このデータセットを公開することにより、プログラム検証、仕様推論、AI支援ソフトウェア開発の研究を進めることを目指している。
データセットとコードはhttps://github.com/MadhuNimmo/FormalSpecCppで公開されている。
関連論文リスト
- CPP-UT-Bench: Can LLMs Write Complex Unit Tests in C++? [0.4915744683251149]
CPP-UT-Benchは、大規模言語モデル(LLM)のC++単体テスト生成能力を測定するベンチマークデータセットである。
データセットには2,653のコードと14のオープンソースC++から引き出されたユニットテストペアが含まれている。
論文 参考訳(メタデータ) (2024-12-03T18:35:24Z) - Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。
Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
論文 参考訳(メタデータ) (2024-10-02T09:11:10Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳(メタデータ) (2024-06-14T06:52:08Z) - Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。
仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。
実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文 参考訳(メタデータ) (2024-03-31T18:15:49Z) - Large Language Models to Generate System-Level Test Programs Targeting Non-functional Properties [3.3305233186101226]
本稿では,テストプログラムを生成するためのLarge Language Models (LLM)を提案する。
我々は、DUTの非機能特性を最適化するために、事前訓練されたLLMがテストプログラム生成でどのように機能するかを、一目で見てみる。
論文 参考訳(メタデータ) (2024-03-15T08:01:02Z) - SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。
SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
論文 参考訳(メタデータ) (2024-01-16T20:13:50Z) - Leveraging Large Language Models to Improve REST API Testing [51.284096009803406]
RESTGPTはAPI仕様を入力として、機械解釈可能なルールを抽出し、仕様内の自然言語記述からサンプルパラメータ値を生成する。
評価の結果、RESTGPTはルール抽出と値生成の両方において既存の技術よりも優れています。
論文 参考訳(メタデータ) (2023-12-01T19:53:23Z) - Instruct and Extract: Instruction Tuning for On-Demand Information
Extraction [86.29491354355356]
On-Demand Information extractは、現実世界のユーザのパーソナライズされた要求を満たすことを目的としている。
InstructIEというベンチマークを、自動生成したトレーニングデータと、人手による注釈付きテストセットの両方を含む形で提示する。
InstructIE 上に構築した On-Demand Information Extractor, ODIE をさらに発展させる。
論文 参考訳(メタデータ) (2023-10-24T17:54:25Z) - Python Code Generation by Asking Clarification Questions [57.63906360576212]
本稿では,この課題に対して,より斬新で現実的なセットアップを導入する。
我々は、自然言語記述の過小評価は、明確化を問うことで解決できると仮定する。
我々は、生成した合成明確化質問と回答を含む自然言語記述とコードのペアを含む、CodeClarQAという新しいデータセットを収集し、導入する。
論文 参考訳(メタデータ) (2022-12-19T22:08:36Z) - CodeExp: Explanatory Code Document Generation [94.43677536210465]
既存のコード・トゥ・テキスト生成モデルは、コードの高レベルな要約のみを生成する。
我々は、コードのための高品質な説明記述の基準を特定するために、人間の研究を行う。
タスクのための多段階微調整戦略とベースラインモデルを提案する。
論文 参考訳(メタデータ) (2022-11-25T18:05:44Z) - GEMv2: Multilingual NLG Benchmarking in a Single Line of Code [161.1761414080574]
Generation, Evaluation, and Metrics Benchmarkは、データセット、モデル、メトリック開発者のためのモジュラーインフラストラクチャを提供する。
GEMv2は51言語で40のドキュメントデータセットをサポートする。
すべてのデータセットのモデルはオンラインで評価でき、インタラクティブなデータカード作成とレンダリングツールによって、生きたベンチマークに新しいデータセットを簡単に追加できます。
論文 参考訳(メタデータ) (2022-06-22T17:52:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。