miniCTX-v2

新框架通过编译器指导增强 Lean 4 证明搜索

研究人员开发了一个编译器指导的自适应证明搜索框架，旨在改进 Lean 4 编程语言中的定理证明。该新方法通过使用双模型生成和由停滞触发的重采样来平衡探索和利用，同时通过编译器为基础的比较来优化有希望的证明状态。在真实 Lean 4 项目上的实验表明，与现有基线相比，该方法提供了更好的有效性-效率权衡，显著提高了平均通过率并减少了 LLM 调用次数。