論文の概要: Cycle-Consistent Neural Explanation of Formal Verification Certificates
- arxiv url: http://arxiv.org/abs/2606.24414v1
- Date: Tue, 23 Jun 2026 10:51:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-24 22:16:48.904463
- Title: Cycle-Consistent Neural Explanation of Formal Verification Certificates
- Title（参考訳）: 形式検証証明書のサイクル一貫性ニューラル記述
- Authors: Andoni Rodriguez, Alberto Pozanco, Daniel Borrajo,
- Abstract要約: 本稿では,検証証明書の忠実な自然言語記述を生成するサイクル一貫性ニューラルアーキテクチャを提案する。
ポインタジェネレータ機構は、証明書から直接状態名をコピーすることで、語彙基底を保証する。
学習したアーキテクチャは、ハイブリッドな推論時ルーティング戦略と組み合わせて、90.0%のサイクル検証された音性を実現する。
- 参考スコア（独自算出の注目度）: 5.61123152362224
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal verification produces machine-checkable certificates that attest to the satisfaction or violation of temporal properties, yet these certificates remain opaque to non-specialist stakeholders. We propose a cycle-consistent neural architecture that generates faithful natural language explanations of verification certificates. A forward network NN1 maps certificates to explanations, and an inverse network NN2 reconstructs certificates from explanations; a symbolic verifier closes the loop, providing a differentiable faithfulness proxy. A pointer-generator mechanism ensures lexical grounding by copying state names directly from the certificate. We evaluate on 420 test certificates spanning six verification methods (bounded proof, k-induction, inductive invariant, lasso, reachability, witness pair) in both YES and NO verdict variants, drawn from a financial compliance domain with 207 named states. Our trained architecture, combined with a hybrid inference-time routing strategy, achieves 90.0% cycle-verified soundness, surpassing a multi- LLM few-shot baseline (76.1% for the best of 16 LLM combinations across four frontier models) by 13.9 percentage points. The neural model wins on 10 of 12 verdict/kind categories, with three categories reaching 100% soundness. The architecture offers 860x faster inference (185 ms vs. 160 s per certificate for the full multi-LLM baseline), offline operation, deterministic outputs, and zero per-inference cost. These results demonstrate that trained specialization outperforms general-purpose LLM prompting for structured certificate explanation, while eliminating the deployment constraints of cloud-based inference.
- Abstract（参考訳）: 形式的検証は、時間的特性の満足度や違反を証明したマシンチェック可能な証明書を生成するが、これらの証明書は非専門家の利害関係者には不透明である。
本稿では,検証証明書の忠実な自然言語記述を生成するサイクル一貫性ニューラルアーキテクチャを提案する。
フォワードネットワークNN1は、証明書を説明にマップし、逆ネットワークNN2は説明から証明書を再構築する。
ポインタジェネレータ機構は、証明書から直接状態名をコピーすることで、語彙基底を保証する。
我々は,YESとNOの両変種における6つの検証方法(有界証明, k-インダクション, 帰納的不変量, ラッソ, 到達可能性, 目撃者ペア)にまたがる420の試験証明を,207の名前を冠した金融コンプライアンス領域から抽出した。
学習したアーキテクチャは、ハイブリッドな推論時ルーティング戦略と組み合わせて、サイクル検証された音質を90.0%達成し、マルチLLM数ショットベースライン(4つのフロンティアモデルで16LLMの組み合わせで76.1%)を13.9%上回った。
ニューラルネットワークは、12の評定/類型のうち10のカテゴリーで勝利し、3つのカテゴリが100%の音性に達する。
このアーキテクチャは、完全なマルチLLMベースラインの証明書あたり160秒に対して860倍高速な推論(185ミリ秒)、オフライン操作、決定論的出力、推論コストゼロを提供する。
これらの結果から,訓練された専門化は,クラウドベースの推論の展開制約を排除しつつ,構造化証明書の説明を促す汎用LSMよりも優れていた。
関連論文リスト
- Calibration of Structured Ignorance Certificates for Diagnosing Unknown Unknowns in Reasoning Models [0.0]
大きな言語モデルは、しばしば特徴的な方法で失敗する。無知を認めるのではなく、知識境界を越えて存在する質問に対して、流動的だが誤った答えを生み出す。
textbfStructured Ignorance Certificates (SICs) というパラフレーズ形式の出力スキーマを導入する。
735 UU質問に対する評価は、99.46%の妥当性率、0.967の平均証明特異度スコア、3.6%のROUGE-L改善を達成する。
論文 参考訳（メタデータ） (2026-06-07T11:01:13Z) - Hallucination as Exploit: Evidence-Carrying Multimodal Agents [10.441697487723568]
マルチモーダルエージェントはますます、スクリーンショットやドキュメント、Webページからツールコールを選択している。
本稿では,自由形式モデルテキストを不許容な証拠として扱うエビデンス搬送型マルチモーダルエージェント(ECA)を提案する。
ECAは不透明なモデルの信念を検証者、スキーマ、実装レベルで監査可能な残留物に変換する。
論文 参考訳（メタデータ） (2026-05-18T23:40:43Z) - Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture [0.0]
本稿では,大規模言語モデルを取り巻く決定論的構造化計算を検証するためのフレームワークを提案する。
リーン4の信頼境界アーキテクチャを,現代的なLLMパイプラインの汎用インターフェースに拡張しています。
論文 参考訳（メタデータ） (2026-05-13T12:01:41Z) - Towards Intelligent Legal Document Analysis: CNN-Driven Classification of Case Law Texts [1.3192560874022086]
本研究は,引用処理分類のための軽量かつ高精度なフレームワークを提案する。
単語認識型FastText埋め込みと1次元畳み込みニューラルネットワーク(CNN)との補間に基づく前処理を併用する。
提案システムは97.26%の分類精度と96.82%のマクロF1スコアを達成し,既存のベースラインを超えている。
論文 参考訳（メタデータ） (2026-04-20T00:14:11Z) - Governing Dynamic Capabilities: Cryptographic Binding and Reproducibility Verification for AI Agent Tool Use [0.0]
既存のセキュリティレイヤでは、AIエージェントに何ができるか、それが主張するものを実行したのか、マルチエージェントインタラクションで何が起きたのかを検証できない。
既存のフレームワークはこれら2つを詳述し、サイレントな能力のエスカレーションを可能にし、検証済みの証明なしに相互作用を残す。
我々は3つのエージェントガバナンス要件を導出する:能力の完全性(G1)、行動の妥当性(G2)、相互作用監査性(G3)。
基本(Ed25519, SHA-256; 97 us verify)と拡張(BBS+選択開示、Groth16 DV-SNARK; 13.8 ms)の2つの暗号に依存しないインスタンス化で検証する。
論文 参考訳（メタデータ） (2026-03-15T11:46:57Z) - TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。
我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
論文 参考訳（メタデータ） (2026-02-26T05:11:44Z) - Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
グラフニューラルネットワーク(GNN)におけるラベルフリップの正確な認証手法を提案する。
本稿では,ノード分類タスクにおける広範囲なGNNアーキテクチャの認証に本手法を適用した。
私たちの研究は、ニューラルネットワークによって引き起こされた毒殺攻撃に対する最初の正確な認証を提示します。
論文 参考訳（メタデータ） (2024-11-30T17:05:12Z) - Sound and Complete Verification of Polynomial Networks [55.9260539566555]
PN(Polynomial Networks)は、最近顔と画像の認識において有望な性能を示した。
分岐とバウンド(BaB)技術に基づくReLUニューラルネットワーク(NN)上の既存の検証アルゴリズムは、PN検証に自明に適用できない。
我々は、VPNと呼ばれるグローバルコンバージェンス保証のためのBaBを備えた新しいバウンダリング手法を考案した。
論文 参考訳（メタデータ） (2022-09-15T11:50:43Z) - Towards Evading the Limits of Randomized Smoothing: A Theoretical
Analysis [74.85187027051879]
決定境界を複数の雑音分布で探索することにより,任意の精度で最適な証明を近似できることを示す。
この結果は、分類器固有の認証に関するさらなる研究を後押しし、ランダム化された平滑化が依然として調査に値することを示す。
論文 参考訳（メタデータ） (2022-06-03T17:48:54Z) - Second-Order Provable Defenses against Adversarial Attacks [63.34032156196848]
ネットワークの固有値が有界であれば、凸最適化を用いて$l$ノルムの証明を効率的に計算できることを示す。
認証精度は5.78%,44.96%,43.19%であった。
論文 参考訳（メタデータ） (2020-06-01T05:55:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。