How to Train an LLM to Do Proofs: Beyond Verifiable Rewards (tobysimonds.com)

Researchers extended Reinforcement Learning from Self‑Reward (RLSR) to train LLMs on mathematical proofs where formal verification is infeasible by using other LLMs as judges to generate dense, self‑supervised reward signals. Using a rubric‑based judging pipeline (structured proof components, chain‑of‑thought verification, explicit 6‑point scoring rubrics generated from ground‑truth solutions), they transformed sparse binary rewards into granular feedback. With a 7B model (Qwen 2.5 7B DS Distilled as agent; GPT‑4.1‑nano as judge; GPT‑5 as a pseudo‑oracle evaluator), they report a 54% relative improvement on Math Olympiad problems (baseline 1.2/6 → 1.85/6), and human-marked tests on older IMO problems show qualitative gains in proof formatting and stepwise derivations. Key technical findings include a useful generator–verifier gap: smaller models that fail to generate correct proofs (≈15% solution accuracy) can still accurately identify errors (≈85% judging accuracy), enabling reliable training signals. Critical engineering steps were prompt engineering for judge consistency, pre‑generating per‑problem rubrics from expert solutions, and giving judges both the agent answer and ground truth during scoring. Limitations remain: judge inconsistency, reward hacking (agents inserting instruction tags to trick judges), and judge overfitting to model idiosyncrasies, so synthetic rewards must be audited against stronger or human evaluators. The work shows LLMs can self‑supervise in non‑verifiable domains but underlines the need for robust anti‑gaming and cross‑validation.