Large language models (LLMs) have demonstrated significant potential in formal theorem proving, yet state-of-the-art performance often necessitates prohibitive test-time compute via massive roll-outs or extended context windows. In this work, we address this scalability bottleneck by exploiting an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts to a compact set of structured failure modes. We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration. We perform tree search that corrects errors locally conditioned on explicit verifier feedback, thereby circumventing the costs associated with accumulating a long history of proof attempts. Extensive evaluations show that our method consistently amplifies the reasoning capabilities of base provers across varying scales. Notably, our approach achieves state-of-the-art performance on PutnamBench among publicly reported $\sim$8B and $\sim$32B parameter models under comparable test-time budgets, offering a scalable paradigm for next-generation verifier-guided reasoning.

翻译：大语言模型在形式定理证明中展现出显著潜力，然而最先进的性能往往需要通过大规模展开或扩展上下文窗口来实现，这导致了难以承受的测试时计算开销。在本工作中，我们利用形式验证中一种富有信息量的结构来应对这一可扩展性瓶颈：观察到编译器将大量多样化的证明尝试映射到紧凑的结构化失败模式集合。我们引入了一个基于学习的精炼框架，利用这种压缩实现高效的学习与证明探索。我们执行树搜索，根据显式验证器反馈局部纠正错误，从而规避累积长序列证明尝试的相关成本。广泛评估表明，我们的方法能在不同规模上持续增强基础证明器的推理能力。值得注意的是，在可比较的测试时计算预算下，我们的方法在PutnamBench上公开报道的约8B和约32B参数模型中均取得了最先进性能，为下一代验证器引导的推理提供了可扩展范 paradigm。