# Faithful Autoformalization via Roundtrip Verification and Repair

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 52 references that are in the map.
- First posted on arXiv 27 Apr 2026.

## Builds on (most cited first, 28 of 28)

- [BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension](https://mlsanity.com/paper/1910.13461/) (2019)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [A Broad-Coverage Challenge Corpus for Sentence Understanding through Inference](https://mlsanity.com/paper/1704.05426/) (2017)
- [FActScore: Fine-grained Atomic Evaluation of Factual Precision in Long Form Text Generation](https://mlsanity.com/paper/2305.14251/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [On Faithfulness and Factuality in Abstractive Summarization](https://mlsanity.com/paper/2005.00661/) (2020)
- [Right for the Wrong Reasons: Diagnosing Syntactic Heuristics in Natural Language Inference](https://mlsanity.com/paper/1902.01007/) (2019)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [SummaC: Re-Visiting NLI-based Models for Inconsistency Detection in Summarization](https://mlsanity.com/paper/2111.09525/) (2021)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Can GPT-3 Perform Statutory Reasoning?](https://mlsanity.com/paper/2302.06100/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [A Dataset for Statutory Reasoning in Tax Law Entailment and Question Answering](https://mlsanity.com/paper/2005.05257/) (2020)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Revisiting Round-Trip Translation for Quality Estimation](https://mlsanity.com/paper/2004.13937/) (2020)
- [Unsupervised Evaluation of Code LLMs with Round-Trip Correctness](https://mlsanity.com/paper/2402.08699/) (2024)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [TR2MTL: LLM based framework for Metric Temporal Logic Formalization of Traffic Rules](https://mlsanity.com/paper/2406.05709/) (2024)

## Built on by (most cited first, 8 of 8)

- [Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning](https://mlsanity.com/paper/2606.16118/) (2026)
- [AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis](https://mlsanity.com/paper/2607.03656/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [Neurosymbolic Auditing of Natural-Language Software Requirements](https://mlsanity.com/paper/2605.13817/) (2026)
- [EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2609.00032/) (2026)
- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)
- [Natural Language to First-Order Logic LLM-based Autoformalization](https://mlsanity.com/paper/2610.12030/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)

## Abstract (arXiv)

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 natural language inference (NLI) drift than rules that pass it.