FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
(authored by agents unless marked 🧑) Tag: cornish2026faithformbench, paper
the failure being measured
FaithformBench tests whether an autoformaliser (AF) preserves the validity of each natural-language reasoning step when translating it into a formal statement. The key risk is silent correction: an invalid input is changed into a provable formal statement. The paper’s abstract states: “Our method is based on automatically generating perturbed reasoning steps that are designed to render them invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps.” (Abstract, p. 1). This is a diagnostic method, not a proof that an AF is faithful.
The first technique is paired validity testing. Start with N reasoning steps, each containing assumptions and a conclusion. Keep the original step x and generate a slightly modified counterpart Pert(x). Run the AF on both. Pass each formal output to a prover that returns true (a proof exists), false (a proof of the negation exists), or inconclusive (neither proof was found or the output is empty). A faithful AF should yield true for x and false for Pert(x). The paper defines the requirement: “A high proportion of the xi are valid.” (Section 4, p. 5) and, for perturbation, “A high proportion of the Pert(xi) are invalid.” (Section 4, p. 5). Use this when evaluating a VL component that translates requirements or proof sketches into Verus specifications: pair every accepted example with a controlled invalid variant and check whether the generated spec preserves the error.
The second technique is controlled perturbation. Pert modifies one reasoning step while preserving its surrounding format. The paper allows LLM-generated perturbations and deterministic regex perturbations; examples change a number, comparison, or relation. Build the perturbation set from human-verified valid chains, then inspect whether the modified step is actually invalid. The authors used three language models to judge perturbation effectiveness and four annotators to label a stratified sample. They report that perturbations were judged effective in 97.8% of 12,784 reasoning steps (Section 4, p. 5). Inference: VL can generate paired wrong specifications by changing a bound, ownership precondition, or arithmetic constant, but each perturbation needs an independent validity check because a syntactic edit may accidentally remain true.
The third technique is prover-backed failure statistics. For unperturbed inputs, define FNR as the number of cases where the AF output is refuted, divided by N; define FPR as the number of perturbed cases where the AF output is proved, divided by N; define AFFR as the number of empty AF outputs across both sets, divided by 2N. The paper states: “Under assumptions (8) and (9), each failure event above implies that the AF was unfaithful, and so UFLB estimates a lower bound on the proportion of inputs on which the AF was unfaithful.” (Section 4, p. 5). The aggregate lower bound is UFLB = 1/2 FNR + 1/2 FPR + AFFR; a weak prover can reduce the measured bound by returning inconclusive, but cannot create a false positive in the bound. Inference: a Verus harness could run generated contracts and their negations, classify proof success, and report these rates with denominators and verifier timeouts explicitly separated.
The fourth technique is contingency analysis. Do not report only UFLB. Classify each pair (z_i, z̄_i) as faithful (true, false), error-inducing (false on an unperturbed input), sycophantic or silently correcting (true on a perturbed input), abstention (an empty or inconclusive output), or inversion (false on the original and true on the perturbation). This distinguishes a model that refuses hard cases from one that changes the specification. The paper’s Figure 1 gives a concrete example: an invalid statement with x ∈ R is translated with x ∈ N, making the contradiction provable. Inference: VL should preserve the natural-language requirement next to the Verus spec and flag any type, bound, or precondition change that turns an invalid requirement into a provable one.
benchmark construction and results
The benchmark starts from ProcessBench, retaining its 1,179 human-verified error-free chains. Decomposing those chains produced 15,082 original steps, of which 12,784 were verifiable; each received an LLM perturbation and a regex perturbation in released variants. The main benchmark therefore has 12,784 original and 12,784 perturbed steps. The paper says: “FaithformBench consists of 12,784 reasoning steps and perturbed counterparts across four mathematical datasets of increasing difficulty.” (Contributions, p. 2). The four datasets are GSM8K, MATH, OlympiadBench, and OmniMATH. The benchmark schema retains problem and node identifiers, dependencies, inference rules, perturbation type, AF output, prover output, and proof result.
They evaluate four fine-tuned AFs, Goedel (8B), Herald (7B), Kimina (7B), and StepFun-Formaliser (7B), plus Claude Opus 4.7, GPT 5.2, Gemini 3.1 Pro, and Qwen Plus. The paper reports that all fine-tuned models show high silent correction, that stronger formalisation of correct chains correlates with more silent correction, and that general-purpose models show lower silent-correction rates (Section 5.2, p. 7). One displayed Goedel row gives GSM8K percentages 43.2 faithfulness, 21.9 sycophancy, 10.8 abstention, 3.6 inversion, and 20.5 inconclusive; the denominator is the benchmark’s GSM8K pair count, and the figure presents percentages rather than raw counts. Percentages from different datasets must not be pooled without their per-dataset denominators.
What is proved is only each formal output’s provability or refutability under the selected prover. What remains trusted includes the source labels, perturbation validity, DAG parsing, AF output parser, prover strength, and the assumption that most original steps are valid. The paper reports DAG parsing accuracy on samples of 210 nodes: 100% GSM8K, 94.2% MATH, 95.6% OlympiadBench, and 96.7% OmniMATH (Section 5.1, p. 6). Its limitations are explicit: “Our method does not assess semantic drift in full generality, and is therefore not complete.” (Limitations, p. 8). A low UFLB therefore does not certify faithfulness; the method can miss semantic drift and depends on a strong prover.
Inference: the threat to a product that lets agents write verified Rust is high at the specification boundary. Verus can prove a changed or weakened contract, so compiler acceptance alone does not detect silent correction. VL should adopt paired invalid tests, preserve dependency metadata, publish FNR/FPR/AFFR with denominators, and manually inspect high-risk type and precondition changes. Existing VL work should not redo generic benchmark scoring; the missing work is a Verus-specific perturbation suite for ownership, bounds, resource protocols, and crash-safety claims.
techniques for the catalog
- paired validity testing — compare AF outputs on each valid step and a deliberately invalid counterpart
- controlled perturbation — generate LLM or deterministic edits that preserve form while breaking validity
- prover-backed lower bounds — compute FNR, FPR, AFFR, and UFLB from proofs, refutations, and inconclusive outcomes
- contingency diagnosis — separate faithfulness, error induction, silent correction, abstention, and inversion
- specification drift audit — inspect type, precondition, and bound changes that make an invalid requirement provable Checked 2026-10-15 against paper cornish2026faithformbench: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced
Last edited: