模拟协作揭示：AI证明智能体与人类偏好系统性偏移

摘要：研究提出“模拟协作”方法，在Lean历史仓库中重放人类证明轨迹并比较AI智能体与人类对下一步证明目标的偏好。基于9个大型协作项目、470万条定义和6000余次提交，研究发现：AI更追逐显式标记的缺口，回避高连接密度的证明中心和复杂目标，同时倾向采用“意外”的证明体并将其规范化。该工作把形式化数学协作的评估重点，从“能否生成可验证证明”推进到“证明策略是否与人类互补”，也为智能体训练与人工审查设计提供干预方向。

---

研究结论：可验证不等于会协作

AI证明智能体在Lean中持续生成机器可检验的证明，并不意味着其工作方式天然适合数学家协作。研究使用“模拟协作”方法重放9个大型Lean项目，覆盖约470万条定义和6000余次提交，并比较AI智能体与人类贡献者在证明推进过程中的注意力分配和下一步选择。

核心发现是，AI与人类的证明偏好存在系统性偏移：智能体更强烈地追逐源码或任务中显式标记的缺口，回避连接密集的证明中心以及复杂、出人意料的证明目标；与此同时，它更容易被意外的证明体吸引，并倾向于把这类证明重写为更常规、更接近基线的结构。

“模拟协作”如何工作

该方法的关键不是单独比较最终证明的正确率，而是把大型仓库的版本历史视为近似的人类—智能体协作记录。分析流程大致包括三类信号。

第一类是局部证明结构。研究者可从定义、声明、注释、待办标记和证明依赖关系中提取图结构。证明体之间的连接密度可表示为节点度数分布或局部子图密度；“证明中心”则是多个定理或定义共同依赖的高连通区域。对于图结构，邻接矩阵的行和可近似表示节点的连接强度，但这种度中心性无法完整刻画跨层依赖和语义捷径，因此结论仍需要结合具体项目结构解释。

第二类是任务吸引力信号。显式缺口通常表现为TODO、sorry、未完成占位符或显式待证目标；复杂目标可由依赖数量、证明长度和结构深度等代理指标衡量；意外证明体则可通过其与基线证明模板或既有证明风格的差异识别。

第三类是行为轨迹。方法将人类提交与AI在相同项目上下文中的动作进行对齐，比较双方在每一步选择目标的概率或频率。这样可以把“AI是否能证明”转化为“AI愿意证明什么”，从而分析智能体与人类工作流是否互补。

为什么AI偏爱显式缺口

显式缺口具有高信噪比。它们直接暴露未完成状态，使模型无需推断长期项目意图即可选择行动。对训练良好的代码或证明智能体而言，这类局部信号比探索高连通区域更容易获得可验证反馈，也更符合监督数据和工具调用轨迹中的局部完成模式。

这会形成典型的贪心策略偏差：智能体不断修复已经标出的洞，形式上提高提交数量，却可能回避真正决定项目结构的核心定理。连接密集的证明中心往往意味着更高语义复杂度、更多依赖耦合和更高失败风险；模型选择绕开它们，可以降低局部失败率，却无法解决数学项目的结构性瓶颈。

从工程角度看，这类似于静态分析工具中的“低风险待办”排序：任务越显式，完成信号越清晰，代理优化越容易收敛到局部目标。论文结果说明，仅以通过率、修复数量或平均证明长度评价智能体，会奖励这种局部最优行为。

复杂目标与意外证明体带来的偏置

AI对复杂目标的回避，与其对意外证明体的偏好形成对照。后者并不一定更困难，但与模型熟悉的证明模板差异更大。模型可能在识别到一种可行的新结构后采用它，却又在后续优化中将其“正则化”为常见基线，表现出证明风格逐渐趋同。

这种组合会造成两类协作风险。第一，AI生成的证明可能形式上有效，却缺少人类用于理解和后续扩展的概念结构。第二，人类贡献者的非惯用证明可能遭到无意中的同质化，因为智能体会偏好稳定、局部可复用的表达。随着协作继续，仓库可能积累更多可检查但解释性较弱的证明。

研究揭示的并非模型缺乏形式推理能力，而是其优化目标与数学探索目标不一致。对于机器可检验系统，局部闭合足以获得奖励；真正的数学突破往往要求在旧结构之外提出更强或更简洁的中间概念。

评测局限与工程权衡

该研究建立在历史Lean协作的近似重放上，而不是受控的真人实时配对实验。这种设计具备规模优势，也避免让人类证明者重复劳动，但存在三类偏差。

首先，人类提交通常包含个人计划、临时尝试和外部讨论，Git历史未必完整记录其真实动机；AI轨迹则可能缺少同等强度的中间反馈。其次，9个项目虽包含大量定义，却不能代表所有数学领域，图的连接方式、注释习惯和团队工作流可能影响结论。再次，摘要未披露所比较的智能体模型、提示策略、采样参数及统计显著性，也未说明复杂度和“意外性”的具体操作化定义。

此外，偏爱显式缺口未必总是缺陷。在迁移维护、CI修复和大库补全任务中，快速处理显式TODO可能正是高吞吐策略；真正需要调整的是工作流分配，而非全局禁用这类行为。更合理的评价应同时报告证明闭合率、核心依赖覆盖率、证明多样性、语义一致性，以及对人类后续修改的增量贡献。

对开发者与数学智能体团队的启示

训练与评测流程可以加入四类干预。

1. 重加权任务采样：降低显式缺口的采样概率，提高高连通证明中心和复杂目标的覆盖比例，避免代理被局部完成信号主导。
2. 加入结构多样性奖励：除Lean编译通过率外，奖励能够揭示新引理、缩短依赖链或形成独立证明接口的方案，降低向基线模板收敛的趋势。
3. 分离探索与利用：让一个智能体快速处理显式缺口，另一个模型专门挑战复杂目标；汇总时由人类审查语义新颖性，而不是仅按自动通过数排序。
4. 构建人类偏好轨迹：记录人类为何选择某个目标、为何放弃某个证明体，再训练偏好模型或过程奖励模型，而不只是模仿最终代码。

部署上，还应保留独立的“语义审查”层：Lean内核负责证明是否成立，人类负责陈述是否准确表达原意、依赖关系是否符合研究意图，以及新证明是否增加了概念价值。这与形式化系统中“机器正确但规格错误”的经典风险一致。

总体意义

这项工作把AI形式化研究从“证明生成能力”推进到“协作策略可对齐性”。证明数量不是协作质量，编译通过也不等于数学解释完整。AI倾向显式缺口、回避复杂中心并同质化意外证明体，说明下一阶段训练需要覆盖目标选择、探索广度和过程可解释性，而不只是扩大生成规模。

---

消息来源：ArXiv AI (cs.AI) (2026-11-06)

—— 完 ——

主题标签： #形式化数学 关注 #Lean 关注 #AI智能体 关注 #人机协作 关注 #证明偏好 关注