Characterizing initial human-AI proof formalization workflows
本文通过混合方法研究调查了人工智能对人类证明形式化工作流的初步影响，结果表明，尽管用户渴望保持高层级的人类控制，但获取人工智能工具显著提高了形式化的准确性，并促进了数学家与人工智能之间灵活且协作式的参与。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
将数学想象成一个庞大而复杂的建筑工程。几个世纪以来，人类数学家一直是建筑师和建造者，绘制蓝图（证明）以确保他们的想法是可靠的。但问题在于：检查一份蓝图是否完美无缺是非常困难的，即使是对专家而言也是如此。有时，微小的错误会溜进去，导致地基不稳。
AI（人工智能） 应运而生，它是一种高科技工具，承诺帮助更快地构建和检查这些蓝图。但在我们将钥匙交给机器人之前，研究人员提出了一个至关重要的问题：“人类建造者究竟希望如何使用这些工具，以及他们在现实生活中是如何与这些工具协作的？”
以下是他们研究结果的详细解读，使用了简单的类比：
1. 调查：建造者“想要什么” vs. “恐惧什么”
研究人员首先询问了一群数学家（从学生到专业人士）他们对 AI 的看法。
- 对控制权的渴望： 大多数人并不希望 AI 接管整个建筑工地。他们不希望有一个机器人建筑师在他们注视下从零开始设计建筑。相反，他们希望自己保持工头的角色。他们希望 AI 处理繁重的体力活、重复性的砌砖工作和乏味的文书工作，但他们希望将“大局观”的决策和创意方向保留在自己手中。
- 信任问题： 尽管人们非常喜欢 AI 节省时间的想法，但对其可靠性感到沮丧。这就像拥有一个非常有热情但不太靠谱的实习生，他很擅长找工具，但有时当你想要螺丝刀时，他却递给你一把锤子。许多用户表示：“我在使用它，但我必须反复检查一切，因为我还不能 100% 信任它。”
- “瑞士军刀”式的方法： 人们不想要单一的 AI 工具。他们想要一个工具箱。如果一个工具擅长寻找现有的蓝图但写不出新的蓝图，他们就会切换到另一个专门用于该特定工作的工具。
2. 实验：将理论付诸实践
为了观察这在实际中是如何运作的，研究人员进行了一项受控实验。他们给了七位数学家一组数学问题（有些简单，有些非常难），并要求他们将这些问题转化为一种严格的、计算机可读的语言——Lean。
- 设置： 参与者必须做两次。
- 第一周： 他们独自完成，没有任何 AI 帮助（仅使用文本编辑器）。
- 第二周： 他们可以使用任何他们想要的 AI 工具（聊天机器人、代码助手、搜索引擎）。
- 结果： 当数学家被允许使用 AI 时，他们犯的错误更少了。AI 帮助他们更频繁地完成正确的“蓝图”。
- 时间因素： 有趣的是，使用 AI 并不一定会让他们完成得更快。这是一种权衡。他们需要花时间研究使用哪个工具以及检查 AI 的工作，但最终结果更加准确。
3. 他们实际上是如何工作的：这种“混合”舞步
最有趣的部分是观察他们是如何使用这些工具的。他们并没有只是让 AI 做完工作然后走开。他们开发出了一种混合工作流：
- “人在回路”风格： 大多数参与者表现得像指挥管弦乐队的指挥。他们会向 AI 请求一个建议（比如某个特定的定理或一段代码片段），听取 AI 的意见，然后决定：“是的，这符合要求，”或者“不，这是错的，再试一次。”
- “工具切换者”： 例如，一位参与者使用一个工具来寻找特定的规则，另一个工具来编写重复性的代码部分，第三个工具则用于重写某段代码使其看起来更美观。他们不断地在不同的工具之间切换，以确保正确完成任务。
- “AI 重度型”风格： 少数参与者让 AI 完成了几乎所有的重活，只在最后阶段介入以修正最终产品。这种方法可行，但要求人类必须具备极强的识别错误的能力。
核心结论
该论文得出结论：数学的未来不是人类对抗 AI，甚至不是人类取代 AI。而是伙伴关系。
把它想象成驾驶一辆配备了先进 GPS 的汽车。GPS（AI）可以告诉你最快的路线并提醒你交通状况，但人类（数学家）仍然需要握住方向盘，决定何时绕道，并确保车不会开下悬崖。
研究表明，当人类保持“方向盘”（战略控制）的同时，让 AI 处理“导航”（寻找模式和检查细节）时，他们能构建出更好、更准确的证明。关键不仅在于 AI 有多聪明，还在于人类如何学习适应并使用这些新工具来契合自己的工作风格。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。