論文の概要: ProofPulse: Interactive Proof Coverage Analysis for Dafny
- arxiv url: http://arxiv.org/abs/2608.30818v1
- Date: Mon, 31 Aug 2026 14:00:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-01 18:31:31.428523
- Title: ProofPulse: Interactive Proof Coverage Analysis for Dafny
- Title（参考訳）: ProofPulse: ダニーの対話型証明カバレッジ分析
- Abstract要約: 帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。
本稿では,3値の証明カバレッジモデルを用いて,仕様品質を診断するDafny用ツールであるProgrampulseを提案する。
- 参考スコア（独自算出の注目度）: 47.23158426199152
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification. As such, weak specifications and redundant invariants may create overconfidence in ``verified'' code. We present \proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model. By analyzing proof dependencies, ProofPulse distinguishes between elements that contribute to specification intent, those used only for auxiliary checks, and those irrelevant to any proof obligation. Evaluated against an oracle of 252 programs from the dafny-synthesis benchmark, ProofPulse provides a high-precision signal for specification weaknesses, particularly unnecessary preconditions and vacuous proofs. With unsat-core minimization, ProofPulse achieves perfect precision for precondition classification and reduces false positives across all evaluated categories. These results show that proof coverage is a practical complement to verification. Although it cannot fully capture semantic intent, it can reveal weak proof coupling in programs that otherwise appear fully verified. Just as a pulse check distinguishes vitality from the mere absence of symptoms, ProofPulse exposes weaknesses in proofs that technically verify successfully but still suffer from inadequate or redundant code and specifications.
- Abstract（参考訳）: 帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。
このように、弱い仕様と冗長な不変性は ` `verified'' コードで過剰な自信を生み出す可能性がある。
本稿では、3値の証明カバレッジモデルを用いて仕様品質を診断するDafny用ツールである‘proofpulse’を提案する。
ProofPulseは、証明の依存関係を分析することによって、仕様の意図に寄与する要素、補助的なチェックにのみ使用される要素、証明義務に無関係な要素を区別する。
ダフニー合成ベンチマークから252のプログラムのオラクルに対して評価され、ProofPulseは仕様の弱点、特に不要な前提条件と空白の証明のための高精度な信号を提供する。
アンサットコアの最小化により、ProofPulseは事前条件分類の完全精度を達成し、すべての評価されたカテゴリで偽陽性を減少させる。
これらの結果は,証明カバレッジが検証の事実上の補完であることを示している。
意味的意図を完全に捉えることはできないが、そうでなければ完全に検証されたプログラムにおいて弱い証明結合を明らかにすることができる。
パルスチェックがただの症状の欠如と活力を区別するのと同じように、ProofPulseは技術的に検証が成功しているが、不適切なコードや仕様に苦しむ証明の弱点を露呈する。
関連論文リスト
- A distribution-free certification framework for trustworthy crash-severity prediction [1.089614199781423]
厳密なモデルを修正せずにラップする認証層を開発します。
テキサス州の7つのベースモデルにまたがる520万件の記録では、同層は同一の妥当性を持つ。
フレームワークは定理レベルのテストを備えたオープンソースパッケージとしてリリースされている。
論文 参考訳（メタデータ） (2026-09-10T14:20:08Z) - How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
Coinsは、信頼できるテストケースの評価下で仕様をインスタンス化し、具体的な証明義務を生成することで仕様品質を評価する評価フレームワークである。
我々はHumanEvalに関する大規模な研究を、人間によるRocq仕様のキュレートされたセットで実施する。
以上の結果から, 仕様生成は依然として重大な課題であり, 検証の複雑さは仕様品質の真の相違を曖昧にする可能性があることが示唆された。
論文 参考訳（メタデータ） (2026-08-13T10:45:18Z) - GoodDiffusion: Proactive Copyright Protection for Diffusion Bridge Models via Learnable Sample-specific Signatures [88.63093209858387]
モデルレベルの使用時間制御を実現するために,バックドア機構にインスパイアされたGoodDiffusionを提案する。
GoodDiffusionは、有効なシグネチャを持つ認証クエリの高品質な生成を保存するが、許可されていないインプットの生成を拒否する。
セキュリティを強化するために,各入力に条件付きサンプル固有署名を割り当てるLearningable Signature Network(LSN)を導入する。
論文 参考訳（メタデータ） (2026-06-29T04:07:09Z) - Decodable but Not Faithful: Coupling Natural-Language Rationales to Programmatic Verifiers [0.7212939068975618]
言語モデルはそれらの予測に対して妥当な有理性を生成することができるが、これらの説明はモデルの内部的推論を忠実に表すものではないかもしれない。
本稿では,インラインクレームを推論トレースに挿入するフレームワークである検証器結合推論を提案し,プログラム的検証器出力を予測するための補助整合ヘッドを訓練する。
整合性トレーニングは、検証情報を合理性表現から復調可能にしますが、復調性は忠実な生成を保証しません。
論文 参考訳（メタデータ） (2026-06-19T18:37:24Z) - Stress-Testing Neural Network Verifiers with Provably Robust Instances [10.017475431603389]
我々は,地中構造ラベルを用いた検証インスタンス生成のための再利用可能なフレームワークを提案する。
また、インスタンスの硬さの異なるソースを推定可能な量の集合であるDifficulty Profileについても紹介する。
我々のフレームワークとこれらのプロファイルを用いて、5つの最先端検証ツールを評価し、異なるインスタンスが検証パイプラインの異なる側面を強調していることを示す。
論文 参考訳（メタデータ） (2026-05-16T20:56:52Z) - Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis [7.936959383169967]
本稿では,Dafny における仕様記述のための強化学習フレームワーク SpecRL を提案する。
我々は、仕様完全性の信号として、候補仕様によって拒否された負のテストのごく一部を用いる。
実験により、SpecRLはSFTおよびRLよりも仕様強度と検証成功の両方を改善していることが示された。
論文 参考訳（メタデータ） (2026-04-07T12:53:42Z) - Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。
ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。
タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
論文 参考訳（メタデータ） (2026-04-07T01:19:41Z) - COIN: Uncertainty-Guarding Selective Question Answering for Foundation Models with Provable Risk Guarantees [51.5976496056012]
COINは、統計的に有効な閾値を校正し、質問毎に1つの生成された回答をフィルタリングする不確実性保護選択フレームワークである。
COINはキャリブレーションセット上で経験的誤差率を推定し、信頼区間法を適用して真誤差率に高い確率上界を確立する。
リスク管理におけるCOINの堅牢性,許容回答を維持するための強いテストタイムパワー,キャリブレーションデータによる予測効率を実証する。
論文 参考訳（メタデータ） (2025-06-25T07:04:49Z) - CertDW: Towards Certified Dataset Ownership Verification via Conformal Prediction [48.82467166657901]
本稿では,最初の認証データセット透かし(CertDW)とCertDWベースの認証データセットオーナシップ検証手法を提案する。
共形予測に触発されて,主確率 (PP) と透かし頑健性 (WR) の2つの統計指標を導入する。
我々は、不審モデルのWR値が、透かしのないデータセットでトレーニングされた良性モデルのPP値を大幅に上回る場合に、PPとWRの間に証明可能な低い境界が存在することを証明した。
論文 参考訳（メタデータ） (2025-06-16T07:17:23Z) - TrustLoRA: Low-Rank Adaptation for Failure Detection under Out-of-distribution Data [62.22804234013273]
本稿では,共変量および意味的シフトの両条件下での拒絶による分類を統一し,促進する,単純な故障検出フレームワークを提案する。
キーとなる洞察は、障害固有の信頼性知識を低ランクアダプタで分離し、統合することにより、障害検出能力を効果的かつ柔軟に向上できるということです。
論文 参考訳（メタデータ） (2025-04-20T09:20:55Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
実世界の情報ニーズから10kクレームを抽出したファクトチェックデータセットであるAmbiFCを提示する。
アンビFCの証拠に対する主張を比較する際に,曖昧さから生じる不一致を分析した。
我々は,このあいまいさをソフトラベルで予測するモデルを開発した。
論文 参考訳（メタデータ） (2021-04-01T17:40:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。