論文の概要: VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications

• arxiv url: http://arxiv.org/abs/2604.00280v1
• Date: Tue, 31 Mar 2026 22:12:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-02 16:44:31.746309
• Title: VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
• Title（参考訳）: VeriAct:Beyond Verifiability -- 正確で完全な形式仕様のエージェント合成
• Authors: Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes,
• Abstract要約: 自動JML仕様合成における古典的手法と急進的手法を比較した。 提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。 本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
• 参考スコア（独自算出の注目度）: 0.3240750198587795
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specifications play a central role in ensuring software reliability and correctness. However, automatically synthesizing high-quality formal specifications remains a challenging task, often requiring domain expertise. Recent work has applied large language models to generate specifications in Java Modeling Language (JML), reporting high verification pass rates. But does passing a verifier mean that the specification is actually correct and complete? In this work, we first conduct a comprehensive evaluation comparing classical and prompt-based approaches for automated JML specification synthesis. We then investigate whether prompt optimization can push synthesis quality further by evolving prompts through structured verification feedback. While optimization improves verifier pass rates, we find a clear performance ceiling. More critically, we propose Spec-Harness, an evaluation framework that measures specification correctness and completeness through symbolic verification, revealing that a large fraction of verifier-accepted specifications, including optimized ones, are in fact incorrect or incomplete, over- or under-constraining both inputs and outputs in ways invisible to the verifier. To push beyond this ceiling, we propose VeriAct, a verification-guided agentic framework that iteratively synthesizes and repairs specifications through a closed loop of LLM-driven planning, code execution, verification, and Spec-Harness feedback. Our experiments on two benchmark datasets show that VeriAct outperforms both prompt-based and prompt-optimized baselines, producing specifications that are not only verifiable but also correct and complete.
• Abstract（参考訳）: 正式な仕様は、ソフトウェアの信頼性と正確性を保証する上で中心的な役割を果たす。 しかし、高品質な形式仕様を自動で合成することは難しい課題であり、しばしばドメインの専門知識を必要とする。 最近の研究は、Java Modeling Language(JML)の仕様を生成するために大きな言語モデルを適用し、高い検証パス率を報告しています。 しかし、検証をパスすることは、仕様が実際に正しく完成していることを意味するのだろうか? 本稿では,JML仕様の自動合成における古典的手法と急進的手法を総合評価する。 そこで我々は,構造化された検証フィードバックを通じて,プロンプトを進化させることにより,プロンプト最適化が合成品質をさらに向上させることができるかどうかを検討する。 最適化によって検証器のパスレートが向上する一方、明確な性能天井が見つかる。 より重要な点として,シンボル検証による仕様の正しさと完全性を評価する評価フレームワークであるSpec-Harnessを提案する。 この天井を越えるために、私たちは検証誘導型エージェントフレームワークであるVeriActを提案し、LCM駆動の計画、コード実行、検証、Spec-Harnessフィードバックのクローズドループを通じて仕様を反復的に合成し、修復する。 2つのベンチマークデータセットに対する実験により、VeriActはプロンプトベースとプロンプト最適化ベースラインの両方を上回り、検証可能なだけでなく、正確かつ完全な仕様を生成することがわかった。

関連論文リスト

• InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
  InFi-Checkは、大規模な言語モデルの解釈ときめ細かい事実チェックのためのフレームワークである。 InFi-Checkerは、サポートエビデンスを提供し、きめ細かいエラータイプを分類し、修正と共に正当化を生成する。 実験の結果,InFi-CheckerはInFi-Check-FGの最先端性能を実現することがわかった。
  論文  参考訳（メタデータ） (2026-01-10T20:00:17Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。 AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。 このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
  論文  参考訳（メタデータ） (2025-07-14T14:43:14Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• FactLens: Benchmarking Fine-Grained Fact Verification [6.814173254027381]
  我々は、複雑なクレームを個別の検証のためにより小さなサブステートに分割する、きめ細かい検証へのシフトを提唱する。 我々は,ファクトレンス(FactLens)という,ファクトレンス(FactLens)という,詳細な事実検証のベンチマークを紹介した。 この結果から,FactLens自動評価器と人的判断との整合性を示し,評価性能に対する準定値特性の影響について考察した。
  論文  参考訳（メタデータ） (2024-11-08T21:26:57Z)
• OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
  OpenFactCheckは、カスタマイズされたファクトチェックシステムを構築するためのフレームワークである。 ユーザーは自動的にファクトチェッカーをカスタマイズし、文書やクレームの事実的正当性を検証できる。 CheckerEVALは、人間の注釈付きデータセットを使用して、自動ファクトチェッカーの検証結果の信頼性を高めるソリューションである。
  論文  参考訳（メタデータ） (2024-05-09T07:15:19Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)

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

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