論文の概要: Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
- arxiv url: http://arxiv.org/abs/2602.04786v1
- Date: Wed, 04 Feb 2026 17:35:28 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-05 19:45:11.658056
- Title: Demonstrating ARG-V's Generation of Realistic Java Benchmarks for SV-COMP
- Title(参考訳): SV-COMPのためのARG-VによるリアルなJavaベンチマークのデモ
- Authors: Charles Moloney, Robert Dyer, Elena Sherman,
- Abstract要約: SV-COMPフォーマットでJava検証ベンチマークを自動的に生成するためのARG-Vツールの応用について述べる。
新たに生成された68の現実的なベンチマークセットにおいて、4つの主要なJava検証者は、既存のベンチマークスイートのパフォーマンスと比較して、正確さとリコールを減少させます。
- 参考スコア(独自算出の注目度): 2.440576202925247
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: The SV-COMP competition provides a state-of-the-art platform for evaluating software verification tools on a standardized set of verification tasks. Consequently, verifier development outcomes are influenced by the composition of program benchmarks included in SV-COMP. When expanding this benchmark corpus, it is crucial to consider whether newly added programs cause verifiers to exhibit behavior distinct from that observed on existing benchmarks. Doing so helps mitigate external threats to the validity of the competition's results. In this paper, we present the application of the ARG-V tool for automatically generating Java verification benchmarks in the SV-COMP format. We demonstrate that, on a newly generated set of 68 realistic benchmarks, all four leading Java verifiers decrease in accuracy and recall compared to their performance on the existing benchmark suite. These findings highlight the potential of ARG-V to enhance the comprehensiveness and realism of verification tool evaluation, while also providing a roadmap for verifier developers aiming to improve their tools' applicability to real-world software.
- Abstract(参考訳): SV-COMPコンペティションは、標準化された検証タスクセット上でソフトウェア検証ツールを評価するための最先端のプラットフォームを提供する。
その結果、SV-COMPに含まれるプログラムベンチマークの構成に影響される。
このベンチマークコーパスを拡張する際には、新たに追加されたプログラムが検証者に対して、既存のベンチマークで観測されたものと異なる振る舞いを示すかどうかを検討することが重要である。
そうすることで、競争結果の妥当性に対する外部からの脅威を軽減することができる。
本稿では,SV-COMPフォーマットでJava検証ベンチマークを自動的に生成するARG-Vツールの応用について述べる。
新たに生成された68の現実的なベンチマークセットにおいて、4つの主要なJava検証者は、既存のベンチマークスイートのパフォーマンスと比較して、正確さとリコールを減らしている。
これらの知見は、検証ツール評価の包括性と現実性を高めるためにARG-Vの可能性を浮き彫りにするとともに、検証ツールの実際のソフトウェアへの適用性向上を目的としたロードマップを提供する。
関連論文リスト
- RAG-IGBench: Innovative Evaluation for RAG-based Interleaved Generation in Open-domain Question Answering [50.42577862494645]
本稿では,RAG-IG(Retrieval-Augmented Generation)に基づくインターリーブドジェネレーション(Interleaved Generation)の課題を評価するためのベンチマークであるRAG-IGBenchを提案する。
RAG-IGは、MLLM(Multimodal large language model)と検索機構を統合し、モデルがコヒーレントなマルチモーダルコンテンツを生成するための外部画像テキスト情報にアクセスできるようにする。
論文 参考訳(メタデータ) (2025-10-11T03:06:39Z) - Saving SWE-Bench: A Benchmark Mutation Approach for Realistic Agent Evaluation [5.332969177132911]
SWE-Bench Verifiedのようなソフトウェアエンジニアリングエージェントを評価するための現在のベンチマークは、主にGitHubの問題に由来する。
既存のベンチマークを現実的なユーザクエリに変換する,新たなベンチマークフレームワークを導入する。
論文 参考訳(メタデータ) (2025-10-10T04:42:02Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳(メタデータ) (2025-05-25T19:00:52Z) - VerifyBench: Benchmarking Reference-based Reward Systems for Large Language Models [53.128374915958624]
OpenAI o1とDeepSeek-R1は、推論の領域で素晴らしいパフォーマンスを達成した。
彼らのトレーニングの重要な要素は、強化学習に検証可能な報酬を取り入れることである。
既存の報酬ベンチマークでは、参照ベースの報酬システムの評価は行われていない。
論文 参考訳(メタデータ) (2025-05-21T17:54:43Z) - 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) - Rethinking Link Prediction for Directed Graphs [73.36395969796804]
有向グラフのリンク予測は、様々な現実世界のアプリケーションにとって重要な課題である。
埋め込み手法とグラフニューラルネットワーク(GNN)の最近の進歩は、有望な改善を示している。
本稿では,既存手法の表現性を評価する統一的なフレームワークを提案し,二重埋め込みとデコーダ設計がリンクの有向予測性能に与える影響を強調した。
論文 参考訳(メタデータ) (2025-02-08T23:51:05Z) - N-Version Assessment and Enhancement of Generative AI [2.4861619769660637]
ジェネレーティブAI(GAI)は、ソフトウェアエンジニアリングの生産性を向上させる大きな可能性を秘めている。
GAI生成アーティファクトの広範な検証と検証(V&V)の必要性は、潜在的な生産性向上を損なう可能性がある。
本稿では、GAIが複数バージョンのコードとテストを生成する能力を利用して、これらのリスクを軽減する方法を提案する。
論文 参考訳(メタデータ) (2024-09-21T09:00:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。