Researchers propose a cycle-consistent neural architecture that generates faithful natural language explanations for formal verification certificates, addressing the opacity of these machine-checkable proofs for non-specialists. The system achieves 90.0% cycle-verified soundness on test data from a financial compliance domain, significantly outperforming multi-LLM baselines in both accuracy and inference speed.
- The architecture uses a forward network (NN1) to map certificates to explanations and an inverse network (NN2) to reconstruct certificates, with a symbolic verifier closing the loop for differentiable faithfulness.
- A pointer-generator mechanism ensures lexical grounding by copying state names directly from the certificate, evaluated across 420 test certificates spanning six verification methods.
- The model achieves 90.0% cycle-verified soundness, surpassing the best multi-LLM few-shot baseline of 76.1% by 13.9 percentage points.
- It wins on 10 of 12 verdict/kind categories, with three categories reaching 100% soundness.
- The system offers 860x faster inference (185 ms vs. 160 s), offline operation, deterministic outputs, and zero per-inference cost compared to cloud-based LLMs.
This approach demonstrates that trained specialization outperforms general-purpose LLM prompting for structured certificate explanation while eliminating the deployment constraints associated with cloud-based inference.