Summary

• FaithformBench is a novel benchmark for evaluating the faithfulness of autoformalisation (AF) systems—systems that translate natural-language reasoning steps into formal statements for proof assistants like Lean.
• The key innovation is a perturbation-based methodology: automatically generating invalid variants of valid reasoning steps, then checking whether the AF system preserves validity (on unperturbed steps) and invalidity (on perturbed steps).
• The benchmark is cheap to apply (no human-annotated ground truth required), sound under weak assumptions (relies on a trusted proof assistant rather than LLM judges), and assesses both positive and negative examples.
• Evaluation of 8 AF systems (4 specialised, 4 general-purpose) reveals pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements, with the most validity-preserving fine-tuned models also being the most sycophantic.
• A tension exists between validity preservation and invalidity preservation in current AF systems, posing a critical pitfall for chain-of-thought (CoT) verification applications.

Introduction and Theoretical Foundation

Background and Motivation: Autoformalisation (AF) systems translate natural-language reasoning steps into formal mathematical statements verifiable by proof assistants such as Lean, Rocq, and Isabelle. There is growing interest in using AF to verify the chain-of-thought (CoT) reasoning of LLMs, where each step is formalised and checked individually. For these use-cases, faithfulness—the formal statement's meaning matching the original natural language—is crucial.

Existing Approaches and Limitations:

1. Human-annotated ground truth datasets (e.g., BEq, GTED): reliable but slow and expensive.
2. LLM judges or embedding models (e.g., ProofBridge): fast and scalable but with no guarantees of accuracy, and can miss subtle errors.

Both approaches typically assume inputs are correct, failing to test whether the AF system preserves errors in incorrect statements—essential for CoT verification where the goal is to identify incorrect reasoning steps.

Theoretical Foundation: The paper formalises faithfulness through two key conditions:

• Validity preservation: If input $x$ is valid, then $\mathsf{AF}(x)$ should be true.
• Invalidity preservation: If input $x$ is invalid, then $\mathsf{AF}(x)$ should be false.

Two primary failure modes are identified:

1. Error induction: valid input maps to a false formal statement.
2. Silent correction: invalid input maps to a true formal statement.

The methodology leverages the Lean kernel as a trusted verifier: to check if a formal statement is true, try to find a proof; to check if it is false, try to refute it by finding a proof of its negation.

Methodology

Formal Framework: An AF system takes a reasoning step $x$ (a natural-language string) and produces a sequent:

$$\phi_{1}, \dots, \phi_{n} \vdash \psi, \tag{2}$$

where $\phi_1, \dots, \phi_n$ are premises (typing or propositional assumptions) and $\psi$ is the conclusion. For example:

$$a, b, c: \mathbb{R}, a > b, b > c \vdash a > c. \tag{3}$$

Perturbation Function: A function $\text{Pert}$ takes a reasoning step $x$ and returns a slightly modified version $\text{Pert}(x)$ designed to be invalid. The method assumes:

• (8) A high proportion of the original $x_i$ are valid.
• (9) A high proportion of the perturbed $\text{Pert}(x_i)$ are invalid.

Prover Component: A prover $\text{Prove}$ takes a formal statement $y$ and returns:

• $\top$: finds a proof of $y$
• $\perp$: refutes $y$ (finds a proof of its negation)
• $\emptyset$: fails to find either (timeout or syntactic failure)

Failure Statistics: For each input $x_i$, compute:

$$\bar{x}_i := \text{Pert}(x_i), \quad z_i := \text{Prove}(\mathsf{AF}(x_i)), \quad \bar{z}_i := \text{Prove}(\mathsf{AF}(\bar{x}_i))$$

The key metrics are:

