論文の概要: VerusEval: Evaluating LLM-Generated Verus Specifications Beyond Verifier Acceptance
- arxiv url: http://arxiv.org/abs/2610.26464v1
- Date: Mon, 19 Oct 2026 14:15:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-23 17:27:03.737979
- Title: VerusEval: Evaluating LLM-Generated Verus Specifications Beyond Verifier Acceptance
- Title（参考訳）: VerusEval: 検証受け入れを超えたLLM生成のVerus仕様の評価
- Abstract要約: 大規模な言語モデルは、RustプログラムのVerusコントラクトの生成にますます使用されている。
VerusEvalは、6次元に沿って生成されたコントラクトを評価するフレームワークである。
- 参考スコア（独自算出の注目度）: 26.73935855697832
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models (LLMs) are increasingly used to generate Verus contracts for Rust programs together with the proofs that establish them. Yet verifier acceptance, the common measure of success, shows only that the implementation satisfies the generated contract, so it leaves open whether the contract captures the intended behavior. Assessing specification generation therefore requires an evaluation methodology, not a single metric. We present VerusEval, a framework that evaluates generated contracts along six dimensions, including Verus-native checks for semantic triviality, validated input-output (I/O) suites, and contract equivalence, and that relates them so that the strength and blind spots of each become measurable. Evaluating 13,716 artifacts from four workflows, five LLMs, and two prompting settings on 762 tasks, we find that acceptance overstates quality: only 42.3\% of the accepted artifacts complete all three semantic checks without a flag, and across workflows and models, higher acceptance does not consistently come with more correct contracts. I/O evaluation rejects 23.6\% of the accepted artifacts, yet only 63.2\% of those that pass it are proved equivalent. Of the accepted artifacts flagged by contract comparison, 84.1\% have a rejected completeness obligation, and the direction of a failure prioritizes inspection of the generated contract or the reference; it does not by itself establish which artifact is defective. Screening and review further identify 36 candidate defects among 61 selected reference contracts, and repairing one of them makes 10 of its 11 failing artifacts equivalent. Based on these findings, we derive four actionable lessons for evaluation, generation, and benchmark maintenance.
- Abstract（参考訳）: 大規模な言語モデル(LLM)は、RustプログラムのVerusコントラクトの生成と、それらを確立するための証明にますます使用されている。
しかし、検証者の受け入れは、成功の一般的な尺度であり、実装が生成されたコントラクトを満たすことのみを示し、契約が意図した振る舞いをキャプチャするかどうかを公開します。
したがって仕様生成を評価するには、単一のメトリクスではなく評価方法論が必要である。
VerusEvalは,意味的自明性に対するVerus-native Checks,検証された入出力(I/O)スイート,およびコントラクト等価性など,6次元に沿って生成されたコントラクトを評価するフレームワークである。
4つのワークフローから13,716のアーティファクトを評価し、5つのLLMと2つのプロンプト設定を722タスクで行うと、受け入れアーティファクトの品質が過大評価されていることが分かる。
I/O評価は、承認されたアーティファクトの23.6\%を拒絶するが、それを通過するアーティファクトの63.2\%のみが等価であることが証明されている。
契約比較により通知された受理された成果物のうち、84.1\%は完全性義務を拒絶しており、故障の方向は生成された契約又は基準の検査を優先する。
審査とレビューにより、61の基準契約のうち36の欠陥が特定され、そのうちの1つを修復すると、11の欠陥のうち10が同等となる。
これらの結果から,評価,生成,ベンチマークの4つの実践的教訓を導出した。
関連論文リスト
- Right Answers, Wrong States: Hidden Information Failures in Multi-Agent Collaboration [69.14904049421806]
共同作業は、即時決定が正しい場合でも、腐敗した情報状態に置き去りにすることができる。
GPT、Gemini、Qwenモデル全体では、標準的なコラボレーションは、状態の信頼性よりもはるかに強力なタスクパフォーマンスを示している。
我々は、矛盾する証拠を解決し、共有された事実を検証し、信頼された国家を再構築するReGroundを紹介します。
論文 参考訳（メタデータ） (2026-10-01T07:42:27Z) - Maat: Independent Deterministic Contract-Based Governance for Multi-Agent LLM Workflows [0.0]
私たちは、バージョン管理されたワークフロー契約アンカーに対してエージェントからエージェントへのハンドオフを検証するランタイムガバナンス層であるMaatを紹介します。
データレベルの欠陥を注入した6つの制御ドメイン(6～15エージェント、522トライアル)と決定論的7チェックルーブリックで評価した。
論文 参考訳（メタデータ） (2026-09-27T23:23:52Z) - IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。
提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。
IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
論文 参考訳（メタデータ） (2026-09-09T17:59:04Z) - The Architect, the Adversary, and the Judge: Closed-Loop Generation of Standards-Aligned Assessment Items at Scale [13.85834524293015]
CLAIMは、K-12アセスメント・イテム生成のための生産パイプラインである。
パイプラインは9,074イテムの生産で97.8%のエキスパート評価パスレートに達する。
論文 参考訳（メタデータ） (2026-08-26T08:54:32Z) - Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
正しいパッチの発見と保持、検証、提出のギャップについて検討する。
我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
論文 参考訳（メタデータ） (2026-07-27T16:05:23Z) - Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。
この問題は、事前評価が結果駆動である変換において特に深刻である。
ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。
このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
論文 参考訳（メタデータ） (2026-05-27T19:57:15Z) - ContractBench: Can LLM Agents Preserve Observation Contracts? [9.057486468322933]
観察契約の遵守は、緊急かつ回帰的な能力であることを示す。
ContractBenchは、2つの障害モードを探索する33の二重軸タスクのベンチマークである。
i)評価モデルが80%,Claude-Opus-4.6が77.8%, (ii)Qwen 3.5で4B (0%) から9B (56.6%) の急激な家庭内能力崖が397B-A17Bで70.7%, (iii) GPT-5ファミリーでの非単調性スケーリングが消失した。
論文 参考訳（メタデータ） (2026-05-17T06:37:04Z) - Measuring LLM Trust Allocation Across Conflicting Software Artifacts [4.974612243038232]
本稿では,Javadoc上の構造化アーティファクトレベルの信頼トレース,メソッドシグネチャ,実装,テストプレフィックスを付与するフレームワークであるTRACEを紹介する。
我々は,人工物ごとの品質評価,不整合検出,影響を受ける人工物属性,ソース優先性を評価した。
論文 参考訳（メタデータ） (2026-04-03T20:38:14Z) - HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。
HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。
我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7～10ポイントの絶対精度を観測した。
論文 参考訳（メタデータ） (2026-02-15T02:50:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。