描述人类与AI协作进行证明形式化的初期工作流程

# 人机协作证明形式化工作流的初步研究

来源：https://arxiv.org/html/2606.04273

Katherine M. Collins\* · Simon Frieder\* · 牛津大学 · Jonas Bayer · 剑桥大学 · Jacob Loader · 剑桥大学 · Jeck Lim · Caltech · Peiyang Song · Caltech / 卡内基梅隆大学 · Fabian Zaiser · 麻省理工学院 · Lexin Zhou · 普林斯顿大学 · Shanda Li · 卡内基梅隆大学 · Sam Looi · 牛津大学 · Joshua B. Tenenbaum · 麻省理工学院 · Umang Bhatt · 剑桥大学 · Adrian Weller · 剑桥大学 · Jose Hernandez-Orallo · 瓦伦西亚理工大学 / 剑桥大学 · Cameron E. Freer† · 麻省理工学院 · Valerie Chen† · 卡内基梅隆大学 · Ilia Sucholutsky† · 纽约大学

## 摘要

几个世纪以来，人类数学家一直通过撰写证明来论证其数学主张；然而，自动验证证明有效性长期以来都是一大难题。AI 系统在代码生成和日益高层次数学推理方面的进步，有望彻底改变人们形式化并验证证明的方式。尽管许多研究聚焦于评测当前前沿能力，我们转而研究人们如何使用这些工具。我们对 AI 对人们形式化工作流初期影响进行了混合方法分析：人们声称自己想要什么、他们认为实现这些愿景的障碍是什么，以及他们在实践中如何实际使用和调整 AI。

定性调查表明，人们的偏好多种多样，但总体上希望 AI 在形式化方面提供辅助，同时保持人类对证明发现过程的高层次控制。为了评估人们在上述限制下如何实际将 AI 用于形式化，我们开展了一项受控用户研究：参与者在有无 AI 辅助的条件下，对不同难度和领域的数学问题及其证明进行形式化。尽管当时工具存在局限，在允许使用 AI 工具的情况下，参与者的形式化准确率普遍高于独立形式化时的水平，大多数参与者灵活地选择使用多种不同的 AI 工具。综合来看，我们的工作揭示了 AI 融入形式化工作流的早期阶段，其中人类与 AI 之间存在密切的相互作用。

数学长期以来一直是智能的重要阵地。AI 正在数学推理领域取得巨大进展，在国际数学奥林匹克竞赛中斩获金牌 \(deepmind2025imo\)，甚至帮助数学家攻克了长期悬而未决的研究难题 \(davies2021advancing; romera2024mathematical; ellenberg2025generative; liu2025ai; epochai2026frontiermath; hariharan2026milestoneformalizationspherepacking; openai2026unitdistance\)。然而，面对如此显著的进步，AI 将如何影响——以及正在如何影响——日常数学实践，无论是对专业人士还是对正处于学习阶段的新一代数学家而言，仍是一个开放问题。

AI 对数学实践产生影响的方式和范围，不仅取决于 AI 系统的能力，更取决于人们**实际上**希望 AI 介入其工作流的哪些环节，以及他们如何在实践中构建并实例化新的工作流。在此，我们聚焦于数学工作流中的一个特定环节：形式化定理证明。几个世纪以来，数学家一直从事发现和撰写证明的实践，以严格论证或反驳所猜想的命题。虽然定理证明被培养为获取和确认"真理"的方式，但正式验证证明正确性在历史上一直颇为困难 \(avigad2010understanding; hales2017formal\)。这使一些人猜测许多证明可能存在小错误（甚至有些是实质性错误 \(lamport2023errors\)）。形式数学语言（如 Lean \(moura2021lean\)、Isabelle \(paulson1994isabelle\)、Rocq \(hugo\_herbelin\_2026\_19256047\)）已开始简化形式验证流程，不仅有助于扩展证明验证的规模，甚至能在大型团队中更大规模地推进证明撰写 \(CommelinTopaz2024\)。然而，用这类形式语言撰写证明并非易事，往往也不够直观 \(bayer2024proof\)。

用于形式化的 AI 有望大规模推动人类所撰写证明的形式化进程 \(yang2026formal\)。我们不着眼于评测 AI 能力的提升，而是将目光集中于人与 AI 系统之间的相互作用。具体而言，我们迈出初步步伐，在更具自然情境的环境下刻画人们对 AI 融入定理证明工作流的偏好，以及他们在实践中如何构建此类工作流、如何分配主导权。我们通过混合方法分析来实现这一目标，将定性调查与受控用户研究相结合。

