Monte carlo search improves solving formal proofs in lean4 framework
Reap: Uncovering Monte Carlo proof search with a lightweight model
Artificial Intelligence
Summary
Finding formal proofs can be very complex and slow. The authors created Reap, a tool that combines neural networks with a search algorithm to improve how these proofs are found, all while working inside the Lean4 environment. Their model, Reaper-1, learns to organize proofs better and relies less on trial-and-error, leading to stronger performance than similar-sized systems. This approach helps the automated prover make smarter decisions and handle bigger proof steps efficiently.
What this means in practice
- •For software engineers building verification tools: Design formal verification systems that find proofs more efficiently by integrating neural-guided search techniques within interactive theorem provers.
- •For developers of artificial intelligence assistants: Create smarter programming assistants that can generate or verify code correctness proofs using learned proof search strategies.
Authors
Yutong Wang, Xuanzhi Ren, Tianyi Xu, Ruitong Liu, Jingda Xu, Peihao Wu, Bryan Dai, Bin Dong
Abstract
We present Reap, an open framework for learning and analyzing formal proof search in Lean4. Reap implements policy-value-guided Monte Carlo Tree Search directly in Lean, sharing proof-state transitions, AND-OR search, and replay verification between inference and training rollouts. Structured action logs expose how neural predictions and tactic execution interact during search. Using this framework, we train Reaper-1, a 1.7B-parameter policy-value model, through continued pre-training, supervised tactic learning, and iterative search-based reinforcement learning. Using a separate premise selector, the final system solves 79.9% of miniF2F-test at pass@32, establishing state-of-the-art performance among open provers of comparable size while remaining competitive with substantially larger models. Beyond improved solve rates, our results suggest that RL strengthens the prover's ability to organize proofs around useful intermediate results, favoring substantial advances over repeated local adjustments. This more directed proof construction is accompanied by increasingly elaborate tactic programs: fewer explicit search decisions are needed, while more work is performed within each decision. The resulting trade-off between search effort and tactic execution cost provides insight into how learning changes the prover's problem-solving strategy.