論文の概要: Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
- arxiv url: http://arxiv.org/abs/2607.09366v1
- Date: Fri, 10 Jul 2026 12:44:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-13 14:47:12.841111
- Title: Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
- Title（参考訳）: 検証の多様化: タスク等価プログラムが検証可能性に影響を及ぼすとき
- Authors: Shirley Yu, Ruben Martins,
- Abstract要約: 本稿では,複数のプログラムが同じタスクレベルのセマンティクスを満たすことを意図した場合,実装構造が自動検証可能性に影響を及ぼすかを検討する。
We present Diversify2Verify, a staged LLM-based pipeline for Why3 that infers representation-specific contract。
また、整数、配列、リストに対する73のタスクの検証指向のベンチマークを構築し、292種類の実装を出力した。
- 参考スコア（独自算出の注目度）: 4.920145245773581
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Program verification is crucial for software correctness, but producing fully verified programs remains difficult in practice. This paper studies whether implementation structure affects automated verifiability when multiple generated programs are intended to satisfy the same task-level semantics. We present Diversify2Verify, a staged LLM-based pipeline for Why3 that infers representation-specific contracts, generates and tests diverse recursive and imperative array/list implementations, and attempts verification with bounded verifier-guided annotation repair. We also construct a verification-oriented benchmark of 73 tasks over integers, arrays, and lists, yielding 292 implementation variants. Diversify2Verify verifies 96 artifacts initially and 154 after two repair passes, improving artifact-level verification from 32.9% to 52.7%. At the task level, at least one variant verifies for 49 of 73 tasks, a 67.1% success rate. These results show that task-equivalent implementations can differ substantially in verifiability and that implementation diversity helps find verification-friendly artifacts.
- Abstract（参考訳）: プログラム検証は、ソフトウェアの正確性には不可欠であるが、完全に検証されたプログラムを作成することは、実際は難しい。
本稿では,複数のプログラムが同じタスクレベルのセマンティクスを満たすことを意図した場合,実装構造が自動検証可能性に影響を及ぼすかを検討する。
We present Diversify2Verify, a staged LLM-based pipeline for Why3 which infers representation-specific contract, generated and testing various recursive and imperative array/list implementation, and try verification with bounded verifier-guided annotations repair。
また、整数、配列、リストに対する73のタスクの検証指向のベンチマークを構築し、292種類の実装を出力した。
Diversify2Verifyは2回の修理の後、96のアーティファクトと154の検証を行い、アーティファクトレベルの検証を32.9%から52.7%に改善した。
タスクレベルでは、少なくとも1つの変種が73タスクのうち49、67.1%の成功率を検証している。
これらの結果から,タスク等価な実装は検証可能性に大きく違いがあり,実装の多様性は検証しやすい成果物を見つけるのに役立つことが示唆された。
関連論文リスト
- Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。
SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
論文 参考訳（メタデータ） (2026-07-05T11:09:30Z) - SkillAudit: Ground-Truth-Free Skill Evolution via Paired Trajectory Auditing [81.51044612408793]
SkillAuditは、地味なフィードバックなしにエージェントスキルを進化させるフレームワークである。
行動の違いを編集指導に変換するために、SkillAuditはProcess-Aligned Contrastive Evaluationを使用する。
Refineはノイズや無関係なガイダンスを広く有用なスキルから取り除き、修復はタスクと競合するパスを置き換える。
論文 参考訳（メタデータ） (2026-06-12T08:20:09Z) - Automating Formal Verification with Reinforcement Learning and Recursive Inference [0.0]
我々はダフニーで検証可能な報酬(RLVR)と検証者誘導推論時間探索を用いてオープンソースモデルを訓練する。
固定ベースモデルでは、証明修正器を備えた完全な足場は、直接修理中の初期VeriCodingパイロットセットのパスレートを46.2%から69.2%に改善する。
Rust $texttcurve25519-dalek$検証プロジェクトから派生した,レポジトリスケールのLeanベンチマークであるDalek-Benchについても紹介します。
論文 参考訳（メタデータ） (2026-05-29T06:59:28Z) - Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。
この問題は、事前評価が結果駆動である変換において特に深刻である。
ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。
このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
論文 参考訳（メタデータ） (2026-05-27T19:57:15Z) - Agentic Proving for Program Verification [44.663012714194025]
エージェントシステムは、形式数学における自動定理証明のための最先端のアプローチとして登場した。
検証可能なコード生成のためのLean 4ベンチマークであるCLEVERのエージェント証明フレームワークでClaude Codeを評価した。
論文 参考訳（メタデータ） (2026-05-22T15:41:27Z) - SPECA: Specification-to-Checklist Agentic Auditing for Multi-Implementation Systems -- A Case Study on Ethereum Clients [1.711666249985278]
SPECAは、標準要件をチェックリストに変換する仕様からChecklistフレームワークである。
SPECAは,11社を対象とし,フサカアップグレードのセキュリティ監査コンテストの会場内でインスタンス化を行う。
我々の改善されたエージェントは、競争監査の基礎的真実に対して評価され、高影響の脆弱性について27.3%の厳格なリコールを達成した。
論文 参考訳（メタデータ） (2026-02-07T12:19:00Z) - Comprehensive Evaluation of Large Language Models on Software Engineering Tasks: A Multi-Task Benchmark [0.0]
大規模言語モデル(LLM)は、ソフトウェア工学において顕著な能力を示している。
本稿では,5つのソフトウェアエンジニアリングタスクにまたがる11の最先端LCMのマルチタスク評価について述べる。
論文 参考訳（メタデータ） (2026-02-06T03:30:19Z) - Inferring multiple helper Dafny assertions with LLMs [47.33158055894705]
本研究では,Dafnyプログラムにおけるヘルパーアサーションの欠落を自動的に推測するために,Large Language Modelsの使用について検討する。
推論の難易度を分析するために,アサーション型の分類を導入した。
その結果、自動アサーション推論は証明工学の労力を大幅に削減できることが示された。
論文 参考訳（メタデータ） (2025-10-31T09:45:39Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。