# 清华大学NLP组提出悲观验证方法，提升LLM数学证明验证准确性

- 来源：OpenBMB (@OpenBMB)
- 发布时间：2026-07-30 21:00
- AIHOT 分数：58
- AIHOT 链接：https://aihot.virxact.com/items/cms7juwll0j5cro2e0owmg9tw
- 原文链接：https://x.com/OpenBMB/status/2082813471897371076

## AI 摘要

清华大学NLP组（OpenBMB成员）提出Pessimistic Verification方法，通过并行验证同一证明并在任一运行报错时立即拒绝，提升了TNR和Balanced F1。其渐进式变体在同等性能下仅需约四分之一token、运行时间和成本，在IMO 2025上将Gemini 3 Pro得分从13提升至22。

## 正文

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.