CNLVerifier: A Controlled-Natural-Language Verifier for LLM-Driven Mathematical Reasoning

Large language models can generate mathematical proofs in natural language, but such informal proofs are difficult to use as reliable, automatic, and actionable feedback for post-training and inference-time compute. Formal proof assistants provide strong correctness guarantees, but their proof languages are often costly for current models to generate and interact with. We present CNLVerifier (Controlled Natural Language Verifier), a lightweight verifier for proofs written in a controlled, LaTeX-flavored natural language. CNLVerifier provides structured diagnostics that can serve both as a binary acceptance signal and as feedback for self-refinement. We use these signals for verifier-filtered supervised fine-tuning and reinforcement learning. Experiments on miniF2F show that verifier-based training and inference-time compute improve the generation of verifier-accepted CNL proofs.