$$\text{FNR} := \frac{\#\{i \mid z_i = \bot\}}{N} \quad \text{FPR} := \frac{\#\{i \mid \bar{z}_i = \top\}}{N}$$ $$\text{AFFR} := \frac{\#\{i \mid \mathsf{AF}(x_i) = \emptyset\} + \#\{i \mid \mathsf{AF}(\bar{x}_i) = \emptyset\}}{2N}$$

where FNR = false negative rate (error induction), FPR = false positive rate (silent correction), AFFR = autoformalisation failure rate.

Unfaithfulness Lower Bound (UFLB): An aggregate statistic:

$$\text{UFLB} = \frac{1}{2}\text{FNR} + \frac{1}{2}\text{FPR} + \text{AFFR}$$

Under assumptions (8) and (9), each failure event implies unfaithfulness, so UFLB estimates a lower bound on the proportion of inputs where the AF is unfaithful.

Contingency Analysis: Pairs $(z_i, \bar{z}_i)$ are classified into five categories:

1. Faithfulness: $z_i = \top$, $\bar{z}_i = \perp$ (desired outcome)
2. Sycophancy: $z_i = \bar{z}_i = \top$ (silently corrects invalid inputs)
3. Abstention: $z_i = \bar{z}_i = \perp$
4. Inversion: $z_i = \perp$, $\bar{z}_i = \top$ (rare)
5. Inconclusive: $z_i = \emptyset$ or $\bar{z}_i = \emptyset$

Dataset Construction: From ProcessBench (3,400 reasoning chains), the error-free subset (1,179 chains) was selected. Chains were converted to DAGs, and each node with its parents formed an individual reasoning step, yielding 12,784 reasoning steps across four datasets of increasing difficulty: GSM8K, MATH, OlympiadBench, and Omni-MATH.

Empirical Validation / Results

Perturbation Validation: LLM judges rated perturbations as effective in 97.8% of cases. Human agreement with GPT-5.2 was 95.9% overall (90.0% GSM8K, 98.6% MATH, 95.5% OlympiadBench, 95.1% OmniMATH).

Specialised AF Results (Goedel, Herald, Kimina, StepFun):

General-Purpose LLM Results (Claude Opus 4.7, GPT 5.2, Gemini 3.1 Pro, Qwen Plus):

• All frontier models exhibit lower sycophancy than specialised AFs.
• Claude Opus 4.7 and Gemini 3.1 Pro improve on Goedel's UFLB on every dataset, driven primarily by substantially lower FPR.
• Frontier models achieve uniformly better invalidity preservation than specialised AFs.

Contingency Analysis (Goedel example):

• Faithfulness and Sycophancy categories capture the vast majority of cases.
• Both tend to decrease together as dataset difficulty increases.
• Abstention and Inversion are edge cases across all models.

Theoretical and Practical Implications

Key Finding—The Validity-Sycophancy Tension: The paper reveals a fundamental tension in current AF training: systems best at preserving validity on correct inputs are also the most prone to silent correction on incorrect ones. This suggests that AF pipelines implicitly conflate faithful translation with producing a provable statement.

Implications for CoT Verification: This tension poses a critical pitfall for CoT verification applications, where incorrect inputs are precisely the cases of interest. A system that silently corrects errors fails to flag invalid reasoning steps, defeating the purpose of verification.

Methodological Contributions:

• The perturbation-based approach offers a middle ground between expensive human annotation and unreliable neural judges.
• Soundness under weak assumptions: if a model fails the benchmark, we can be confident a failure mode is present.
• The method is incomplete (does not detect semantic drift in full generality) but provides valuable diagnostic information.

Practical Recommendations:

• Train AF systems with deliberate exposure to invalid inputs so they learn to preserve errors rather than repair them.
• Extend the perturbation-based methodology to other natural-to-formal translation tasks (e.g., formal specifications, code-from-spec) where silent correction has similar costs.
• Use FaithformBench as one diagnostic measure among others, not as a complete certificate of reliability.

Conclusion

FaithformBench provides a scalable, sound, and comprehensive methodology for benchmarking the faithfulness of autoformalisation systems, addressing the critical gap of testing how AFs handle invalid inputs. The benchmark of 12,784 reasoning steps across four mathematical datasets reveals pervasive sycophancy in specialised AFs, with the most validity-preserving models being the most prone to silent correction. Frontier general-purpose models demonstrate lower sycophancy, suggesting potential directions for improvement.

Future Directions:

1. Training AF systems with deliberate exposure to invalid inputs to learn error preservation.
2. Extending perturbation-based methodology to other translation tasks.
3. Addressing the incompleteness of the method regarding semantic drift detection.

Limitations: The method does not assess semantic drift in full generality; UFLB being small does not guarantee faithfulness. The method relies on a strong prover; a weak prover may return inconclusive results. FaithformBench should be used as one diagnostic measure among others, not as a complete certificate of reliability.