Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving

基于编译器引导的自适应证明搜索与跨模型协同在上下文相关定理证明中的应用

Abstract: Theorem proving in real-world Lean 4 projects is challenging because proofs often depend on project-specific context. While iterative refinement can use compiler errors to repair failed proofs, reusing failed attempts requires careful search control: some proofs provide better starting points than others, and later revisions may degrade a partially correct proof.

摘要： 在实际的 Lean 4 项目中进行定理证明极具挑战性，因为证明往往依赖于项目特定的上下文。虽然迭代细化（iterative refinement）可以利用编译器错误来修复失败的证明，但重用失败的尝试需要谨慎的搜索控制：某些证明能提供比其他证明更好的起点，且后续的修订可能会导致原本部分正确的证明质量下降。

We propose a compiler-guided proof search framework that balances exploration and exploitation. It explores diverse starting points through dual-model generation and stagnation-triggered resampling, while exploiting promising proof states through current-best refinement guided by compiler-grounded pairwise comparison.

我们提出了一种编译器引导的证明搜索框架，旨在平衡探索与利用。该框架通过双模型生成和停滞触发的重采样来探索多样化的起点，同时通过基于编译器基础的成对比较来引导当前最优细化，从而利用有潜力的证明状态。

Experiments on seven real-world Lean 4 projects from miniCTX-v2 show that our method achieves a better effectiveness—efficiency tradeoff than pass@k baselines. Within the pass@32 budget, our method improves average pass rate by 12.8 percentage points while reducing LLM calls by 21.9%.

在来自 miniCTX-v2 的七个真实 Lean 4 项目上的实验表明，与 pass@k 基准相比，我们的方法在有效性和效率之间取得了更好的平衡。在 pass@32 的预算内，我们的方法将平均通过率提高了 12.8 个百分点，同时将大语言模型（LLM）的调用次数减少了 21.9%。