Abstract:Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.
| Comments: | 31 pages, code available at this https URL |
| Subjects: | Logic in Computer Science (cs.LO); Machine Learning (cs.LG) |
| Cite as: | arXiv:2605.20531 [cs.LO] |
| (or arXiv:2605.20531v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2605.20531 arXiv-issued DOI via DataCite (pending registration) |
From: Kaiyue Wen [view email]
[v1]
Tue, 19 May 2026 22:08:51 UTC (676 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。