Researchers have built an automated pipeline that turns real mathematical proofs into fill-in-the-blank tests for language models.
The system, called Mask-Proof, redacts key formula steps from actual proofs and asks models to reconstruct them. An LLM-based judge scores each reconstruction using repeated votes for consistency, reaching 96.8% agreement with human expert annotators. The team assembled Mask-ProofBench, a set of 292 curated problems spanning diverse research areas, and ran 17 models through it. Reasoning-enhanced models outperformed standard ones by 12% to 27%, depending on the task.
Most math benchmarks reward correct final answers, which tells you whether a model can arrive at a result but not whether it reasons soundly at each step along the way. Step-level evaluation is harder to game and harder to automate at scale, which explains why almost no one has done it reproducibly before now. If the 96.8% expert-agreement figure holds under scrutiny from outside the original team, Mask-Proof offers a cheaper proxy for human grading on a specific but meaningful slice of AI math evaluation.
The benchmark, annotations, and code are all public - so rivals can stress-test their own models against it immediately, which is either a generous contribution to the field or an uncomfortable mirror, depending on your leaderboard position.