🤖 AI

Faithful Autoformalization via Roundtrip Verification and Repair

This paper proposes a roundtrip verification framework that ensures faithful natural language-to-formal translation by iteratively translating back to natural language, checking for logical equivalence, and applying diagnosis-guided scoped repairs to correct errors without requiring ground-truth annotations.

Original authors: Daneshvar Amrollahi, Jerry Lopez, Clark Barrett

Published 2026-05-12

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Daneshvar Amrollahi, Jerry Lopez, Clark Barrett

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to translate a complex legal rule from English into a strict, computer-readable language (like a secret code). You ask a super-smart AI to do this translation. But how do you know the AI didn't accidentally change the meaning of the rule while translating it?

This paper proposes a clever "translation check" system that doesn't need a human expert to hold the answer key. Instead, it uses a Roundtrip Verification method.

Here is how it works, using a simple analogy:

The "Roundtrip" Game

Think of the process like a game of "Telephone," but with a twist:

The Forward Trip (Translation): You give the AI a natural language rule (e.g., "No cars over 3 tons can enter the park"). The AI translates this into a strict logical code (Stage 1).
The Back Trip (Reverse Translation): The AI takes that logical code and translates it back into plain English (Stage 2).
The Re-Forward Trip (Re-Translation): The AI takes this new English sentence and translates it back into logical code again (Stage 3).

The Check: The system now compares the First Code (from step 1) with the Second Code (from step 3).

If they match perfectly: The AI likely got the meaning right. It's a "faithful" translation.
If they don't match: Something went wrong. The meaning drifted somewhere along the line.

The "Doctor" and the "Scalpel"

When the two codes don't match, a naive approach would be to just tell the AI, "Try again from the start!" and hope for the best. This paper argues that's wasteful.

Instead, they use a Diagnosis and Repair system:

The Doctor (Diagnosis): A special AI "judge" looks at the four pieces of the puzzle (Original Text, First Code, Back-Translated Text, Second Code) to figure out exactly which step broke the meaning. Did it mess up the first translation? Did it misunderstand the back-translation?
The Scalpel (Scoped Repair): Once the doctor identifies the specific broken step, the system only fixes that one part. It doesn't throw away the whole work; it just performs surgery on the faulty step and re-runs the rest of the chain.

The Real-World Test

The researchers tested this on two sets of Texas laws:

Traffic Laws: Rules about driving, speed limits, and school buses.
Wildlife Laws: Rules about hunting, fishing, and protected animals.

They used two different powerful AI models (Claude and GPT) to see if this system worked.

Key Findings (The "So What?")

The Check Works: When the system says the two codes match (Formal Equivalence), it is a very strong signal that the meaning hasn't drifted. When the codes don't match, the meaning is almost certainly wrong.
Fixing the Right Thing Matters: The most successful method wasn't just "trying again." It was using the "Doctor" to find the specific broken step and using the "Scalpel" to fix only that step.
The Bottleneck: The system works best when the "Doctor" (the diagnosis step) is reliable.
- When they used the Claude model to act as the doctor, the system was fast and accurate.
- When they used the GPT model as the doctor, it kept blaming the first step for every error, even when it wasn't the first step's fault. This made the system slow and inefficient.
- The Fix: They found that if they kept GPT for the heavy lifting (translation) but swapped in Claude just to act as the doctor, the system became fast and accurate again.

The Bottom Line

This paper shows that you can verify if an AI is faithfully translating complex rules without needing a human to check every single answer. By translating back and forth and fixing only the specific broken links in the chain, you can get much more reliable results.

Important Note: The authors explicitly warn that even with this system, the output should not be used for safety-critical tasks (like autonomous driving or medical devices) without a human expert reviewing it first. It's a great tool for checking consistency, but not a magic guarantee of absolute truth.

Technical Summary: Faithful Autoformalization via Roundtrip Verification and Repair

Problem Statement
The paper addresses a critical gap in autoformalization: the lack of a reliable method to verify whether a Large Language Model (LLM) has faithfully captured the semantic meaning of a natural language statement when translating it into a formal, machine-checkable representation. Existing evaluation methods rely on syntactic validity or downstream task success, which do not directly test semantic fidelity. Furthermore, when errors occur, current repair strategies are limited to end-to-end regeneration, lacking the ability to diagnose where in the translation pipeline the meaning was lost. This is particularly challenging in domains like statutory law, where ground-truth formalizations are unavailable.

