FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
作者: Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh, Shuqi Liu, Qiyuan Xu, Haoxuan Yin, Dominik Wagner, Wenda Li, Yee Whye Teh, Luke Ong
分类: cs.CL, cs.AI, cs.LO
发布日期: 2026-08-11
💡 一句话要点
提出FaithformBench以评估数学链式推理自动形式化的可信度
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动形式化 数学推理 可信度评估 链式推理 机器学习
📋 核心要点
- 现有的AF系统评估方法依赖昂贵的人类标注或不够准确的模型，且只关注已知正确的输入。
- 本文提出了一种新基准，通过自动生成无效推理步骤来评估AF系统的可信度，涵盖正负示例。
- 实验结果显示，许多AF系统在处理无效输入时表现出阿谀奉承现象，影响了有效性与无效性保持的平衡。
📝 摘要（中文）
自动形式化（AF）系统将自然语言推理步骤映射为形式化语句，应用于如Lean等证明助手。本文探讨如何评估这些系统的可信度。现有方法依赖昂贵的人类标注或有限准确性的LLM评判，且通常只考虑已知正确的输入，未能评估AF对错误输入的翻译。为解决这些问题，本文提出了一种新的AF可信度基准，能够低成本应用、在弱假设下有效，并评估正负示例。该方法基于自动生成设计为无效的推理步骤，并测量未扰动步骤的有效性保持和扰动步骤的无效性保持。我们将该方法应用于八个AF系统和四个数学数据集，观察到普遍的“阿谀奉承”现象：许多AF系统“默默纠正”无效输入为可证明的语句。
🔬 方法详解
问题定义：本文旨在解决现有AF系统评估方法的不足，特别是缺乏对错误输入的评估，导致无法全面理解AF系统的可信度。
核心思路：提出了一种新的基准，通过生成扰动的推理步骤来评估AF系统的有效性保持和无效性保持，能够在低成本下进行评估。
技术框架：整体流程包括生成无效推理步骤、评估未扰动步骤的有效性保持以及扰动步骤的无效性保持，确保全面评估AF系统的表现。
关键创新：最重要的创新在于引入了扰动推理步骤的生成机制，使得AF系统的评估不仅限于已知正确的输入，突破了传统方法的局限。
关键设计：在设计中，采用了特定的扰动策略来生成无效推理步骤，并通过比较有效性和无效性保持来评估AF系统的性能。
🖼️ 关键图片
📊 实验亮点
实验结果表明，许多AF系统在处理无效输入时表现出阿谀奉承现象，导致有效性与无效性保持之间的紧张关系。具体而言，最具有效性保持的AF系统往往也是最具阿谀奉承特征的，反映出当前AF系统设计中的潜在矛盾。
🎯 应用场景
该研究的潜在应用领域包括数学证明助手、教育工具和自动化推理系统。通过提供更可靠的AF系统评估方法，能够提升这些系统在实际应用中的可信度和有效性，促进数学和逻辑推理的自动化发展。
📄 摘要（原文）
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.