REVIEW 20 cited by
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
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.
Forward citations
Cited by 20 Pith papers
-
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
A new Lean 4 benchmark of 100 combinatorics problems, together with a two-stage evaluation method for fill-in-the-blank questions, shows that current LLM-based provers solve at most 7 of the 100 problems.
-
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
CausalForge is a Lean-grounded, self-improving agentic framework that proposes, proves, and statement-audits causal inference theorems; its runs produced nine accepted results including a new ATE minimax upper bound.
-
Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems
A fully automated pipeline produces proof-centric math benchmarks, demonstrated on algebraic geometry with 456 items, where leading LLMs score near 60 percent.
-
KRISTEVA: Close Reading as a Novel Task for Benchmarking Interpretive Reasoning
KRISTEVA is the first close reading benchmark for large language models, and current models still underperform experienced human readers on 10 of its 11 tasks.
-
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
Formulates problem-solving as a sound Markov decision process, implements it in Lean as FPS and D-FPS, and introduces three formal problem-solving benchmarks plus the RPE answer-equivalence checker.
-
PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs
PROVE-RT, a retrieval-augmented, staged LLM pipeline, mechanizes 44.7% of a new 300-sketch benchmark of real-time scheduling analyses in the PROSA/Rocq library, far above direct LLM prompting.
-
Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
A verifier-grounded self-evolving Lean proof agent with a champion-driven, self-hardening benchmark reached 45.1% held-out miniF2F solve rate versus 32.0% for a fixed-benchmark baseline.
-
The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data
The topological dual of a dataset is introduced as a transformation that encodes logical structures into topological ones to expose invariants in neural latent spaces for AlphaGeometry-style reasoning.
-
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
White-box proof search with factorized Lean 4 goals reaches 18.4% on MiniF2F with Llemma-7B, outperforming black-box generation at 9.6%.
-
Mathesis: Towards Formal Theorem Proving from Natural Languages
An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Decomposing Elements of Problem Solving: What "Math" Does RL Teach?
Reinforcement learning (GRPO) on math LLMs primarily increases execution robustness on already-solvable problems, not planning or coverage of new problems.
-
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
An open-source theorem-proving model reaches state-of-the-art scores on miniF2F (57.6% Pass@32) and PutnamBench by training on 800K formal proofs synthesized through autoformalization and expert iteration.
-
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
ProofWala is a multilingual proof-engineering framework that demonstrates cross-lingual transfer between Lean 4 and Coq for neural theorem proving.
-
Question Begets Question: Self-Evolving Curriculum for Reinforcement Fine-Tuning on Competition Mathematics
A self-evolving curriculum that retrains a language model on variants of problems it can mostly get right lifts AIME pass@1 from 5.6% to 16.5%, beating static augmentation under the same data budget.
-
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.
-
FMC: Formalization of Natural Language Mathematical Competition Problems
An LLM-based error-feedback pipeline produces FMC, a dataset of 3,922 Olympiad problems aligned with 9,787 Lean statements, claimed to be a challenging ATP benchmark.
-
Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
Verifier-integrated reinforcement learning with multi-turn reflection improves 7B-scale Lean 4 theorem proving by 2 to 3 points on MiniF2F at pass@128.
-
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
LeanConjecturer automatically generates thousands of Lean 4 theorem statements from Mathlib files and uses them for reinforcement learning, with modest measured gains on held-out problems.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
Discussion (0). Continue with ORCID to comment.