我们对数学学生和研究人员就其 AI 融合的偏好与自我报告的使用情况开展了调查：他们希望在哪些环节集成 AI、他们认为当前实现这些愿景的障碍是什么，以及他们**不**希望 AI 介入的环节。该调查于 2025 年底开展，让我们得以在智能体工具兴起的浪潮之前，一窥人们在愿意委托 AI 与控制 AI 使用之间的偏好光谱，以及他们对当时 AI 工具能否实现这些愿景的看法。

为了解人们在实践中如何切实构建此类工作流，我们设计并开展了一项受控用户研究：参与者被给予数学问题（难度各异，从简单的数论问题到拓扑学问题）及其以非形式数学表达的证明，并被要求用 Lean 对证明进行形式化，分为有无 AI 工具辅助两种条件。我们观察到，尽管当时工具存在局限，参与者在允许使用工具时的形式化准确率普遍更高，这在一定程度上得益于许多参与者灵活设计了多工具工作流。

我们的工作强调了一点：不仅要研究 AI 的能力，还要研究人们对工作流的偏好、他们认为的工作流障碍，以及他们在实践中相对于这些感知到的和实际存在的障碍如何使用工具。

参见图 1：**调查结果：当前与预期的 AI 使用情况。**  
**a**，受访者自我报告的 AI 使用情况及是否贡献过 mathlib 库（作为其参与 Lean 社区程度/经验的指标之一）；**b**，表示偏好形式化工作流不同环节中特定人类与 AI 参与形式的受访者人数。气泡大小表示希望某类参与形式及其涉及（或不涉及）何种 AI 参与的受访者人数。人类参与编码涵盖整体定理证明和形式化过程；AI 参与则更细化地编码于受访者明确表示希望（或不希望）AI 介入的定理证明和形式化工作流的具体环节。注意，调查回复根据参与者的实际表述进行编码（他们可能属于其未报告的其他类别；详见方法部分）。**c–d**，表示给定因素的受访者比例，分别对应他们（**c**）喜欢和（**d**）对 AI 工具感到不满意的方面（调查时）。回复按自我报告的 AI 使用情况细分，未对该问题给出有意义回答的受访者已被排除（31 位受访者中，**c** 有 24 条回复被编码为有意义，**d** 有 27 条）。

## 结果

参见图 2：**调查结果。** 完整的编码调查回复。每列代表一位受访者。若受访者在其回复中提及某一因素，则对应单元格着色。列顶标注受访者自我报告的 AI 使用情况（例如，"极少"使用 AI）。底部标注受访者自我报告的数学经验、形式化经验，以及是否贡献过 Mathlib。

##### 人们对数学工作流中 AI 使用的偏好呈现出异质性，但普遍共享保持高层次控制的愿望。

在通过质量控制筛选的 31 位调查受访者¹中，自我报告的 AI 使用情况差异显著，且几乎不受受访者是否为活跃 Lean 社区贡献者的影响（以是否贡献 mathlib 衡量，见图 1a），也不受其数学和形式化经验多寡的影响（见补充信息 S.I.A2）。受访者对于希望 AI 在数学实践中以何种方式介入哪些环节表达了不同偏好；然而，大多数受访者倾向于 AI 不完全自动化数学的工作流（见图 1b）。尽管许多受访者希望自动化形式化过程的核心环节（70.3%），但提及 AI 用于证明发现的受访者要少得多（40.7%），在提及 AI 参与形式化过程的受访者中，仅有 33.3% 表示希望由 AI 自动化形式化过程的所有环节。相反，大多数受访者（81.7%）表示偏好对整个过程保持完全或至少部分的人类控制（14.8% 表示永远不会使用 AI；66.7% 表示在使用 AI 时倾向于保持高层次的创造性和/或策略性控制；见图 1b 及补充信息表 2）。我们观察到，这一趋势在具有不同 AI 使用水平和先前形式化经验的参与者中均持续存在（见图 2）。

