[论文] ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Researc...

论文概要

研究领域: NLP 作者: Zeyu Zheng, Yiyang Liu, Yuyang Zhao, Congmin Zheng, Jiachen Zhu, Jianian Chen, Kangning Zhang, Kayue Daniel Wong, Lingyu Yang, Rong Shan, Shihao Chen, Thomas Zhu, Wentao Zhang, Xiaopeng Li, Yan Hu, Yongxi Lin, Yuxiang Chen, Zhuoying Ou, Jianghao Lin, Jeremy Avigad, Prasad Tetali, Jingbang Chen, Sean Welleck 发布时间: 2026-10-22 arXiv: 2610.27046

中文摘要

随着AI系统开始解决开放性研究问题，可靠的验证变得越来越重要。形式化数学为数学推理提供了一个可信的框架，使智能体在进行数学探索的同时能够产生机器可验证的证明。现有的形式化数学基准通常聚焦于已知结果或少数著名的开放问题，一旦解被发现并广泛传播，这些问题就很难被可靠地评估。现有的评估协议也不总是与现代编码智能体的工作方式一致。因此我们引入ReuF2F，一个包含244个形式化开放问题的Lean 4基准测试，这些问题源自本科生研究体验（REU）项目，涵盖广泛的数学子领域的入门级开放研究问题。我们预计这些不太引人注目的开放问题——往往受到较少关注且可能更长时间保持未解决状态——更适合用于Lean中端到端开放问题解决的留出评估。我们采用标准的编码智能体评估设置，将每个问题及其逻辑否定放入Docker容器中的Lean项目中。我们还基于mini-SWE-agent构建了Leanimum-agent，为跨模型的公平比较提供统一的运行环境。我们的评估发现，即使表现最好的模型也只能解决约40%的问题，在形式化开放研究问题上仍有很大的改进空间。

原文摘要

As AI systems begin to resolve open research problems, reliable verification becomes increasingly important. Formal mathematics provides a trusted framework for mathematical reasoning, enabling agents to produce machine-checkable proofs while conducting mathematical exploration. Existing formal mathematics benchmarks often focus on known results or a small set of prominent open problems, which can become difficult to evaluate reliably once solutions are discovered and widely disseminated. Existing evaluation protocols are also not always aligned with how modern coding agents operate. We therefore introduce ReuF2F, a Lean 4 benchmark of 244 formalized open problems drawn from Research Experiences for Undergraduates (REU), spanning entry-level open research problems across a broad range of m...

#论文 #arXiv #NLP #小凯