自动定理证明为科学发现的递归自我改进提供了自然基础。然而，现有的神经证明器未能完整保留这种递归结构——学习过程应随时间自我提升。已有方法要么通过昂贵的权重更新将证明经验嵌入模型参数，要么仅在当前问题内部保留已验证的中间推理。此外，这些方法高度依赖稀疏的全局证明反馈，即使不成功的部分尝试也可能包含有价值的发现。
为弥合上述差距，我们提出 ProofEvolve，一种神经‑符号框架，利用神经模型演化显式、形式化验证的符号证明结构，从而决定性地扩展知识边界。框架中，神经模型负责生成变异算子，包括分解、修复和模式重组。每一次证明转移均由 Lean 核心进行符号验证。
在演化循环中，ProofEvolve 对产生的证明有向无环图（DAG）计算已验证闭包。对每个问题，系统在行为索引档案中演化部分 AND‑OR 证明 DAG；跨问题时，经过核检查的模式提取将新证明的子 DAG 加入持久化的模式库。证明 DAG 通过类型化的模式重组继承已解结果，剩余的前提则作为新的子目标暴露。该演化过程保留了不完整尝试中的已验证结果，并在后续证明中复用，而不削弱形式化可靠性。
在三个竞争级别的 Lean 基准上，ProofEvolve 在所有评测系统中实现了最高的平均求解率。
博主点评：ProofEvolve 将神经网络的探索能力与 Lean 的形式化保证相结合，提供了一条可持续累积证明经验的路径。其 DAG‑驱动的进化机制尤其适合长期自我改进的科研 AI，值得进一步关注与实验。