编译器引导的自适应证明搜索与跨模型协同
原标题：Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving
AI 摘要
罗切斯特大学的研究者提出了一种编译器引导的自适应证明搜索框架，用于Lean 4项目级定理证明。该框架通过双模型生成和停滞触发的重采样来探索多样化的起始证明，并利用编译器反馈进行当前最优精化。在miniCTX-v2的七个真实项目上，该方法在pass@预算内将平均通过率提高了12.8个百分点，同时将LLM调用减少了21.9%。
正文节选
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. We propose a compiler-gui