Failed proofs get a second life: a 7B pipeline lifts Isabelle success on miniF2F to 73.8%

Whole-proof synthesis and stepwise tactic generation now sit in one pipeline, and a failed whole-proof candidate is converted into a reusable intermediate structure instead of being discarded. The two paradigms were largely used in isolation: whole-proof synthesis plans well at a high level but errs on detail, while tactic generation handles local steps but lacks global structure. On the 244 test problems of the Isabelle version of miniF2F, the whole-proof synthesis model alone reaches 45.9%, the tactic-based generation model alone 39.3%, a simple union of the two 49.6%, tactic generation with sketch refinement 71.3%, and the full pipeline 73.8%.

The pipeline uses proof sketches as an intermediate representation, separating high-level planning from low-level reasoning and then filling each subgoal inside the sketch. Sketches are built mechanically from the whole-proof model's own candidates, rather than prompted from informal proofs by another model as in DSP. The sketch builder checks each subgoal independently, replacing the other subgoals' proofs with sorry so correct local steps are kept and only failures are left open; sketches are then checked by Isabelle to drop structurally invalid ones, most pass, and sketches reach up to 90% success when detailed tactics are omitted.

Two 7B-scale models are supervised-fine-tuned on optimized Isabelle data and then optimized with reinforcement learning using Isabelle verification as the signal. Training data come from the Isabelle Standard Library and the Archive of Formal Proofs, split by Isabelle's two proof styles, Isar and apply-style, matching the two pipeline stages. The whole-proof model trains on Isar data and the tactic model on apply-style data, both with LoRA; reinforcement learning uses GRPO with rewards of 1.0 for verified proofs, 0.2 for syntactically valid but unverified proofs, 0.0 for invalid outputs and a -0.2 penalty for patterns such as sorry, on a randomly sampled 1% subset of the optimized dataset.

The demonstrated setting is the miniF2F test set in Isabelle/HOL, evaluated with a sampling size of 128 candidate proofs, with all training data drawn from AFP and STD and miniF2F used only for evaluation. The authors' stated next steps are to integrate more advanced proof search into tactic-based generation, to evaluate on broader Isabelle/HOL domains using carefully defined AFP-based evaluation sets, and to develop a more user-friendly integrated system.

The authors note that current ablations do not hold other factors fixed, so improvements are attributed to the post-training pipeline as a whole rather than to supervised fine-tuning or reinforcement learning separately. The proof search in sketch refinement is relatively simple, and as subgoals grow the refinement and evaluation become less efficient with substantial computational overhead; the pipeline relies on Isabelle as a verification oracle, which brings latency and scalability bottlenecks when many candidates are evaluated; training on existing proof corpora may bias the model toward familiar patterns and limit generalization to novel or significantly different proof structures; and the empirical conclusions are limited to miniF2F.