Faithful Autoformalization via Roundtrip Verification and Repair
cs.CL, cs.AI
Submitted: 2026-04-27
Updated: 2026-09-21
License: http://creativecommons.org/licenses/by/4.0/
The gist: 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,
Terminology
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 natural language inference (NLI) drift than rules that pass it.
Sources
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
- Unsupervised Evaluation of Code LLMs with Round-Trip Correctness
- Teaching Large Language Models to Self-Debug
- Herald: A Natural Language Annotated Lean 4 Dataset
- SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Models
- TR2MTL: LLM based framework for Metric Temporal Logic Formalization of Traffic Rules
- On Faithfulness and Factuality in Abstractive Summarization
- ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
- Multilingual Mathematical Autoformalization
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
- Process-Driven Autoformalization in Lean 4
- Clover: Closed-Loop Verifiable Code Generation
- Autoformalization with Large Language Models
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
- LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
- MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
Related papers
- Exploring Solution Divergence and Its Effect on Large Language Model Problem Solving
- Ishigaki-IDS-Bench: A Benchmark for Generating Information Delivery Specification from BIM Information Requirements
- Subliminal Steering: Stronger Encoding of Hidden Signals
- MedStruct-S: A Benchmark for Key Discovery, Key-Conditioned QA and Semi-Structured Extraction from OCR Clinical Reports
- The End of Transformers? On Challenging Attention and the Rise of Sub-Quadratic Architectures
- Untangling the Mechanisms of Misleading Context in Medical Question Answering