Autoformalization

Overview

Autoformalization turns a statement written in natural language into a formal one that a proof assistant can check. In the paper this page is built on, the input is one step of a chain of reasoning and the target language is Lean 2608.10916 §1 §3. The purpose is to verify reasoning step by step. That only works if the translation keeps the meaning of each step, including steps that are wrong 2608.10916 §1.

The shared invariant is that the formal output has the same logical meaning as its input 2608.10916 §3. Faithfulness can fail in four ways. A valid step can come out false (error induction). An invalid step can come out true (silent correction). The meaning can drift without either verdict. Or the formaliser produces no output at all 2608.10916 §3. A proof checker can detect the first two soundly, but it cannot see drift, so any test built on it is partial 2608.10916 §3 § Limitations.

The paper's test needs no human-written reference. It takes a known-valid step, rewrites it so that it becomes false, formalises both versions, and asks a prover to prove or refute each formal statement 2608.10916 §4 §5.2. The results are summarised as an unfaithfulness lower bound (UFLB), built from the error-induction rate, the silent-correction rate and the formaliser's failure rate 2608.10916 §4.

Variants

The paper compares two groups of formaliser. Both are scored with the same prover and the same test set 2608.10916 §6. The paper's own framing is the basis for the grouping here.

Fine-tuned formalisers

Goedel, Herald, Kimina and StepFun-Formaliser, each about 7–8B parameters, run with greedy decoding. They allow up to 16,384 generated tokens, except Herald, which is capped at 2,048 because of its shorter context window 2608.10916 §6 app. F. Card: FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation.

Goedel has the lowest UFLB in this group, and Stepfun comes next. Goedel also has the lowest error-induction rate and the highest silent-correction rate, especially on the three harder datasets. Only Goedel keeps formaliser failures under 10% on those three 2608.10916 §6.1 fig. 3. The paper gives the UFLB values only as bars in a chart, so this page uses the rankings the text states.

Prompted frontier models

Qwen Plus, Gemini 3.1 Pro, GPT 5.2 and Claude Opus 4.7 are used without fine-tuning. Each gets a few-shot prompt: a set of system rules, three worked examples, and an instruction not to correct the input 2608.10916 §6 app. G. The paper does not state their decoding settings app. G. Card: FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation.

All four show less sycophancy than the fine-tuned group 2608.10916 §6.2 fig. 4. Claude Opus 4.7 and Gemini 3.1 Pro have the lowest UFLB of all eight formalisers. Their lead over Goedel holds on every dataset, and it comes mainly from a lower silent-correction rate. They also have a lower failure rate than the fine-tuned models 2608.10916 §6.2.

When to use which

The choice rests on what a wrong step costs you and what you can run. The paper's results support the rows below. The paper does not measure cost or latency, so none of the rows make a claim about them.

Pitfalls the paper names:

• A degenerate formaliser that ignores its input can be labelled faithful by the contingency groups. Read those labels as descriptive, not as guarantees 2608.10916 §4.
• UFLB is a lower bound. Prover failures can only lower it, and it does not detect semantic drift 2608.10916 §4 § Limitations.
• Frontier results depend on decoding settings that the paper does not state 2608.10916 app. G.

Implementation sketch

The core loop is the same for every formaliser. Only the formaliser and the prompt change between variants. The metric definitions follow the paper 2608.10916 §4.

# Faithfulness check for one formaliser  [arxiv:2608.10916 §4]
# Input:  steps (N valid steps), perturb (makes a step false), af, prover
# Output: fnr, fpr, affr, uflb, with rates over the N steps

def faithfulness(steps, perturb, af, prover):
    # One invalid counterpart per valid step  [arxiv:2608.10916 §5.2]
    bad = [perturb(x) for x in steps]
    # Formalise both versions with the same formaliser  [arxiv:2608.10916 §4]
    good_f = [af(x) for x in steps]
    bad_f = [af(x) for x in bad]
    # Prover returns proven, refuted or fail  [arxiv:2608.10916 §4] [app. A]
    good_v = [prover(y) for y in good_f]
    bad_v = [prover(y) for y in bad_f]
    # Error induction: valid step, refuted formalisation  [arxiv:2608.10916 §4]
    fnr = good_v.count("refuted") / len(steps)
    # Silent correction: invalid step, proven formalisation  [arxiv:2608.10916 §4]
    fpr = bad_v.count("proven") / len(steps)
    # Failures pooled over both arms, divided by 2N  [arxiv:2608.10916 §4]
    affr = (good_f.count("fail") + bad_f.count("fail")) / (2 * len(steps))
    # Lower bound on the share of unfaithful outputs  [arxiv:2608.10916 §4]
    uflb = 0.5 * fnr + 0.5 * fpr + affr
    return fnr, fpr, affr, uflb

Where the variants differ is in af: a fine-tuned model with its own decoding cap, or a frontier model with the few-shot prompt 2608.10916 §6 app. F app. G. The paper fixes the prover to DeepSeek-Prover-V2, and it treats a proof that changes the statement as inconclusive [arxiv:2608.10916 app. A] app. B.

Contradictions

None known between papers. This page draws on one card, so there is no second source to disagree with it. The card for this paper records one unresolved gap. The paper reports that 2.2% of perturbations were judged contaminated 2608.10916 §5.2. A comment in the authors' code gives 10.45% for a preliminary single-judge filter. The paper's own text does not reconcile the two, so treat the 2.2% figure as the paper's claim. See the card's Paper vs code section.

Papers

• FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation: a benchmark and metric for whether Lean formalisers keep valid steps valid and invalid steps invalid, comparing four fine-tuned and four frontier formalisers.