論文の概要: Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
- arxiv url: http://arxiv.org/abs/2610.10604v1
- Date: Wed, 07 Oct 2026 02:11:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-10 02:36:53.562778
- Title: Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
- Title（参考訳）: 型チェックを超えて:形式仕様生成の全体的評価を目指して
- Abstract要約: SpecGenは、エージェントが実装の正確性を証明するための正式な契約を生成する。
既存のLeanタスク350ドル、VERINAから189ドル、CLEVERから161ドルで構成された統合データセットを構築しています。
認可された制御では、仕様書は100%の正のテストリコールと負のテスト拒否を達成し、必要な入力の0%の値を受け入れる。
- 参考スコア（独自算出の注目度）: 3.8103821995386356
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: When generating verifiable code, natural language requirements are mapped to machine checked code using LLMs and agentic workflows. A crucial component of this pipeline is specification generation (SpecGen), which produces a formal contract against which an agent can prove implementation correctness. Proof generation can obtain deterministic feedback from a theorem prover, but SpecGen lacks a definitive check that a generated specification captures the user's intent. A checked proof can therefore establish correctness against a specification that misrepresents the intended behaviour. We take a step towards holistic SpecGen evaluation with a unified dataset assembled from $350$ existing Lean tasks, including $189$ from VERINA and $161$ from CLEVER, and a framework covering formal validity, reference similarity and equivalence, and behavioural adequacy. We distinguish acceptance of required inputs from acceptance of valid outputs and rejection of invalid outputs, while making each metric's evidence scope explicit. Across four SpecGen configurations, restricting the generalized tree edit distance (GTED) comparison, a reference similarity measure, to $32$ jointly measurable VERINA tasks changes the VERINA configuration's position from second to fourth in mean similarity, showing the importance of measurement coverage. In an authored control, a specification achieves $100\%$ positive test recall and negative test rejection while accepting $0\%$ of required inputs. This demonstrates that perfect postcondition scores can miss an unusable input contract, motivating separate feedback on input coverage and output constraints.
- Abstract（参考訳）: 検証可能なコードを生成する場合、自然言語要件はLLMとエージェントワークフローを使用してマシンチェックコードにマップされる。
このパイプラインの重要なコンポーネントは仕様生成(SpecGen)である。
証明生成は定理証明器から決定論的フィードバックを得ることができるが、SpecGenは生成された仕様がユーザの意図をキャプチャする決定的なチェックを欠いている。
したがって、チェックされた証明は、意図した振る舞いを誤って表現する仕様に対して正当性を確立することができる。
これは、VERINAから189ドル、CLEVERから161ドル、そして正式な妥当性、参照の類似性と等価性、振る舞いの妥当性を含むフレームワークです。
我々は、必要な入力の受け入れと有効出力の受け入れと無効出力の拒絶を区別し、各指標の証拠範囲を明確にする。
一般的なツリー編集距離(GTED)比較(参照類似度尺度)を32ドルに制限した4つのSpecGen構成では、VERINA設定の位置を平均類似度で2位から4位に変更し、測定カバレッジの重要性を示している。
認可された制御では、仕様書は100\%の正のテストリコールと負のテスト拒絶を達成し、必要な入力の0\%の値を受け入れる。
これは、完全な条件後スコアが使用不可能な入力契約を見逃し、入力カバレッジと出力制約に対する別のフィードバックを動機付けていることを示している。
関連論文リスト
- Watermarking: from Impossibility to Auditable Compliance [78.87513208320995]
EU人工知能法第50条(2)は、合成出力を機械可読かつ検出可能にするために、生成システムの提供者を要求する。
自由形式のテキストにとって、重要な実装の1つは、生成的な透かし処理の実装である。
本稿は、強い透かしに代わる聴覚的な代替品を開発する。
論文 参考訳（メタデータ） (2026-10-05T13:32:41Z) - Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning [5.040391802660918]
VeriSpecは、仕様テキスト自体を監査することで、モデル仕様の不整合を直接検出する最初のアプローチである。
我々の重要な洞察は、LLMを検証子として使用しながら、自然言語で仕様を維持することである。
VeriSpecをOpenAI Model Specに適用し、405のルールを抽出し、5つの矛盾を手作業で検証します。
論文 参考訳（メタデータ） (2026-10-01T15:13:31Z) - Testing and Verification of Quantum Compilers through Assurance Contracts and Evidence [0.25489046505746704]
この調査は、検証済みの変換、等価チェック、差分および変成テスト、プロパティベースのテスト、およびリビジョン間の保証の証拠を比較します。
記録されたカバレッジ更新とソースレベルの選択決定は、レビューを宣言されたスコープ内で監査可能にする。
論文 参考訳（メタデータ） (2026-09-24T01:24:49Z) - ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。
本稿では,3値の証明カバレッジモデルを用いて,仕様品質を診断するDafny用ツールであるProgrampulseを提案する。
論文 参考訳（メタデータ） (2026-08-31T14:00:31Z) - How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
Coinsは、信頼できるテストケースの評価下で仕様をインスタンス化し、具体的な証明義務を生成することで仕様品質を評価する評価フレームワークである。
我々はHumanEvalに関する大規模な研究を、人間によるRocq仕様のキュレートされたセットで実施する。
以上の結果から, 仕様生成は依然として重大な課題であり, 検証の複雑さは仕様品質の真の相違を曖昧にする可能性があることが示唆された。
論文 参考訳（メタデータ） (2026-08-13T10:45:18Z) - Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。
SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
論文 参考訳（メタデータ） (2026-07-05T11:09:30Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
論文 参考訳（メタデータ） (2026-04-29T09:57:07Z) - Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。
各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。
これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
論文 参考訳（メタデータ） (2026-04-20T13:25:40Z) - Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。