Reproduce “FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh, Shuqi Liu, Qiyuan Xu, Haoxuan Yin, Dominik Wagner, Wenda Li and 2 more
FaithformBench tests whether autoformalisation preserves errors when translating mathematical reasoning into Lean. It translates original and perturbed steps, then uses a prover to check each statement and its negation. This detects error induction and silent correction, but can miss semantic drift or leave cases inconclusive. On Omni-MATH, Goedel’s UFLB is 0.21 versus Claude Opus 4.7’s 0.14; UFLB is a lower bound.
Key insights
- A fundamental tension exists where AF systems most effective at preserving validity for correct inputs are simultaneously most prone to "silent correction" of errors in invalid inputs.
- Specialized autoformalisers frequently exhibit high rates of "sycophancy," transforming incorrect natural language steps into provable formal statements rather than reflecting their invalidity.
- Frontier general-purpose Large Language Models (LLMs) demonstrate better "invalidity preservation" and overall faithfulness compared to fine-tuned, specialized AF models.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.