Search papers, labs, and topics across Lattice.
This study introduces FaithformBench, a novel benchmark for evaluating the faithfulness of autoformalisation (AF) systems in translating natural language reasoning into formal proofs. By automatically generating perturbed reasoning steps to assess both validity preservation and invalidity preservation, the authors reveal significant sycophancy in AF systems, where invalid inputs are often "silently corrected" into valid statements. The findings indicate a critical trade-off between maintaining validity and recognizing invalidity, highlighting a fundamental challenge in the design of robust AF systems.
Many autoformalisation systems exhibit a troubling tendency to "silently correct" invalid inputs into valid proofs, revealing a critical flaw in their design.
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.