Methodology
The authors propose a Roundtrip Verification and Scoped Repair Framework that operates without ground-truth annotations. The core mechanism involves a three-stage translation pipeline:

T1 (Autoformalization): Translates natural language input $x$ into a formal expression $y_{orig}$ in a target formalism $\Sigma$ .
T2 (Back-translation): Translates $y_{orig}$ back into natural language $x'$ .
T3 (Re-formalization): Translates $x'$ back into a formal expression $y_{rt}$ .

Verification: The system checks for logical equivalence between the initial formalization ( $y_{orig}$ ) and the roundtrip formalization ( $y_{rt}$ ) using a formal tool (specifically an SMT solver in the experiments). If $y_{orig} \equiv_\Sigma y_{rt}$ , the pipeline is considered self-consistent.

Diagnosis and Repair: When equivalence fails, the framework employs a stage-based diagnosis procedure. An LLM judge examines the artifacts ( $x, y_{orig}, x', y_{rt}$ ) to identify the first stage where semantic drift occurred (Stage 1, 2, or 3). Crucially, the diagnosis is "scoped," meaning the explanation is constrained to artifacts relevant only to that specific stage.

Scoped Repair: Instead of regenerating the entire pipeline, a targeted repair operator ( $R_i$ ) corrects only the identified faulty stage. Downstream stages are then regenerated to maintain pipeline coherence.
Iterative Loop: This process repeats up to a fixed budget ( $K=3$ ) until equivalence is achieved or the budget is exhausted.

Auxiliary Semantic Signal: To evaluate the semantic quality of the formalizations independently of the repair loop, the authors use a bidirectional Natural Language Inference (NLI) model. This serves as a post-hoc diagnostic to measure "drift" (e.g., contradictions or unrelatedness) between the original text and the reconstructed text, distinguishing between rules that are formally consistent but semantically drifted.

Key Contributions

Roundtrip Verification Framework: A method to signal the faithfulness of autoformalization without ground-truth formalizations, applicable to any formalism admitting an equivalence check (e.g., SMT, type checkers).
Diagnosis-Guided Scoped Repair: A procedure that localizes errors to specific translation steps, enabling targeted corrections rather than costly full-pipeline regeneration.
Empirical Analysis of Bottlenecks: A study across two statutory domains (Texas Transportation Code and Texas Parks and Wildlife Code) and two model families (Claude Opus 4.6 and GPT-5.2) identifying the diagnosis step as the primary bottleneck for scoped repair, rather than the pipeline or repair operators themselves.

Results
The framework was evaluated on 150 traffic rules and 77 wildlife rules.

Effectiveness of Repair: Diagnosis-guided scoped repair achieved the highest verified-equivalence rates at the lowest cost when the diagnosis function was reliable.
Model Dependency: With Claude performing the pipeline and diagnosis, scoped repair outperformed baselines (no repair, random stage selection, full regeneration). However, with GPT, the diagnosis step was unreliable (heavily biased toward blaming Stage 1), causing scoped repair to underperform and become more expensive than full regeneration.
Cross-Model Intervention: Replacing only the GPT diagnosis step with Claude (while keeping GPT for the pipeline and repair) restored the efficiency and effectiveness of scoped repair, proving the diagnosis function is the critical variable.
Faithfulness Prediction: Formal equivalence is a strong predictor of semantic faithfulness. Rules that passed the equivalence check (UNSAT) showed 1.4× to 2.5× less NLI drift than those that failed (SAT). However, formal equivalence is necessary but not sufficient; approximately 16% of formally equivalent rules still exhibited semantic drift.

Significance and Claims
The paper claims that formal equivalence serves as a practical, ground-truth-free signal for semantic faithfulness in autoformalization. It demonstrates that scoped repair, driven by accurate stage-level diagnosis, is a more cost-effective and efficient strategy than full regeneration. The authors emphasize that the reliability of the diagnosis function is the determining factor for the success of this approach.

The work is modest in its scope, noting that the framework is heuristic and does not guarantee correctness against the original natural language intent (as the pipeline could stabilize at a semantically different fixed point). The authors explicitly state that the system is not suitable for safety-critical applications without independent expert review and that the current evaluation is limited to English statutory text, requiring further study for other genres like code or scientific text.