用编译器反馈优化大模型证明搜索，提升成功率并减少调用次数。
Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving
- 双模型生成+编译器触发重采样，平衡探索与利用
- 在pass@32下提升12.8%成功率，减少21.9% LLM调用
- 适合需要高可靠性的形式化验证项目
真实世界中的Lean 4项目定理证明具有上下文依赖性，单纯迭代修正难以有效复用失败尝试。我们提出一种编译器引导的证明搜索框架，通过双模型生成和停滞触发的重采样探索多样化起点，同时利用编译器支持的成对比较指导当前最优路径的精细化修正。在miniCTX-v2的七个真实项目上实验表明，相比pass@k基线，该方法在pass@32预算下平均通过率提升12.8个百分点，同时减少21.9%的LLM调用。
原文摘要 · Abstract (English)
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. 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%.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。