---
kind: concept
slug: autoformalization
title: Autoformalization
summary: >-
  Translating a reasoning step or statement into a formal language a proof checker can read, here Lean. The check that matters is faithfulness: valid steps must stay valid and invalid steps must stay invalid. Measured by asking a prover to prove the output or its negation. One author-reported paper; fine-tuned and prompted frontier formalisers differ in how often they silently correct wrong steps.
tags: [formal-verification, lean, evaluation, chain-of-thought]
papers: ["2608.10916"]
related: [sycophancy, llm-as-a-judge, benchmark-validity, chain-of-thought]
status: draft
updated_at: 2026-11-08
---

## 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
[arxiv: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 [arxiv:2608.10916 §1].

The shared invariant is that the formal output has the same logical meaning as
its input [arxiv: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 [arxiv: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 [arxiv: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 [arxiv: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 [arxiv:2608.10916 §4].

## Variants

The paper compares two groups of formaliser. Both are scored with the same
prover and the same test set [arxiv: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
[arxiv:2608.10916 §6] [app. F]. Card: [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](/papers/2608.10916).

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 [arxiv: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
[arxiv: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](/papers/2608.10916).

All four show less sycophancy than the fine-tuned group [arxiv: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 [arxiv: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.

| Situation | Use | Why |
|---|---|---|
| The verifier must not quietly fix wrong steps | A prompted frontier model, such as Claude Opus 4.7 or Gemini 3.1 Pro | Lowest UFLB of the eight, mainly through lower silent correction [arxiv:2608.10916 §6.2] |
| You cannot call a hosted frontier model | A fine-tuned model; Goedel if you want the lowest UFLB in that group | Best of the fine-tuned four on the bound, but it has the highest silent correction in the group [arxiv:2608.10916 §6.1] |
| You care most about valid steps staying valid | Look at the error-induction rate, but also measure silent correction | Goedel is strongest on error induction and weakest on silent correction, so one rate alone can mislead [arxiv:2608.10916 §1] [§6.1] |
| You have no formaliser and want a cheap check | Do not use an LLM judge or embedding match as a faithfulness test | The paper says both assume the input is correct, so neither tests whether a wrong input stays wrong [arxiv:2608.10916 §1] |
| Your prover is weaker than DeepSeek-Prover-V2 | Expect more inconclusive results, and read them with care | All reported results use DeepSeek-Prover-V2 with pass@2. A weaker prover can leave faulty formalisers inconclusive [arxiv:2608.10916 app. A] [§ Limitations] |

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
  [arxiv:2608.10916 §4].
- UFLB is a lower bound. Prover failures can only lower it, and it does not
  detect semantic drift [arxiv:2608.10916 §4] [§ Limitations].
- Frontier results depend on decoding settings that the paper does not state
  [arxiv: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
[arxiv:2608.10916 §4].

```pseudocode
# 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 [arxiv: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 [arxiv: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/2608.10916).

## Papers

- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](/papers/2608.10916): a benchmark and metric for whether Lean formalisers keep valid steps valid and invalid steps invalid, comparing four fine-tuned and four frontier formalisers.