¹ 我们在以下[网页](https://collinskatie.github.io/hai_formalization.github.io/)公开所有匿名化的调查回复。

##### 人们在提出可靠性顾虑的同时仍然使用 AI。

调查刻画了受访者对未来人机协作形式化工作流的愿景，以及当时阻碍实现这一愿景的现实挫折。尽管 AI 使用频率中等至较高的受访者普遍认可 AI 能带来效率提升并减少繁琐工作（图 1b），但最主要的挫折感来自于可靠性不足（图 1d）。值得注意的是，许多提出可靠性顾虑的人恰恰是仍然选择使用 AI 的人（73.3% 表示有时或总是使用 AI 的受访者表达了对可靠性不足的不满）。此外，相当一部分受访者（18.5%）提到了与形式化相关的特定挫折，例如所用 AI 系统难以匹配其预期的形式代码风格，以及缺乏与其特定形式化工作流的整合（见表 2）。这表明，为形式化社区构建更具针对性的 AI 系统、并将评估维度拓展至形式正确性之外，是一个值得深耕的机遇。

参见图 3：**问题求解描述性分析汇总：有无工具访问权限的对比及形式化工作流。**  
**a**，有无工具使用两组的各问题平均准确率（语句和证明均正确形式化，详见附录）；**b**，各问题的平均耗时（分钟）。误差棒表示标准误；**c**，参与者使用的工具类型及每位参与者估计使用的独特工具数量。每行代表一位参与者；**d–f**，参与者中观察到的不同工作流模式：**d**，以人类为主、AI 辅助的形式化；**e**，以 AI 为主、人类辅助的形式化；**f**，多样化的人机协同形式化。

**表 1：参与者自我报告的工具使用情况。** 用户研究结束后，参与者填写了一份问卷，被要求说明在形式化过程中使用了哪些 AI 工具（如有）及其使用方式。我们在此收录参与者的完整回复。参与者并非总能完整报告其在研究中实际使用的所有工具（见方法部分及补充信息 S.I.A4.4）。工具名称按类别着色，与图 3d 对应：内联 LLM、聊天机器人、语义搜索、LLM（其他）。注意，在某些情况下，例如倒数第二行的参与者，他们提到了 GitHub Copilot 的两种用途，横跨我们的两个颜色分类。

##### 人机协作通常能提升形式化准确率，对时间的影响则喜忧参半。

调查捕捉了受访者对未来人机协作形式化工作流的愿景，以及阻碍实现这一愿景的当前挫折。但人们在实践中会怎么做呢？AI 形式化工具能否让人们在形式化方面更有成效？如果可以，他们又是如何选择使用 AI 来弥补当前工具局限的？

为初步探索这些问题，我们开展了一项受控用户研究。七位参与者（形式化经验不等，但均至少对 Lean 有基本了解，并修读过至少一门本科水平的数学课程，详见方法部分）被给予非形式证明，并被要求对语句和完整证明均进行形式化。他们须形式化六个问题，其中三个须独立完成（不使用工具），另外三个可使用任意工具（见方法部分）。

参与者在允许使用工具时的形式化准确率普遍高于不使用工具时（图 3a）。在以参与者和问题为交叉随机截距的线性混合效应模型中（correct ~ tools + (1|participant) + (1|problem)），工具访问权限使答题正确概率提高了 0.30 个百分点（95% CI：[0.10, 0.50]；z = 2.94，p = 0.003；来自 7 位参与者的 n = 42 次试验）。参与者随机截距标准差为 0.20，问题随机截距标准差为 0.28，表明问题难度贡献的方差大于参与者技能。事实上，即便有 AI 辅助，某些问题仍极具挑战性；没有任何参与者解出"问题 G"（见附录图 12）。

AI 辅助对时间没有统计显著影响（图 3b），且高度依赖于具体问题（附录图 9）。类似的线性混合效应模型（time ~ tools + (1|participant) + (1|problem)）显示，工具访问权限对时间无显著影响（6.61；95% CI：[−43.62, 56.83]；p = 0.797；来自 7 位参与者的 n = 41² 次试验）。

² 一位参与者未能分享其中一个问题的录屏，因此我们没有该视频的时间戳。

##### 大多数参与者灵活地构建了自己的多工具工作流。

与调查结果类似，参与者在研究结束后的问卷中表达了对当时可用 AI 工具的多种局限性看法（见补充信息 S.I.A5）。参与者倾向于通过至少两种方式来弥补任一单一 AI 工具的当前局限：使用多种 AI 工具，以及对 AI 输出保持审慎判断。七位参与者中有六位选择使用多种 AI 工具……