It bypasses incomplete formal libraries in tools like Lean
Often in research level math, you can't verify a proof with Lean because the formal libraries needed don't exist yet.
Our fix: Pseudo-Formalization (PF), a proof verification method with the modularity and precision of formal proofs, but the flexibility of natural language.
No Digg Deeper questions have been answered for this story yet.
Verifying poorly written math papers used to be painful, and I tried to write my proof and lecture notes more structurally. The same applies to reviewing messy code.
Now, verifying AI-written proofs can also benefit from rewriting into cleaner structures.
One day the models should be trained to write cleaner and structured proofs as well :).
Often in research level math, you can't verify a proof with Lean because the formal libraries needed don't exist yet.
Our fix: Pseudo-Formalization (PF), a proof verification method with the modularity and precision of formal proofs, but the flexibility of natural language.
Often in research level math, you can't verify a proof with Lean because the formal libraries needed don't exist yet.
Our fix: Pseudo-Formalization (PF), a proof verification method with the modularity and precision of formal proofs, but the flexibility of natural language.
PF continues to help over baseline as model capability increases. That is, our method is composable with model scaling.
Paper: https://arxiv.org/abs/2605.20531 Code: https://github.com/Slim205/pseudo-formalization
Why do we need good verification? (1) It's the reward signal for training better AI models (2) Good verification helps humans review and understand long proofs. We propose verifying natural language proofs by first translating them to a Pseudo-Formal format, and then verifying.
We're also releasing ArxivMathGradingBench: 35 arXiv math papers with 40 real errors that the authors later corrected. It's a realistic test of verification on research-level math.
To verify a proof, an LLM first rewrites it into PF, then checks each module on its own. We call this Block Verification. Each check sees just one module and assumes the results it cites are correct.
A Pseudo-Formal proof is a proof broken into modules. Each module states its premises, its conclusion, and a short proof of that conclusion, all in natural language. A dependency graph (DAG) records which modules rely on which, so each one can be checked on its own.
Why does this help? Checking a whole proof at once makes the model hold the entire argument in context. Block Verification keeps each check small. We prove a good PF proof can be checked with context that doesn't grow with its length.
We test PF on two benchmarks: Hard2Verify (olympiad and Putnam level) and our new ArxivMathGradingBench (research-paper proofs). It Pareto-dominates the whole proof verification baseline.
This paper was a joint effort! Thanks to @Slim77235 and @wen_kaiyue for leading, and Mohammed Abouzaid and @tengyuma for advising.
