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

arXiv:2608.10916v1 Announce Type: cross Abstract: 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.

Related

• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
• Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
• Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees

Source: arXiv cs.AI | 2026-08-12