带验证器落地基准协同进化的自修改Lean证明智能体

设计有效的Lean证明智能体是形式化数学推理的核心挑战。除了构建更强的证明器，近期工作强调Lean周边的工作流：智能体如何分解证明义务、使用工具与编译器反馈、诊断失败、修复证明并维护结构化证明上下文。受代码级自进化智能体启发，我们研究这类工作流能否被进化而非手工设计。我们提出一个自进化的Lean证明智能体：一个小的固定可信运行时包裹完全可变的工作区——证明工作流、提示与工具。与多数针对固定外部基准优化的自进化系统不同，我们的系统让智能体与其基准协同进化：代与代之间，最高分智能体（冠军）经掌握节流的课程更新修订活动任务分布——只有当前层级被掌握后才引入更难的证明义务；单锚重校准让冠军在更新后的基准上重跑，以在难度上升时保持分数可比。所有进化都留在以Lean为根基的验证回路内：无论智能体如何改写自己，只有其行为在可信快照下产出经Lean验证的证明才算成功，且每次尝试必须发出机器可读、以Lean为根基的证明上下文——其表示可演化，但其落地性被强制保证。我们运行协同进化轨迹与固定基准基线各15个活动代，并在留出的miniF2F测试划分上比较：最佳协同进化智能体达45.1%留出解题率，种子为12.7%、最佳固定基准智能体为32.0%，表明以验证器为根基的自进化能在协同进化基准下改进Lean证明工作流。