# Cycle-Consistent Neural Explanation of Formal Verification Certificates

arXiv: https://arxiv.org/abs/2606.24414 · HTML: https://mlsanity.com/paper/2606.24414/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 40 of its 82 references that are in the map.
- First posted on arXiv 23 Jun 2026.

## Builds on (most cited first, 30 of 40)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [BERTScore: Evaluating Text Generation with BERT](https://mlsanity.com/paper/1904.09675/) (2019)
- [GPT-4o System Card](https://mlsanity.com/paper/2410.21276/) (2024)
- [Neural Machine Translation by Jointly Learning to Align and Translate](https://mlsanity.com/paper/1409.0473/) (2014)
- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Get To The Point: Summarization with Pointer-Generator Networks](https://mlsanity.com/paper/1704.04368/) (2017)
- [Large Language Monkeys: Scaling Inference Compute with Repeated Sampling](https://mlsanity.com/paper/2407.21787/) (2024)
- [Improving Neural Machine Translation Models with Monolingual Data](https://mlsanity.com/paper/1511.06709/) (2015)
- [Evaluating the Factual Consistency of Abstractive Text Summarization](https://mlsanity.com/paper/1910.12840/) (2019)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Asking and Answering Questions to Evaluate the Factual Consistency of Summaries](https://mlsanity.com/paper/2004.04228/) (2020)
- [FEQA: A Question Answering Evaluation Framework for Faithfulness Assessment in Abstractive Summarization](https://mlsanity.com/paper/2005.03754/) (2020)
- [Unsupervised Machine Translation Using Monolingual Corpora Only](https://mlsanity.com/paper/1711.00043/) (2017)
- [ToTTo: A Controlled Table-To-Text Generation Dataset](https://mlsanity.com/paper/2004.14373/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Beam Search Strategies for Neural Machine Translation](https://mlsanity.com/paper/1702.01806/) (2017)
- [Synchromesh: Reliable code generation from pre-trained language models](https://mlsanity.com/paper/2201.11227/) (2022)
- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [Data Augmentation for Low-Resource Neural Machine Translation](https://mlsanity.com/paper/1705.00440/) (2017)
- [Style Transfer Through Back-Translation](https://mlsanity.com/paper/1804.09000/) (2018)
- [Logical Natural Language Generation from Open-Domain Tables](https://mlsanity.com/paper/2004.10404/) (2020)
- [Improving Coherence and Consistency in Neural Sequence Models with Dual-System, Neuro-Symbolic Reasoning](https://mlsanity.com/paper/2107.02794/) (2021)
- [Pointing the Unknown Words](https://mlsanity.com/paper/1603.08148/) (2016)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [CBMC: The C Bounded Model Checker](https://mlsanity.com/paper/2302.02384/) (2023)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)

## Abstract (arXiv)

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.