論文の概要: 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 -- 正確で完全な形式仕様のエージェント合成
• 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はプロンプトベースとプロンプト最適化ベースラインの両方を上回り、検証可能なだけでなく、正確かつ完全な仕様を生成することがわかった。

関連論文リスト

• SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
  我々は、形式的なコード合成をアトミックで再利用可能なスキルのライブラリに分解するフレームワークであるSKILLFORGEを紹介する。 検証駆動ハーネスはこれらのスキルを編成する。 Dafny仕様のペアに対する自然言語のキュレートされたベンチマークでは、SKILLFORGEは最先端のエージェントアプローチよりも大幅に優れている。
  論文  参考訳（メタデータ） (2026-08-30T15:15:00Z)
• How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
  Coinsは、信頼できるテストケースの評価下で仕様をインスタンス化し、具体的な証明義務を生成することで仕様品質を評価する評価フレームワークである。 我々はHumanEvalに関する大規模な研究を、人間によるRocq仕様のキュレートされたセットで実施する。 以上の結果から, 仕様生成は依然として重大な課題であり, 検証の複雑さは仕様品質の真の相違を曖昧にする可能性があることが示唆された。
  論文  参考訳（メタデータ） (2026-08-13T10:45:18Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。 ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。 1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
  論文  参考訳（メタデータ） (2026-07-01T09:58:59Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification [10.586396714718457]
  SpecSyn は LLM ベースの新しい仕様生成手法である。 実験では、SpecSynは90%以上の高精度なリコールと75%以上の卓越したリコールを維持している。 さらなる評価では、SpecSynは1365のターゲットプロパティのうち1071の処理に成功している。
  論文  参考訳（メタデータ） (2026-04-23T11:46:19Z)
• Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
  LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。 動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。 我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
  論文  参考訳（メタデータ） (2026-04-17T14:56:45Z)
• 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)

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

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