PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition

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.

한 줄 요약

PutnamBench는 대학 수준 수학 경시 문제를 기반으로 한 다언어 정리 증명 벤치마크로, 신경망 정리 증명기의 한계를 드러낸다.

핵심 기여도

640개의 Putnam 경시 문제를 1692개의 정리로 정식화하여, Lean 4, Isabelle, Coq 세 프레임워크에서 평가 가능하게 구성.
기존 벤치마크(MiniF2F, Fimo)와 달리, 넓은 수학 주제(해석학, 추상대수 등)를 다루며, 학부 수준의 문제를 포함.
모든 문제는 수작업으로 정식화되어 있으며, 미국수학회(MAA)의 허가를 받아 원문 문제도 제공.
평가 결과, 기존 신경망 및 기호적 정리 증명기들이 PutnamBench 문제 중 단수의 문제만 해결함.

핵심 아이디어

PutnamBench는 기존의 수학 정리 증명 벤치마크가 특정 주제나 프레임워크에 제한된다는 문제를 해결하기 위해 설계되었다. Putnam 경시 문제는 학부 수준의 수학 지식을 종합적으로 요구하며, 이는 기존의 국제수학올림피아드(IMO) 기반 벤치마크와 구별된다. 또한, 세 가지 주요 증명 도구(Lean 4, Isabelle, Coq)를 모두 지원함으로써, 다중 프레임워크에서의 평가 가능성을 확장하였다. 이는 기존 MiniF2F(Lean 3만 지원)나 Fimo(Lean 3만 지원)와 비교해 큰 진전이다.

기술적 접근법

**데이터셋**: 640개의 Putnam 문제를 1692개의 정리로 수작업 정식화.
**프레임워크**: 모든 문제는 Lean 4와 Isabelle에 정식화되어 있으며, 일부는 Coq에도 포함됨.
**평가 대상**: Draft-Sketch-Prove, Copra, GPT-4, Sledgehammer, Coqhammer 등 신경망 및 기호적 정리 증명기.
**평가 방식**: 정리 증명 성공 여부를 기준으로, 기존 방법들이 단수의 문제만 해결함을 확인.

주요 결과

기존 신경망 정리 증명기(Draft-Sketch-Prove, Copra, GPT-4 등)는 PutnamBench 문제 중 단수의 문제만 해결함.
PutnamBench는 기존 MiniF2F, Fimo 등 대비 훨씬 어려운 수준의 문제를 포함하며, 기존 방법들의 성능 한계를 드러냄.
평가 결과, 모든 방법들이 PutnamBench 문제 중 "단수의 문제"만 해결함을 명시 (정확한 수치는 명시되지 않음).

의의 및 한계

PutnamBench는 학부 수준의 수학 문제를 다루며, 다양한 프레임워크에서 평가 가능하다는 점에서 학술적 가치가 높다. 특히, 기존 벤치마크가 특정 수학 분야나 프레임워크에 제한된다는 문제를 해결하였다. 그러나, 평가 결과가 명시적으로 수치화되지 않았으며, 일부 문제는 Coq에만 포함되어 있어 다중 프레임워크 평가의 균형이 부족할 수 있다. 또한, 기존 정리 증명기들이 새로운 보조정리 생성 및 복잡한 증명 구성 능력이 부족하다는 한계도 드러냈다.

실용적 활용

PutnamBench는 신경망 정리 증명기의 개선을 위한 연구에 활용될 수 있으며, 특히 학부 수준의 수학 문제 해결 능력을 향상시키는 데 기여할 수 있다. 또한, Lean 4, Isabelle, Coq 등 다양한 증명 도구 간의 비교 연구에도 유용하게 사용될 수 있다.