PROCESS-VERIFIED REINFORCEMENT LEARNING FOR THEOREM PROVING VIA LEAN

Traditional reinforcement learning for automated theorem proving often relies on sparse, binary rewards—where a proof is either correct or incorrect. This paper investigates whether the structured, fine-grained feedback provided by the Lean proof assistant can be used to guide language models during training, effectively acting as a process-level oracle to improve reasoning performance.

The researchers treat the Lean proof assistant as a symbolic process oracle. When an LLM generates a proof, Lean parses the tactic sequence and provides two types of signals: a global outcome (pass/fail) and tactic-level feedback (identifying locally sound steps versus the earliest failing step). To integrate this into a reinforcement learning framework, the authors developed a structured credit assignment method. They use a 'first-error propagation' rule, where any tactic following the first failure is penalized, and assign these rewards to the first token of each tactic. This is incorporated into a GRPO-style objective that balances outcome-level and process-level advantages without requiring an auxiliary reward model.

Integrating tactic-level supervision consistently outperforms outcome-only baselines across standard benchmarks, including MiniF2F and ProofNet. The method provides stable and robust performance gains by ensuring that credit assignment is grounded in the formal semantics of type theory. The study demonstrates that symbolic proof assistants are not just evaluation tools, but can serve as active, dense reward sources during the training process, bridging the gap between the scalability of language models and the reliability of formal verification.