编译到压缩：通过编译器输出增强形式定理证明

大语言模型 (LLM) 在形式定理证明方面展示了巨大的潜力，但最先进的性能通常需要通过大规模部署或扩展上下文窗口进行令人望而却步的测试时计算。在这项工作中，我们通过利用形式验证中的信息结构来解决这个可扩展性瓶颈：观察编译器将大量不同的证明尝试映射到一组紧凑的结构化故障模式。我们引入了一个学习优化框架，该框架利用这种压缩来执行有效的学习和证明探索。我们执行树搜索，根据明确的验证者反馈在本地纠正错误，从而避免了与积累长期证明尝试历史相关的成本。广泛的评估表明，我们的方法一致地增强了不同规模的基础证明者的推理能力。值得注意的是，我们的方法在可比较的测试时间预算下公开报告的 $\sim$8B 和 $\sim$32B 参数模型中在 PutnamBench 上实现了最先进的性能，为下一代验证者引导推理提供了可扩展的范例。