PutnamBench：用于评估神经定理证明器的普林顿数学竞赛基准
人工智能
2024-11-05 v2 计算与语言
机器学习
计算机科学中的逻辑
编程语言
摘要
我们提出PutnamBench，这是一个新的多语言基准，用于评估神经定理证明器解决竞赛数学问题的能力。PutnamBench由1692个手工构建的640个定理的形式化版本组成，源自威廉·Lowell Putnam数学竞赛，这是北美最顶尖的本科生数学竞赛。所有问题都有Lean 4和Isabelle的形式化版本，其中一个大子集也有Coq形式化版本。PutnamBench需要显著的解决问题能力和在大学数学课程中广泛主题的熟练功底。我们使用PutnamBench评估了几个 established的神经和符号定理证明器。这些方法只能解决PutnamBench中的一小部分问题，建立了该基准作为神经定理证明研究的困难开放挑战。PutnamBench可在https://github.com/trishullab/PutnamBench上获得。
引用
@article{arxiv.2407.11214,
title = {PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition},
author = {George Tsoukalas and Jasper Lee and John Jennings and Jimmy Xin and Michelle Ding and Michael Jennings and Amitayush Thakur and Swarat Chaudhuri},
journal= {arXiv preprint arXiv:2407.11214},
year = {2024}
}
备注
Accepted at NeurIPS 2024 Datasets & Benchmarks Track