RePro：基于证明验证的基准重写，用于可靠评估LLM的数学问题求解能力

# RePro：基于证明验证的基准改写用于可靠评估大型语言模型的数学问题解决能力  
来源：https://arxiv.org/html/2609.00062  

**Xiyuan Zhou†**†equal contribution  
**Zhuoqi Li**1footnotemark:1  
**Affiliation:** 香港中文大学（深圳）  
**Email:** [[email protected]](mailto:)  
**Xinlei Wang**  
**Affiliation:** INSAIT, 圣克莱门特·奥赫里德索菲亚大学  
**Email:** [[email protected]](mailto:)  
**Yirui He**  
**Affiliation:** 香港中文大学（深圳）  
**Affiliation:** 深圳市河套区域研究院  
**Email:** [[email protected]](mailto:)  
**Yuhao Wu**  
**Affiliation:** 香港中文大学（深圳）  
**Email:** [[email protected]](mailto:)  
**Yuheng Cheng**  
**Affiliation:** 香港中文大学（深圳）  
**Email:** [[email protected]](mailto:)  
**Yan Xu**††Corresponding authors.  
**Affiliation:** 南洋理工大学  
**Email:** [[email protected]](mailto:)  
**Junhua Zhao**22footnotemark:2  
**Affiliation:** 香港中文大学（深圳）  
**Affiliation:** AIRS  
**Email:** [[email protected]](mailto:)  
**Jinjin Gu**22footnotemark:2  
**Affiliation:** INSAIT, 圣克莱门特·奥赫里德索菲亚大学  
**Email:** [[email protected]](mailto:)  

###### 摘要  
数据污染破坏了大型语言模型（LLMs）在数学问题解决上的可靠评估。虽然基于改写的评估缓解了记忆问题，但现有方法缺乏对题目有效性和答案正确性的保证。我们提出**基于证明验证的基准改写（RePro）**——首个将Lean导向的神经自动定理证明器（ATPs）整合到基准改写中的框架。该框架改写题目并重新生成答案，其正确性由Lean验证的证明确保。在GSM8K和MATH上的实验表明，RePro保留的改写实例实现了100%的良定义性、可行性和答案正确性，而现有方法仍会生成无效或错误实例。此外，多个模型在经过证明验证的改写基准上表现出准确率下降，表明其性能对表层和结构变化敏感，可能部分反映了记忆效应。我们的源代码和数据可在https://github.com/AI4Engi/RePro获取。  

## 1 引言  
评估数学能力对于理解大型语言模型（LLMs）的推理能力至关重要（Shao等人，2024；Ahn等人，2024）。然而，基准可靠性因数据污染而受到挑战，因为训练语料库和评估基准常常共享公开来源（Chen等人，2025；Cheng等人，2025）。这种重叠可能使模型通过记忆而非真正的推理获得高分（Li等人，2024；Zhou等人，2026a；Zhao等人，2025）。近期的动态评估方法，包括基准改写、交互式评估和多智能体评估，旨在减少污染（Chen等人，2025）。然而，它们依赖启发式改写或基于模型的生成过程，难以保证题目有效性和答案正确性。参考标题：图1：RePro概览。现有改写方法可能产生无效题目或错误答案。RePro整合形式化验证，确保改写实例是有效问题并配有经过验证的答案，从而实现可靠的LLM评估。基准可靠性在现有评估中仍然是关注点，即使对于有影响力的专家基准如GPQA（Rein等人，2024）和HLE（AI安全中心等人，2026）也是如此，这些基准推动了前沿LLM评估的发展。HLE-Verified进一步强调了答案可靠性的重要性，报告称在HLE的数学类别中，题目有效性超过92%，而答案有效性仅为59.6%（Zhai等人，2026）。这表明基准可靠性取决于题目有效性和答案正确性，反映了LLM系统中对验证器引导可靠性的更广泛重视（Wang等人，2026）。因此，RePro聚焦于数学上可形式化验证的题目，并通过评估改写实例是否良定义、可行，并配有正确参考答案（见第4节）来提升可靠性。  

为提高基准改写可靠性，我们引入确定性证明验证，将Lean导向的神经自动定理证明器（ATPs）和证明助手检查整合到改写流程中，用机器可验证的推理取代基于LLM的启发式评估。在RePro中，证明搜索依赖Lean导向的神经ATPs，如Goedel-Prover（Lin等人，2026）和DeepSeek-Prover（Ren等人，2025）。给定一个形式化陈述，这些模型生成Lean证明脚本，作为候选证明，仅在Lean内核级验证通过后才被接受。与经典ATPs和SMT求解器（如Vampire（Kovács和Voronkov，2013）、Z3（De Moura和Bjørner，2008））在支持的逻辑片段内返回可靠结果不同，神经ATPs可能生成编译失败、目标不匹配或策略级错误的脚本。因此，RePro仅保留通过Lean内核级检查（De Moura等人，2015）的证明。  

基于形式化验证证明提供的保证，我们提出RePro（基于证明验证的基准改写），一个构建数学严谨改写基准的框架。如图1所示，在RePro中，LLMs生成多样化的改写题目并执行保守语义筛选，而ATPs搜索候选证明并由证明助手验证。这样，改写基准在保持高多样性的同时，提供可验证的正确性保证。仅保留参考答案具有形式化验证证明的实例，确保发布的基准仅包含具有形式化验证答案的问题。详细方法见第3节。  

