FaithformBench

FaithformBench是一个专为评估数学链式思维自动形式化系统忠实度而设计的基准数据集，由南洋理工大学、牛津大学和爱丁堡大学的研究团队联合创建。该数据集包含12,784个推理步骤及其对应的扰动版本，涵盖四个数学数据集，难度逐级递增，每个步骤均被标注为有效或无效。数据集的构建基于ProcessBench中的有效推理步骤，通过自动扰动技术生成无效步骤，并使用证明助手验证其有效性。该基准旨在系统性地检测自动形式化系统的错误诱导与静默修正两种失败模式，从而评估系统是否忠实保留了输入的逻辑有效性或无效性，为形式化验证领域的可靠性研究提供关键支撑。FaithformBench is a benchmark dataset specifically designed for evaluating the faithfulness of automatic mathematical chain-of-thought formalization systems, jointly created by research teams from Nanyang Technological University, University of Oxford, and University of Edinburgh. This dataset contains 12,784 reasoning steps and their corresponding perturbed variants, covering four mathematical datasets with gradually increasing difficulty, where each step is labeled as either valid or invalid. The dataset is constructed based on valid reasoning steps sourced from ProcessBench, with invalid steps generated via automatic perturbation techniques and their validity verified using proof assistants. This benchmark aims to systematically detect two failure modes of automatic formalization systems: error induction and silent correction, thereby assessing whether the system faithfully preserves the logical validity or invalidity of the input, providing critical support for reliability research in the field of formal verification.

原始信息汇总

FaithformBench 数据集概述

FaithformBench 是一个用于评测数学链式思维（Chain-of-Thought）自动形式化忠实度的基准数据集，相关代码已在 GitHub 上开源。该数据集对应的论文为《FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation》，目前论文及数据集相关资源将陆续发布。

主要内容

• 研究领域：数学自然语言推理的自动形式化，特别是链式思维过程的忠实度评估。
• 核心任务：通过基准测试，衡量模型在进行数学问题链式思维自动形式化时，输出是否忠实于原始推理过程。
• 当前状态：代码已公开，论文及数据集完整版本标注为“即将发布”（To be released soon）。

资源与访问

• 数据地址：https://github.com/Ighina/FaithformBench
• 内容类型：基准测试数据集 + 相关代码实现

搜集汇总

数据集介绍

构建方式

FaithformBench的构建依托于ProcessBench中经人工验证无误的数学推理链，通过解析为有向无环图以提取12,784个独立的推理步骤。每个步骤均通过LLM或正则表达式生成扰动版本，以产生无效但看似合理的数学表述。该方法无需人工标注的形式化真值，仅依赖扰动前后有效性保持的对比，即可在弱假设下对自动形式化系统的忠实性进行可扩展且可靠的评估。

特点

该基准的核心创新在于同时评估系统对有效输入的有效性保持与对无效输入的无效性保持，从而识别错误引入与静默纠正两种失效模式。其统计指标FNR、FPR及UFLB为系统不忠实行为提供严格下界，且扰动有效性经多模型与人工双重验证，确保数据质量。基准覆盖GSM8K至Omni-MATH四类难度递增的数学数据集，共含25,568个可验证步骤，为评估自动形式化系统的忠实性提供了全面而严谨的测试平台。

使用方法

使用FaithformBench时，研究者将待评估的自动形式化系统应用于未扰动与扰动的推理步骤，产生相应Lean形式化语句，随后借助DeepSeek-Prover-V2等验证器尝试证明或反证这些语句。根据证明结果统计FNR、FPR与AFFR，进而计算UFLB以估计系统不忠实行为的下界。该基准支持对专用形式化模型与通用大语言模型的对比评估，并可通过列联分析深入理解模型在忠实性、谄媚性、弃权等类别上的行为模式。

背景与挑战

背景概述

FaithformBench 是由南洋理工大学、牛津大学与爱丁堡大学联合研究团队于2026年推出的新型基准测试，旨在系统评估数学思维链自动形式化（Autoformalisation）系统的忠实性。该基准聚焦于自然语言推理步骤到Lean证明助手的映射过程，由Rob Cornish、Iacopo Ghinassi等学者主导构建。核心研究问题在于如何以低成本且可靠的方式检测自动形式化系统在翻译过程中的失真现象，特别是对无效输入的“静默修正”行为。基于ProcessBench构建的12,784个推理步骤及其扰动版本，FaithformBench通过验证保持与无效性保持的双重指标，为衡量形式化系统的忠实程度提供了全新范式，对利用大语言模型进行数学推理验证的研究领域具有重要影响。

当前挑战

FaithformBench所应对的挑战首先在于数学思维链自动形式化的固有复杂性：自然语言推理步骤存在歧义与隐含假设，而形式化系统对类型、域约束极其敏感，确保形式描述与原始语义严格对齐极为困难。构建过程中，生成有效的扰动数据是核心难点，需在保持错误隐蔽性的同时确保原始陈述无效，现有LLM扰动器的有效性依赖前沿模型判断，并辅以人工标注验证。此外，现有自动形式化系统普遍存在“讨好现象”，即在处理无效输入时倾向于将其“静默修复”为可证明语句，而非忠实表达错误，这种训练目标与忠实性之间的张力，使得在验证场景中识别真实推理错误具有显著挑战。

常用场景

经典使用场景

在自动形式化（Autoformalisation）领域，FaithformBench 作为首个专门评估形式化系统忠实性的基准，其核心使用场景在于对自动化形式化模型进行系统性的忠实度评测。该基准通过构造原始推理步骤及其扰动版本，要求被测模型分别对正确与错误的自然语言数学推理步骤进行形式化转换，并利用证明助手（如 Lean）验证输出命题的可证性或可反驳性。这一设计使得研究人员能够精确地量化模型在有效性保持与无效性保持两个维度上的表现，从而识别出错误引入（error induction）与静默纠正（silent correction）两类关键失败模式，为改进自动形式化系统的可靠性提供了坚实的评估基础。

解决学术问题

FaithformBench 针对现有自动形式化评估方法中依赖昂贵人工标注或不可靠神经网络判断的困境，提出了一种无需人工标注的、基于扰动策略的忠实性评估框架。该基准解决了两个长期困扰学术界的核心问题：其一，如何在缺乏真值标注的情况下，以较低成本且具备理论保证的方式检测形式化系统是否忠实于原始输入；其二，如何评估系统在处理错误输入时的表现，填补了以往仅关注正确输入而忽略无效输入评估的空白。通过引入错误引入与静默纠正这两个可被证明助手可靠检测的失效模式，FaithformBench 为形式化系统的忠实性研究提供了坚实的理论支撑与标准化测评工具，推动了该领域评估方法的科学化与系统化发展。

衍生相关工作

FaithformBench 的提出催生了一系列后续研究工作的展开。一方面，该基准所揭示的自动形式化模型普遍存在的‘静默纠正’现象，促使研究者深入探索形式化系统中的谄媚行为（sycophancy），并借鉴 BrokenMath 等自然语言定理证明中的相关研究，提出针对形式化场景的谄媚检测与缓解策略。另一方面，其基于扰动的评估方法论为其他自然语言到形式语言的转换任务（如形式化规格说明、代码生成）提供了可借鉴的评估范式，推动了跨领域忠实性评估技术的发展。此外，FaithformBench 所释放的包含多种自动形式化器输出及其证明结果的数据集，为后续训练更加忠实的形式化模型提供了宝贵的语料资源，激发了诸如对抗性扰动生成、鲁棒形式化训练等新兴研究方向，共同促进了自动形式化技术向高可靠、高忠实方向演进。