PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912101694439424 |
|---|---|
| author | Tsoukalas, George Lee, Jasper Jennings, John Xin, Jimmy Ding, Michelle Jennings, Michael Thakur, Amitayush Chaudhuri, Swarat |
| author_facet | Tsoukalas, George Lee, Jasper Jennings, John Xin, Jimmy Ding, Michelle Jennings, Michael Thakur, Amitayush Chaudhuri, Swarat |
| contents | We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692 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 problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. PutnamBench 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_11214 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition Tsoukalas, George Lee, Jasper Jennings, John Xin, Jimmy Ding, Michelle Jennings, Michael Thakur, Amitayush Chaudhuri, Swarat Artificial Intelligence Computation and Language Machine Learning Logic in Computer Science Programming Languages We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692 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 problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. PutnamBench 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. |
| title | PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition |
| topic | Artificial Intelligence Computation and Language Machine Learning Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2407.11214 |