实证结果表明，RePro显著提高了基于改写评估的可靠性。与现有方法相比，RePro在GSM8K（Cobbe等人，2021）和MATH（Hendrycks等人，2021）上保留的改写实例实现了100%的良定义性、可行性和答案正确性，而现有方法仍会产生无效题目或错误参考答案。我们的贡献可总结如下：  
（1）我们提出RePro，首个将ATPs和Lean整合到统一验证流程中的基准改写框架，仅保留具有验证参考答案的实例，并通过三阶段验证过程确保题目有效性。  
（2）我们引入面向可靠性的改写基准评估标准，涵盖良定义性、可行性和答案正确性。  
（3）我们使用证明验证的改写来分析问题重构的敏感性，并识别与记忆相关的潜在信号。  

参考标题：图2：所提出的基于改写评估的验证流程框架。该流程逐步筛选改写实例，以获取具有验证答案的有效问题。  

## 2 相关工作  
**动态基准生成。** 动态基准方法通过自动生成新测试实例来缓解数据污染并扩展评估覆盖范围。常见方法是基准改写，应用语义或结构变换，如同义词释义（Ying等人，2024；Zhu等人，2024）、数值替换（Qian等人，2024）和结构扰动（Cao等人，2024），在利用现有评估资源的同时削弱记忆线索。另一系列工作采用多智能体或基于求解器的框架进行基准构建，如Benchmark Self-Evolving（Wang等人，2025b）、BenchAgents（Butt等人，2024）和基于CSP的逻辑谜题基准ZebraLogic（Lin等人，2025）。尽管提高了多样性和覆盖范围，这些方法仍很大程度上依赖启发式验证，包括人工检查、LLM-as-a-Judge或基于智能体的检查。这种验证可能仍留下语义漂移、错误标签或隐含假设违反等问题，限制了确定性可靠性保证，见第4节和第6.1节。  

**形式化验证与自动定理证明。** 形式推理以机器可验证的格式表示数学陈述和证明，能够严格验证逻辑正确性。证明助手如Lean（De Moura等人，2015）和Coq（Bertot和Castéran，2013）提供数学推理的形式语言，并通过内核级检查验证证明。大型形式化数学库如mathlib支持大规模形式化和自动推理（Yang等人，2023）。经典ATPs和SMT求解器，如Vampire（Kovács和Voronkov，2013）和Z3（De Moura和Bjørner，2008），在支持的逻辑内解决形式逻辑问题，而锤子系统如LeanHammer将Lean与外部证明器连接（Zhu等人，2025）。相比之下，近期的神经Lean证明器，包括DeepSeek-Prover（Ren等人，2025）和Goedel-Prover（Lin等人，2026），生成候选Lean证明脚本，必须在Lean中验证后才能接受。RePro在Lean/mathlib环境下运行，使用神经Lean证明器结合内核级验证来确保答案正确性。先前工作主要研究定理证明本身，而基准验证仍未被充分探索。  

## 3 RePro  
### 3.1 概述  
为构建具有形式化验证参考答案的改写基准，我们提出RePro。现有基于改写的方法通常依赖启发式验证机制，如LLM-as-a-Judge或基于规则的检查，无法对题目有效性或答案正确性提供确定性保证。为解决此局限，RePro将ATPs整合到基准改写过程中，通过形式化证明验证参考答案，同时保留改写实例的多样性。  

RePro遵循渐进式验证范式。它首先提示LLM通过数值重新参数化、逻辑重组、约束修改和上下文重建生成候选改写，并过滤掉未通过基本题目有效性检查的实例（如表述模糊、缺少约束或解不可行）。剩余候选被转换为Lean中的可执行形式化规范，为改写题目提供精确且机器可检查的表示。最后，自动定理证明器（ATP）执行证明搜索以生成候选证明，其正确性由Lean证明助手检查。通过此分阶段过程，RePro仅保留良定义、可行且答案有形式化验证证明支持的改写实例。提示模板和实现细节见附录B，RePro生成的改写实例示例见附录G。  

### 3.2 可行性筛选  
可行性筛选始于基于LLM的改写，随后在可执行形式化和证明验证之前过滤无效候选改写。给定原始问题，LLM在保留核心数学结构、解题逻辑、难度和答案类型的同时生成候选改写。改写过程应用数值重新参数化、逻辑重组、约束修改和应用题上下文重建等策略。改写器被指示不解决改写后的问题或生成新答案。生成的候选随后经过题目有效性筛选。此步骤移除定义不清、模糊、内部不一致、矛盾、不现实或在基本现实或任务特定约束下不可行的问题。此处可行性指改写题目的语义和约束一致性，而不仅仅是目标能否从前提形式推导。因此，即使目标可从矛盾前提形式推导，矛盾前提的候选也会被拒绝。详细的改写提示、筛选标准和实现细节见附录B。  

例如，在涉及人口数量或数量约束的问题中，自动改写可能引入负值或其他违反隐含现实假设的条件（Zhou等人，2026b）。尽管此类输出可能在数学上可表达，但在预期问题语义下被视为不可行，因此被移除。此阶段旨在确保题目有效性而非答案正确性。答案正确性通过后续的证明级验证建立，而最终的答案-目标匹配步骤通过确保验证答案对应改写问题中请求的具体数量，提供额外的目标级一致性检查。  

### 3.3 可执行形式化  
可执行形式化将通过可行性筛选的改写实例转换为Lean中的机器可验证形式化陈述。此阶段包括格式检查和语义检查。格式检查确保生成的Lean代码语法有效且可在Lean中编译。语义检查执行LLM辅助的保守对齐筛选，比较改写后的自然语言问题与Lean形式化陈述中的关键元素，如数量、条件、逻辑结构、对象类型和请求的目标。我们采用保守的全通过策略。对于每个编译的形式化，语义检查器以温度零查询三次。仅当三次判断均返回“一致”时，候选才被接受。任何不匹配、解析失败或未