Cycle-Consistent Neural Explanation of Formal Verification Certificates

• URL: http://arxiv.org/abs/2606.24414v1
• Date: Tue, 23 Jun 2026 10:51:54 GMT
• Title: Cycle-Consistent Neural Explanation of Formal Verification Certificates
• Abstract summary: We propose a cycle-consistent neural architecture that generates faithful natural language explanations of verification certificates.<n>A pointer-generator mechanism ensures lexical grounding by copying state names directly from the certificate.<n>Our trained architecture, combined with a hybrid inference-time routing strategy, achieves 90.0% cycle-verified soundness.
• Score: 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.

Related papers

• When Certificates Fail: A Unified Safety Framework for Embedded Neural Interface Models [0.0]
  We propose a unified empirical audit framework organized around three failures: verification insufficiency, proxy-fidelity divergence, and latent information exfiltration.<n>We instantiate the framework on BCI Competition IV 2a and SEED-IV using multiple deep and classical EEG decoders, official session-level validation, null controls, and paired statistical tests.<n>Our results establish that operational safety auditing, not certificate verification alone, is necessary for responsible neural-interface deployment.
  arXiv  Detail & Related papers  (2026-07-07T13:03:45Z)
• Calibration of Structured Ignorance Certificates for Diagnosing Unknown Unknowns in Reasoning Models [0.0]
  Large language models frequently fail in a characteristic way: rather than acknowledging ignorance, they produce fluent but incorrect answers to questions that lie beyond their knowledge boundaries.<n>We introduce textbfStructured Ignorance Certificates (SICs), a paraphrase-formatted output schema that demands a model explicitly name the missing domain, enumerate concepts, and propose a productive retrieval query rather than hallucinating an answer.<n> Evaluation on 735 held-out UU questions achieves a 99.46% validity rate, a mean Certificate Specificity Score of 0.967, and a 3.6% ROUGE-L improvement over the base
  arXiv  Detail & Related papers  (2026-06-07T11:01:13Z)
• Hallucination as Exploit: Evidence-Carrying Multimodal Agents [10.441697487723568]
  Multimodal agents increasingly choose tool calls from screenshots, documents, and webpages, where a false perceptual claim can turn from an answer-quality error into an authorization failure.<n>We propose evidence-carrying multimodal agents (ECA), which treat free-form model text as inadmissible evidence.<n>ECA converts opaque model belief into auditable residuals at the verifier, schema, and implementation levels.
  arXiv  Detail & Related papers  (2026-05-18T23:40:43Z)
• Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture [0.0]
  We present a framework for verifying the deterministic structured computations surrounding a large language model.<n>We extend a Lean 4 trust-boundary architecture to the generic interfaces of modern LLM pipelines.
  arXiv  Detail & Related papers  (2026-05-13T12:01:41Z)
• Towards Intelligent Legal Document Analysis: CNN-Driven Classification of Case Law Texts [1.3192560874022086]
  This work presents a lightweight yet high-accuracy framework for citation-treatment classification.<n>It pairs lemmatisation-based preprocessing with subword-aware FastText embeddings and a one-dimensional Convolutional Neural Network (CNN)<n>The proposed system achieves 97.26% classification accuracy and a macro F1-score of 96.82%, surpassing established baselines.
  arXiv  Detail & Related papers  (2026-04-20T00:14:11Z)
• Governing Dynamic Capabilities: Cryptographic Binding and Reproducibility Verification for AI Agent Tool Use [0.0]
  No existing security layer verifies what an AI agent can do, whether it executed what it claims, or what happened in a multi-agent interaction.<n>Existing frameworks conflate the two, enabling silent capability escalation and leaving interactions without verifiable provenance.<n>We derive three Agent Governance Requirements: capability integrity (G1), behavioral verifiability (G2), and interaction auditability (G3)<n>We validate with two crypto-agnostic instantiations -- basic (Ed25519, SHA-256; 97 us verify) and enhanced (BBS+ selective disclosure, Groth16 DV-SNARK; 13.8 ms)
  arXiv  Detail & Related papers  (2026-03-15T11:46:57Z)
• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
  arXiv  Detail & Related papers  (2026-02-26T05:11:44Z)
• Shh, don't say that! Domain Certification in LLMs [124.61851324874627]
  Large language models (LLMs) are often deployed to perform constrained tasks, with narrow domains.<n>We introduce domain certification; a guarantee that accurately characterizes the out-of-domain behavior of language models.<n>We then propose a simple yet effective approach, which we call VALID that provides adversarial bounds as a certificate.
  arXiv  Detail & Related papers  (2025-02-26T17:13:19Z)
• Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
  We introduce an exact certification method for label flipping in Graph Neural Networks (GNNs)<n>We apply our method to certify a broad range of GNN architectures in node classification tasks.<n>Our work presents the first exact certificate to a poisoning attack ever derived for neural networks.
  arXiv  Detail & Related papers  (2024-11-30T17:05:12Z)
• Sound and Complete Verification of Polynomial Networks [55.9260539566555]
  Polynomial Networks (PNs) have demonstrated promising performance on face and image recognition recently. Existing verification algorithms on ReLU neural networks (NNs) based on branch and bound (BaB) techniques cannot be trivially applied to PN verification. We devise a new bounding method, equipped with BaB for global convergence guarantees, called VPN.
  arXiv  Detail & Related papers  (2022-09-15T11:50:43Z)
• Towards Evading the Limits of Randomized Smoothing: A Theoretical Analysis [74.85187027051879]
  We show that it is possible to approximate the optimal certificate with arbitrary precision, by probing the decision boundary with several noise distributions. This result fosters further research on classifier-specific certification and demonstrates that randomized smoothing is still worth investigating.
  arXiv  Detail & Related papers  (2022-06-03T17:48:54Z)
• Second-Order Provable Defenses against Adversarial Attacks [63.34032156196848]
  We show that if the eigenvalues of the network are bounded, we can compute a certificate in the $l$ norm efficiently using convex optimization. We achieve certified accuracy of 5.78%, and 44.96%, and 43.19% on 2,59% and 4BP-based methods respectively.
  arXiv  Detail & Related papers  (2020-06-01T05:55:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.