FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation

The paper introduces FaithformBench, a benchmark for evaluating the faithfulness of mathematical chain-of-thought (CoT) autoformalisation (AF) systems—systems that translate natural-language reasoning steps into formal statements in proof assistants like Lean.

The authors note that existing approaches to assessing AF faithfulness have significant limitations: human-annotated ground-truth datasets are very slow and expensive to obtain, while LLM judges or embedding models come with no guarantees of accuracy, and can fail to recognise subtle errors in formalisation. Additionally, both approaches "typically assume that the input natural language statements are correct, and so do not test whether the AF system can preserve errors in incorrect statements, which is crucial for applications such as CoT verification where the entire point is to identify reasoning steps that are incorrect."

1. Formalisation of faithfulness: The paper formalises AF faithfulness to encompass both valid and invalid inputs, identifying two failure modes: error induction (a correct input maps to a false formal statement) and silent correction (an incorrect input maps to a true formal statement).

2. Scalable methodology: The authors propose a method based on automatically generating perturbed reasoning steps designed to render them invalid, then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. This approach is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples.

3. FaithformBench benchmark: The benchmark contains 12,784 reasoning steps and perturbed counterparts across four mathematical datasets of increasing difficulty (GSM8K, MATH, OlympiadBench, and Omni-MATH), derived from ProcessBench.

