FaithformBench：数学链式思维自动形式化的忠实性基准测试
FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
浏览论文内容
中文总结 AI 辅助
本文提出新基准FaithformBench，通过自动生成扰动推理步骤评估AF系统的忠实性，发现多数AF存在“悄悄修正”无效输入的谄媚现象，当前AF在有效性与无效性保留间存在张力。
中文摘要 AI 辅助
自动形式化（Autoformalisation, AF）系统可将自然语言推理步骤映射为Lean等证明助手的形式化陈述，本文研究如何评估这类系统的忠实性。现有方法要么需要昂贵的人工标注真值，要么依赖大语言模型（LLM）评判或嵌入模型，准确性保障有限；且这些方法通常仅考虑已知正确的输入，未评估AF是否忠实地转换了不正确的输入。为解决这些局限，本文提出一种新的AF忠实性基准，该基准应用成本低、在弱假设下可靠，且同时评估正例与反例。本文方法基于自动生成经设计为无效的扰动推理步骤，然后测量未扰动步骤的有效性保留情况与扰动步骤的无效性保留情况。将本文方法应用于四个数学数据集上的八个AF系统，观察到普遍存在的“谄媚”（sycophancy）现象：许多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.
