論文の概要: POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference
- arxiv url: http://arxiv.org/abs/2605.03356v1
- Date: Tue, 05 May 2026 04:29:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-06 19:35:43.765244
- Title: POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference
- Title（参考訳）: POSTCONDBENCH:形式的後条件推論における正当性と完全性のベンチマーク
- Authors: Gehao Zhang, Juan Zhai,
- Abstract要約: 実世界のソフトウェアからメソッドレベルの後条件生成を評価するベンチマークであるPOSTCONDBENCHを紹介する。
自動評価を可能にするため、POSTCONDBENCHは実行可能な実行環境を提供し、欠陥識別を通じて完全性を運用する。
以上の結果から,リポジトリレベルの依存関係とメソッドの複雑性が,このギャップを悪化させることを示す。
- 参考スコア（独自算出の注目度）: 10.01438318022033
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal postconditions precisely characterize program behavior and support debugging, testing, and verification, but writing them requires substantial expertise and effort. This has motivated recent work on automatically generating postconditions from code and natural-language artifacts using large language models (LLMs). However, evaluation remains a key bottleneck. Existing benchmarks primarily emphasize correctness under limited evaluation settings, often relying on surface-form matching or manual assessment on small or synthetic datasets. We introduce POSTCONDBENCH, a multilingual benchmark for evaluating method-level postcondition generation from real-world software. POSTCONDBENCH comprises 420 Python and Java tasks drawn from 121 open-source projects, each paired with a high-quality ground-truth postcondition set constructed with expert involvement. To enable automatic evaluation, POSTCONDBENCH provides a runnable execution environment and operationalizes completeness via defect discrimination: a postcondition set is more complete if it is violated by more defective implementations while remaining satisfied on correct executions. Using POSTCONDBENCH, we formulate three generation settings and evaluate five SOTA LLMs. Our results reveal a substantial gap between correctness and completeness, and show that repository-level dependencies and method complexity exacerbate this gap.
- Abstract（参考訳）: 形式的なポストコンディションは、プログラムの振る舞いを正確に表現し、デバッグ、テスト、検証をサポートするが、それらを書くには相当な専門知識と努力が必要である。
これは、大規模な言語モデル(LLM)を使用して、コードと自然言語のアーティファクトから後条件を自動的に生成する、という最近の取り組みを動機付けている。
しかし、評価は依然として重要なボトルネックである。
既存のベンチマークは主に、限られた評価設定下での正確さを強調しており、しばしば表面形状のマッチングや、小さなデータセットや合成データセットのマニュアルアセスメントに依存している。
実世界のソフトウェアからメソッドレベルの後条件生成を評価するための多言語ベンチマークであるPOSTCONDBENCHを紹介する。
POSTCONDBENCHは、121のオープンソースプロジェクトから引き出された420のPythonとJavaタスクで構成されている。
自動評価を実現するため、POSTCONDBENCHは実行可能な実行環境を提供し、欠陥識別によって完全性を運用する。
POSTCONDBENCHを用いて3つの世代設定を定式化し、SOTA LLMを5つ評価する。
以上の結果から,リポジトリレベルの依存関係とメソッドの複雑性が,このギャップを悪化させることを示す。
関連論文リスト
- LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - You Don't Need Public Tests to Generate Correct Code [0.9668407688201359]
大規模言語モデルには,有効な入力を自律的に構築し,自己補正のための実行フローをシミュレートする能力があることを示す。
我々は,LLMが反復的に計画し,独自のテスト入力を合成し,シミュレートされた実行を行うことで,地平データの必要性を解消するフレームワークであるDryRUNを紹介した。
論文 参考訳（メタデータ） (2026-04-23T12:21:03Z) - SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference [7.324314351910779]
SpecMindは、LEMをインタラクティブで探索的な推論として扱う、ポストコンディション生成のための新しいフレームワークである。
我々の経験的評価は、SpecMindが生成後条件の正確性と完全性の両方において最先端のアプローチを著しく上回っていることを示している。
論文 参考訳（メタデータ） (2026-02-24T07:01:17Z) - From Benchmark Data To Applicable Program Repair: An Experience Report [1.6913109767046948]
本稿では,プログラムの自動修復へのアプローチについて述べる。
我々はこの目的を達成するために文学の様々な技法を組み合わせている。
実験の結果,我々の手法は標準ベンチマークの他の手法よりも優れていることがわかった。
綿密な検査では、これらのテクニックはいずれも、業界で見られる現実的な欠陥には効かない。
論文 参考訳（メタデータ） (2025-08-22T03:59:27Z) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。
プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。
また, GPT-4o miniが74.18%と高い修理成功率を示した。
論文 参考訳（メタデータ） (2025-07-04T15:36:12Z) - A Controllable Examination for Long-Context Language Models [62.845852724511964]
本研究では,長文言語モデルを評価するベンチマークである$textbfLongBioBenchを紹介する。
その結果,ほとんどのモデルでは,検索結果に対する意味的理解や基礎的推論が不足していることが判明した。
我々のさらなる分析は、文脈的非コヒーレンスなど、既存の合成ベンチマークで採用されているいくつかの設計選択を示している。
論文 参考訳（メタデータ） (2025-06-03T14:23:06Z) - Fact-Consistency Evaluation of Text-to-SQL Generation for Business Intelligence Using Exaone 3.5 [0.0]
大規模言語モデル(LLM)は、テキスト・ツー・ジェネレーションによる構造化データクエリーのための自然言語インタフェースの実現を約束している。
本稿では,Exaone 3.5 を用いて LLM 生成したsql 出力の意味的精度を評価するためのFact-Consistency Evaluation Framework を提案する。
本稿では,LG Electronicsの内部BigQuery環境における実際の販売データから抽出した219の自然言語ビジネス質問からなるドメイン固有ベンチマークを構築した。
我々は,応答精度,実行成功率,意味的誤り率,非応答率を用いてモデル性能を評価する。
論文 参考訳（メタデータ） (2025-04-30T14:42:18Z) - Evaluating Generative Language Models in Information Extraction as Subjective Question Correction [49.729908337372436]
本稿では,新しい評価手法SQC-Scoreを提案する。
主観的質問訂正の原則に着想を得て,新しい評価手法SQC-Scoreを提案する。
3つの情報抽出タスクの結果から,SQC-Scoreは基準値よりもアノテータの方が好ましいことが示された。
論文 参考訳（メタデータ） (2024-04-04T15:36:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。