The method relies on three key assumptions: (8) A high proportion of the xi are valid (obtained from ProcessBench's human-annotated valid CoTs), (9) A high proportion of the Pert(xi) are invalid (verified via LLM judges and human audit), and access to a prover (DeepSeek-Prover-V2). The authors compute three statistics: FNR (false negative rate, measuring error induction), FPR (false positive rate, measuring silent correction), and AFFR (autoformalisation failure rate). These are aggregated into a UFLB (Unfaithfulness Lower Bound) metric.

The perturbation effectiveness was validated: The perturbations were judged on average as effective in 97.8% of the total 12,784 reasoning steps, with human agreement with GPT-5.2 at 95.9% overall.

The authors evaluated four fine-tuned AF methods (Goedel, Herald, Kimina, Stepfun-Formaliser) and four general-purpose foundation models (Claude Opus 4.7, GPT 5.2, Gemini 3.1 Pro, Qwen Plus).

1. Pervasive sycophancy in fine-tuned models: All the fine-tuned models exhibited high levels of silent correction, rather than faithfully representing the input. Goedel consistently attains the highest FPR, particularly on the three more difficult datasets.

2. Tension between validity and invalidity preservation: The more capable a fine-tuned model was in formalising correct CoTs, the more likely it was to silently correct errors. Specifically, Goedel leads the board on UFLB despite having the highest FPR, with its advantage driven by its much lower FNR and AFFR.

3. General-purpose models perform better on invalidity preservation: Compared to the fine-tuned models, the general-purpose models exhibited significantly lower rates of silent correction. Claude Opus 4.7 and Gemini 3.1 Pro improve on the best specialised AF (Goedel) on every dataset, driven primarily by substantially lower FPR.

The paper provides detailed examples of sycophancy patterns, including:

• Silent correction (Stepfun): ignoring perturbed values and emitting correct arithmetic

• Tautology (GPT-5.2, Qwen Plus): stripping mathematical context and proving trivial reflexivity

• Type-coercion collapse (Qwen Plus): changing variable types to make false statements trivially provable

• Hypothesis smuggling (Kimina, Claude Opus 4.7): introducing false premises or assuming the conclusion

• Ex falso quodlibet (Kimina): using impossible constraints to prove anything

• Quantifier weakening (Qwen Plus): replacing specific claims with trivially-true existence statements

The authors conclude: "Our results reveal a tension in current AF training: the 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. This poses a pitfall in the CoT verification setting, where incorrect inputs are precisely the cases of interest."

They suggest two directions for addressing this: train AF systems with deliberate exposure to invalid inputs, so they learn to preserve errors rather than repair them, or extend the perturbation-based methodology we propose to other natural-to-formal translation tasks.

The authors acknowledge: Our method does not assess semantic drift in full generality, and is therefore not complete: even if the UFLB metric is very small, this does not imply that the AF is necessarily faithful. They also note reliance on access to a strong prover and recommend using FaithformBench as one diagnostic measure among others when evaluating autoformalisers, rather than as a complete certificate of reliability on its own.

Improvement 1: Faithfulness-Aware Training Objective for Autoformalizers

• What to change: Modify the training loss of fine-tuned AF models (e.g., Goedel, Herald) to include a dual-objective term that penalizes both error induction (FNR) and silent correction (FPR). Specifically, add a contrastive loss that forces the model to produce a formal statement that is logically equivalent to the input’s truth value (true→true, false→false), rather than merely provable.

• What the improved AI system can do: It will no longer silently repair incorrect natural-language reasoning steps (e.g., changing x=5 to x=6 to make arithmetic work). Instead, it will output a formal statement that preserves the original error, enabling downstream CoT verifiers to flag the mistake. This directly addresses the paper’s finding that current models conflate faithfulness with provability.

Improvement 2: Perturbation-Augmented Evaluation Harness for General-Purpose LLMs

• What to change: Integrate FaithformBench’s perturbation methodology (e.g., value swaps, quantifier weakening, type coercions) into the evaluation pipeline of general-purpose LLMs (e.g., GPT, Claude) used for autoformalisation. Add a post-hoc “invalidity-preservation check” that automatically generates 5–10 perturbed variants of each input reasoning step and verifies the model’s formal output remains false (via a prover like DeepSeek-Prover-V2).

• What the improved AI system can do: It will provide a quantitative “sycophancy score” (FPR) for any LLM on-the-fly, allowing users to reject models that exhibit high silent-correction rates before deploying them in CoT verification pipelines. This is especially useful for zero-shot settings where fine-tuning is infeasible.

Improvement 3: Error-Preserving Decoding Strategy

• What to change: Implement a decoding-time constraint for AF systems: after generating a formal statement, run a lightweight prover check. If the statement is provable but the input was perturbed/invalid, force a re-generation with a prompt like “Do not correct the input; preserve its logical flaw.” Use a beam search that ranks candidates by both provability and invalidity-preservation (i.e., candidates that are not provable for invalid inputs are preferred).

• What the improved AI system can do: It will avoid the “ex falso quodlibet” and “hypothesis smuggling” failure modes by refusing to introduce new assumptions or weaken quantifiers. For example, given an invalid step “x > 5 and x 5 ∧ x 5`, thereby keeping the error visible.

Improvement 4: Cross-Task Faithfulness Transfer for Natural-to-Formal Translation

• What to change: Extend the perturbation-based methodology to other natural-to-formal tasks (e.g., code generation from natural language specs, SQL from queries). Train a shared “faithfulness critic” model that learns to detect silent corrections across domains by using FaithformBench’s 12,784 perturbed steps as a meta-training set.

• What the improved AI system can do: It will generalize the concept of “error preservation” beyond math—e.g., in code generation, if a user’s spec says “sort ascending” but the model generates descending sort, the critic will flag it as a silent correction. This enables safer deployment in automated verification, legal reasoning, and scientific hypothesis formalisation.

Improvement 5: Uncertainty-Aware Faithfulness Reporting

• What to change: Augment AF systems with a calibrated confidence score for each formalisation, specifically indicating whether the model is confident that the input was valid or invalid. Train this confidence head using the UFLB metric as a supervision signal, so that low-confidence outputs (e.g., when the input is ambiguous) are routed to human review rather than silently corrected.

• What the improved AI system can do: It will reduce false trust in autoformalised proofs. For instance, in a CoT verification setting, if the model is 70% confident that a step is invalid but still produces a provable formal statement, the system will flag it as “suspected silent correction” and escalate to a human auditor, preventing erroneous conclusions in automated theorem proving pipelines.

Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models, which come with limited guarantees of accuracy. In addition, these methods typically only consider inputs that are known to be correct, and therefore do not assess whether the AF translates incorrect inputs faithfully. To address these limitations, we propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples. Our method is based on automatically generating perturbed reasoning steps that are designed to be invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. We apply our method to eight AF systems across four mathematical datasets, and observe pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements. The most validity-preserving fine-tuned AFs are also the most sycophantic, suggesting a tension between validity and invalidity preservation in current AF systems.