Jul, 2024
PutnamBench: 在Putnam数学竞赛上评估神经定理证明器
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam
Mathematical Competition
TL;DRPutnamBench是一个多语言基准测试,用于评估神经定理证明器解决竞赛数学问题的能力,它包含了来自北美顶级本科数学竞赛William Lowell Putnam Mathematical Competition的640个定理的1697个手工构造形式化的表述,并用Lean 4和Isabelle进行了全部定理的形式化,其中还有一个相当大的子集有Coq形式化。该基准测试用于评估几种已有的神经和符号定理证明器,这些方法只能解决很少一部分的PutnamBench问题,从而将该基准测试确立为神经定理证明研究中的一个具有挑战性的开放问题。