表征初期人类-AI 证明形式化工作流：从理论到实践的深度解读

背景

在数学与计算机科学的交叉领域，形式化证明（Formal Proof）一直被视为验证数学论证有效性的“黄金标准”。几个世纪以来，数学家们通过自然语言撰写证明，虽然逻辑严密，但极易受到人类认知偏差、疏忽或表述模糊的影响。与此同时，计算机辅助证明系统（如 Coq、Isabelle、Lean 等）虽然能够自动验证证明的正确性，但其门槛极高。将非形式化的数学直觉转化为机器可读的形式化代码，这一过程被称为自动形式化（Autoformalization），长期以来一直是该领域的巨大挑战。

近年来，随着大型语言模型（LLMs）和生成式 AI 在代码生成及高层级数学推理能力上的突破，人们开始期待 AI 能够重塑形式化证明的工作流。然而，现有的研究大多集中在基准测试（Benchmarking）上，即单纯评估 AI 模型在特定数据集上的形式化准确率。这种“以模型为中心”的视角忽略了最关键的一环：人如何使用这些工具。

本文源自 arXiv（cs.AI 类别，提交于 2026 年 6 月 2 日），由 Katherine Collins 等人撰写。研究旨在填补这一空白，不再关注 AI 有多“聪明”，而是关注 AI 如何实际融入人类数学家的日常工作流，以及人类在面对工具局限性时的适应策略。

核心内容

本研究采用混合方法（Mixed-methods analysis），深入探讨了 AI 对形式化工作流的初期影响。研究分为两个主要部分：定性调查与受控用户实验。

1. 定性调查：期望、障碍与实际行为

研究首先通过定性调查收集了用户对 AI 辅助形式化的看法，主要涵盖三个维度：

• 用户愿景：人们希望 AI 做什么？
• 感知障碍：阻碍实现这些愿景的因素是什么？
• 实际行为：在实践中，人们如何真正使用并调整 AI 工具？

调查结果显示，用户的偏好虽然多样，但存在一个核心共识：人们渴望 AI 的协助，但必须保留人类在证明发现过程中的高层级控制权。 用户并不希望 AI 完全自动化证明过程，而是希望 AI 作为“副驾驶”，处理繁琐的细节，而由人类把握逻辑主线。

2. 受控用户实验：AI 辅助下的实际表现

为了验证上述观点并评估实际效果，研究团队设计了一项受控用户研究。

• 实验设计：参与者被要求将非形式化的数学问题及其证明转化为形式化代码。实验设置了两个条件：
  1. 无 AI 辅助组：仅依靠人工进行形式化。
  2. 有 AI 辅助组：允许使用 AI 工具进行辅助。
• 变量控制：实验涵盖了不同难度级别和不同领域的数学问题，以测试 AI 在不同场景下的表现。
• 工具使用：参与者被允许灵活选择多种不同的 AI 工具，而非局限于单一模型。

3. 实验结果分析

尽管当时的 AI 工具在“自动形式化”方面仍存在局限性（即无法完美地将自然语言直接转换为无错误的形式化代码），但实验数据揭示了一个显著趋势：

• 准确率提升：在允许访问 AI 工具的情况下，参与者的形式化准确率普遍高于仅靠人工的情况。
• 混合工作流：大多数参与者并没有完全依赖 AI，也没有完全排斥 AI，而是采取了灵活混合的策略。他们利用 AI 生成草稿、查找引理或调试错误，然后由人类进行审查、修正和逻辑重构。
• 工具多样性：参与者倾向于组合使用多个不同的 AI 工具，以弥补单一模型在特定数学领域或推理类型上的不足。

关键要点

• 人类主导，AI 辅助：用户的核心需求并非完全自动化，而是保留对证明发现过程的高层级控制。AI 被视为增强人类能力的工具，而非替代品。
• 准确率显著改善：即使在 AI 自动形式化能力尚不成熟的初期阶段，引入 AI 辅助也能显著提高形式化工作的最终准确率。
• 灵活的工具链组合：没有单一的“最佳”AI 工具。用户倾向于根据问题类型灵活切换或组合使用多种 AI 模型，以应对不同难度和领域的挑战。
• 工作流的适应性：人类并非被动接受 AI 的输出，而是主动调整工作流，将 AI 生成的内容作为起点或参考，通过人工介入确保逻辑的严密性。
• 从基准测试到用户体验：研究指出，仅靠基准测试数据无法全面反映 AI 在真实科研场景中的价值，必须关注人机交互的动态过程。

意义与影响

这项研究对数学、计算机科学以及人机交互领域具有深远的意义：

1. 重新定义 AI 在数学中的地位：它打破了“AI 能否独立证明数学定理”的二元争论，转而关注“AI 如何增强人类数学家的效率与准确性”。这为开发更人性化的数学 AI 助手提供了方向——即侧重于辅助而非替代。
2. 指导工具开发：对于开发形式化证明工具（如 Lean、Coq 的 AI 插件）的研究者而言，结果提示开发者应注重提供可解释性、可编辑性和多模型支持，而非仅仅追求端到端的自动化。
3. 验证混合智能的有效性：研究证实了“人类+AI”的混合智能模式在复杂认知任务中的优越性。这种模式既利用了 AI 的计算速度和模式识别能力，又保留了人类的逻辑直觉和批判性思维。
4. 推动形式化数学的普及：通过降低形式化的门槛并提高成功率，AI 辅助工作流有望吸引更多数学家和程序员参与到形式化验证中，从而加速数学知识的机器验证进程，减少因人类错误导致的数学漏洞。

总之，这篇论文不仅是对当前 AI 形式化能力的评估，更是对未来人机协作数学研究范式的早期描绘。它表明，在 AI 深度融入科学发现的初期，**“受控的、灵活的、以人为核心的辅助”**将是主流且高效的工作流形态。