LLMs can solve hard math now, but checking whether a proof is actually correct is still shaky, and verification sits at the center of every math agent workflow and RL loop. Rule-based checks miss open-ended proofs; LLM verification is unreliable and expensive, sometimes thousands of API calls for one IMO-level problem.🤔
Pessimistic Verification from @TsinghuaNLP (OpenBMB member), to appear at ICML 2026, pins the real bottleneck on error detection and builds a simple fix around it.
Paper: https://arxiv.org/abs/2511.21522
Code: https://github.com/THUNLP-MT/pverify

1⃣️ The core idea: verify one proof many times in parallel and reject it the moment any run reports an error. Detecting an error is a low-probability event, so aggregating pessimistically amplifies it; since models reason soundly before flagging errors, true false negatives are rare. Majority voting, by contrast, barely helps here.
2⃣️ Three variants from whole-proof to fine-grained. Simple (pes@n) repeats standard verification in parallel; vertical (vp@k) splits the proof into k-line chunks for focused review; progressive (prog@n/k) does multi-scale checking, filtering obvious errors first then drilling into steps, with natural pruning. Progressive gives the best performance and efficiency.
3⃣️ It lifts TNR and Balanced F1 across IMO-GradingBench, Hard2Verify, and their new QiuZhen-Bench, and its token efficiency beats long CoT. At matched performance, progressive uses roughly a quarter of the tokens, runtime, and cost of the parallel verification common in agent workflows.
4⃣️ The twist: most false negatives from GPT-5-mini and stronger models are real critical errors the dataset annotators missed, so benchmarks underestimate strong verifiers. On IMO 2025 with Gemini 3 Pro, a verification-based workflow goes 13 → 22 points with progressive, using fewer tokens than simple parallel verification.