PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
<|reference_start|>PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition: We present PutnamBench, a new multilingual benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1697 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the theorems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. Proving the theorems requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We use PutnamBench to evaluate several established neural and symbolic theorem-provers. These approaches can only solve a handful of the PutnamBench problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving. PutnamBench is available at https://github.com/trishullab/PutnamBench.<|reference_end|>
@article{tsoukalas2024putnambench:,
    title={PutnamBench: Evaluating Neural Theorem-Provers on the Putnam
  Mathematical Competition},
    author={George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding,
  Michael Jennings, Amitayush Thakur, Swarat Chaudhuri},
    journal={arXiv preprint arXiv:2407.11214},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.11214},
    primaryClass={cs.AI cs.CL cs.LG cs.LO cs.PL}
}