数学评测防作弊新招！RePro用Lean证明重写题库，正确率100%，模型成绩现原形！
RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
📖 AI 总结
该论文提出了一种名为RePro（Proof-Verified Benchmark Rewriting）的框架，旨在解决大语言模型在数学问题求解评估中因数据污染导致的可靠性问题。现有基于改写的方法虽能缓解记忆效应，但无法保证改写后问题的有效性和答案正确性。RePro首次将面向Lean的神经自动定理证明器整合进基准改写流程，在改写数学题目的同时重新生成答案，并通过Lean验证的证明确保正确性。在GSM8K和MATH基准上的实验表明，RePro保留的改写实例在良定义性、可行性和答案正确性上均达到100%，而现有方法仍会产生无效或错误实例。此外，多个模型在经证明验证的改写基准上出现准确率下降，说明其表现对表层和结构变化敏感，可能部分反映了记忆效应而非真正的推理能力。该研究为构建更可靠的LLM数学评估基准提供了新思路。
🔑 关键词速览
| Data contamination | 数据污染，指训练数据中混入测试集样本，导致模型评估结果虚高。 |
| Benchmark rewriting | 基准重写，通过修改测试题目来减少模型对原题的记忆影响。 |
| Lean | Lean是一种交互式定理证明器，用于形式化数学证明。 |
| Neural automated theorem provers (ATPs) | 神经自动定理证明器，利用神经网络自动生成数学证明。 |
| Proof-verified | 证明验证的，指通过形式化证明确保结果正确性。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