Structured Hints for Sample-Efficient Lean Theorem Proving
This work addresses sample efficiency for theorem proving researchers, but it is incremental as it builds on existing models with a lightweight intervention.
The paper tackled the problem of improving neural theorem provers' efficiency by adding simple structural guidance at inference time, resulting in a 43% relative improvement in pass rate on the miniF2F benchmark.
State-of-the-art neural theorem provers like DeepSeek-Prover-V1.5 combine large language models with reinforcement learning, achieving impressive results through sophisticated training. We ask: do these highly-trained models still benefit from simple structural guidance at inference time? We evaluate a lightweight intervention -- a fixed prompt schedule over 15 common tactic skeletons -- on the miniF2F benchmark. This simple approach yields 21.7% pass@16 compared to 15.2% for standard sampling from the same model, a 43% relative improvement using the same number of samples (k=16) and same maximum generation length (1024 tokens). Our results suggest that even capable RL-trained provers underutilize structural priors available in the tactic language, and that simple inference-time guidance remains a cheap, complementary boost.