StepFun-Prover Preview: Let's Think and Verify Step by Step

Understand

We present StepFun-Prover Preview, a large language model designed for formal theorem proving through tool-integrated reasoning.

• Using a reinforcement learning pipeline that incorporates tool-based interactions, StepFun-Prover can achieve strong performance in generating Lean 4 proofs with minimal sampling.
• Our approach enables the model to emulate human-like problem-solving strategies by iteratively refining proofs based on real-time environment feedback.
• On the miniF2F-test benchmark, StepFun-Prover achieves a pass@1 success rate of $70.0\%$.