# Pseudo-Formalization for Automatic Proof Verification

arXiv: https://arxiv.org/abs/2605.20531 · HTML: https://mlsanity.com/paper/2605.20531/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 23 of its 111 references that are in the map.
- First posted on arXiv 19 May 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 23 of 23)

- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Generative Verifiers: Reward Modeling as Next-Token Prediction](https://mlsanity.com/paper/2408.15240/) (2024)
- [ProcessBench: Identifying Process Errors in Mathematical Reasoning](https://mlsanity.com/paper/2412.06559/) (2024)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning](https://mlsanity.com/paper/2511.22570/) (2025)
- [Prover-Verifier Games improve legibility of LLM outputs](https://mlsanity.com/paper/2407.13692/) (2024)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Towards Robust Mathematical Reasoning](https://mlsanity.com/paper/2511.01846/) (2025)
- [Sample, Scrutinize and Scale: Effective Inference-Time Search by Scaling Verification](https://mlsanity.com/paper/2502.01839/) (2025)
- [SPC: Evolving Self-Play Critic via Adversarial Games for LLM Reasoning](https://mlsanity.com/paper/2504.19162/) (2025)
- [LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback](https://mlsanity.com/paper/2406.14024/) (2024)
- [Trust, But Verify: A Self-Verification Approach to Reinforcement Learning with Verifiable Rewards](https://mlsanity.com/paper/2505.13445/) (2025)
- [Learning to Give Checkable Answers with Prover-Verifier Games](https://mlsanity.com/paper/2108.12099/) (2021)
- [Heimdall: test-time scaling on the generative verification](https://mlsanity.com/paper/2504.10337/) (2025)
- [Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math](https://mlsanity.com/paper/2510.13744/) (2025)
- [LOCA-bench: Benchmarking Language Agents Under Controllable and Extreme Context Growth](https://mlsanity.com/paper/2602.07962/) (2026)
- [Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection](https://mlsanity.com/paper/2511.13027/) (2025)
- [Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Models](https://mlsanity.com/paper/2602.16793/) (2026)
- [Recursive Models for Long-Horizon Reasoning](https://mlsanity.com/paper/2603.02112/) (2026)
- [From Solving to Verifying: A Unified Objective for Robust Reasoning in LLMs](https://mlsanity.com/paper/2511.15137/) (2025)
- [Pessimistic Verification for Open Ended Math Questions](https://mlsanity.com/paper/2511.21522/) (2025)

## Built on by (most cited first, 4 of 4)

- [Learning Strategies to Break Judges](https://mlsanity.com/paper/2609.33773/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [One-Sided Verification Under Limited Expert Review](https://mlsanity.com/paper/2610.18089/) (2026)

## Abstract (arXiv)

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.