Structured Hints for Sample-Efficient Lean Theorem Proving

TL;DR

This work investigates whether lightweight inference-time guidance can improve neural theorem proving when using RL-trained Lean provers under strict compute. It introduces a Lean-aware Intermediate Representation (IR) with a fixed prompt schedule to inject tactic skeletons at inference and evaluates on the miniF2F benchmark with a constrained budget ($k=16$ attempts and $1024$ tokens). The results show a substantial relative improvement: 53/244 solved (≈$21.7\%$) with the structured approach versus 37/244 (≈$15.2\%$) baseline, a ≈$43.2\%$ gain, with 19 Structured-only wins and 3 Baseline-only wins; error distributions remain similar, suggesting gains come from higher hit-rate rather than avoiding specific errors. The work suggests that cheap, inference-time structural priors can complement heavy RL training, enabling better performance in resource-constrained settings and points to future directions in dynamic or learned skeleton selection.

Abstract

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.

Figures (1)

• Figure 1: Venn diagram detailing the overlap of solved problems