Faithful Autoformalization via Roundtrip Verification and Repair

TL;DR

This paper introduces a roundtrip verification framework for assessing the faithfulness of LLM formalizations without ground-truth annotations, using formalization, translation, and logical equivalence checks.

Contribution

It presents a novel verification and repair approach that diagnoses and corrects errors in LLM formalizations through a cycle of translation and logical checks.

Findings

Diagnosis-guided scoped repair improves formalization accuracy.

Rules passing the equivalence check exhibit less NLI drift.

Effectiveness depends on the reliability of the diagnosis function.

Abstract

When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural language, re-formalize, and use a formal tool to check logical equivalence. When the two formalizations agree, this provides evidence of a faithful formalization. When they disagree, a stage-level diagnosis localizes the error to a specific translation step, and a scoped repair operator attempts to correct that step. We evaluate the framework on two statutory domains (the Texas Transportation Code and the Texas Parks and Wildlife Code) using two LLMs (Claude Opus~4.6 and GPT-5.2) with three repair baselines. Diagnosis-guided scoped repair is the most effective method, with effectiveness contingent on the reliability of the diagnosis function. Across both domains and both models, under our full repair system, rules that fail the equivalence check show 1.4x-2.5x more NLI drift than rules that pass it.