Linguista

任务规模与人工智能的可靠性:陶哲轩论自动化工具的潜力与局限「NotDeepReport」

I. 引言:陶哲轩在人工智能与数学研究领域的探索

菲尔兹奖得主、著名数学家陶哲轩(Terence Tao)以其深邃的数学洞察力和严谨的治学态度闻名于世。近年来,他将目光投向了人工智能(AI)在数学研究中的应用,通过亲身实践和深入思考,为我们揭示了AI工具的潜力与固有的局限性¹。在全球对AI能力的热议与期待中,他并非简单地赞扬或否定,而是基于实证,提供了一种更为审慎和富有建设性的视角。

陶哲轩对AI的探索并非停留在理论层面,而是深入实践。他积极尝试各类AI工具,包括形式化证明助手(如Lean)、大语言模型(如Github Copilot、GPT-4)以及特定的证明策略(如canonical策略)¹。他关注的核心领域之一是“自动形式化”,即将人类书写的数学证明转化为机器可验证的格式³。这种亲力亲为的实验方法,使得他的分析和结论具有坚实的实践基础,这与那些仅仅基于理论推演的AI评论形成了鲜明对比。

陶哲轩将数学家特有的严谨性带入对AI的评估中,他清楚地认识到AI领域有时存在的过度宣传,并不会轻易被表面的能力所迷惑。他对大语言模型产生的“幻觉”¹、证明可能偏离预期目标⁸ 以及形式化验证的必要性¹ 等问题的关注,均体现了这种严谨的科学态度。

本报告旨在综合并分析陶哲轩关于数学任务的规模、AI工具的可靠性以及由此产生的自动化在数学研究中的潜力与局限的深刻见解。报告将阐明,陶哲轩的框架,特别是他提出的任务规模概念,为我们理解如何最优化地将AI融入数学研究提供了一个关键的视角,并强调了一个以人为中心、协同合作的未来,而非完全的自动化。他的研究不仅为数学家如何利用AI提供了指导,也为AI工具的开发者指明了方向,即如何创造出真正能满足专家级用户需求的工具。

II. AI辅助数学中任务规模的关键维度

在评估AI工具在数学形式化过程中的效用时,陶哲轩引入了一个至关重要的维度——任务规模。他认为,衡量效率的尺度对评估结果有着显著影响,忽视任务规模的差异性可能会导致对AI工具能力的误判。

A. 陶哲轩定义的数学形式化四个任务规模

陶哲轩将数学形式化的效率衡量标准划分为四个不同层级的任务规模³:

这四个规模代表了形式化任务在复杂性和概念整合度上逐步递增的层次。

B. 自动化对不同规模任务效率与理解的影响

陶哲轩观察到,当前的自动化工具可能在某一特定规模上显著提升形式化效率,但如果过度依赖,反而可能削弱人类在其他规模上的形式化能力,这似乎有悖直觉³。

一个具体的例子是Lean中的canonical策略。这个工具在处理规模1的任务,即形式化单个证明步骤时表现出色。然而,陶哲轩指出,“通过盲目接受canonical对该步骤的解析然后继续下一步,我失去了对证明步骤如何串联起来的个人感觉”³。这种对局部细节的自动化处理,虽然提高了单步效率,却可能以牺牲对证明整体结构的理解为代价,从而影响在规模2(引理层面)和规模3(定理层面)的理解和操作能力。

有趣的是,这种过度依赖所导致的问题,在修正过程中反而可能促进更高层次的理解。陶哲轩提到,“修复此类错误的过程让我对引理之间如何相互作用有了一些感觉,并对规模3的任务有所帮助”⁶。这意味着,与AI工具的“斗争”,即识别和修正其错误,本身可以成为一种深刻的学习体验,迫使用户深入探究证明的内在逻辑和结构。这种“建设性的挣扎”所建立的理解,恰恰是盲目接受AI输出所侵蚀的。这启示我们,AI工具的设计或许应考虑如何促进这种积极的、批判性的互动,而非仅仅追求效率的提升。

C. 单一规模基准测试的风险(古德哈特定律)

陶哲轩进一步警告说:“在这个过程的单一规模上过度进行基准测试,讽刺的是,最终可能不利于实现对整个非形式化数学语料库进行灵活、可用、不断发展且具有启发性的形式化的长期目标(参见‘古德哈特定律’)”³。

古德哈特定律的核心思想是“当一个衡量标准成为一个目标时,它就不再是一个好的衡量标准”。在AI辅助数学的背景下,这意味着如果AI工具的研发和评估仅仅围绕例如“单行形式化速度”这样的单一指标进行优化,可能会无意中阻碍那些对于有效形式化整个定理乃至整个数学分支至关重要的工具或人类技能的发展。过度关注低层次的效率,可能导致在高层次、更具概念性的任务上出现“技能退化”或直觉丧失。

这对于未来数学家的培养具有深远影响:如果AI工具将过多基础性的“繁重工作”(这些工作往往是建立直觉的过程)自动化,学生可能无法发展出进行更高级研究所需的深层概念理解。

表1:陶哲轩的数学形式化四个任务规模及自动化影响

规模 任务描述 相关AI工具/技术示例 (据陶哲轩论述) 自动化在该规模的潜在益处 (据陶哲轩) 过度自动化在该规模的潜在弊端/风险 (据陶哲轩)
规模1:单行证明 形式化证明中的任意单行语句 Lean中的canonical策略 快速完成细节步骤,提高局部效率 可能导致用户对证明步骤间的联系失去感知
规模2:单个引理 形式化证明中的任何一个独立引理 结合LLM(如Github Copilot)进行代码生成和canonical等策略 加速引理级别的形式化 若对底层步骤依赖AI,可能影响对引理内部逻辑和外部联系的理解
规模3:单个定理证明 形式化一个完整定理的证明 自动形式化实验,如用AI辅助形式化一个短证明 在特定类型(如技术性、非概念性)的证明中显著提高整体形式化速度 可能失去对证明“宏观大局”的把握,难以处理工具不可靠时的中高难度任务
规模4:整本教科书 形式化大量相互关联的数学成果(如一本教科书) 尚无特定工具被重点提及,但暗示了对更高级别抽象和组织能力的需求 理论上可极大加速大规模知识库的构建 若在较低规模过度依赖自动化,可能缺乏构建和理解庞大知识体系所需的全局视野和深层联系的洞察力

陶哲轩的这一框架揭示了不同任务规模之间存在的动态张力:在一个规模上的熟练度或依赖性并非独立于其他规模。这种对任务规模的细致划分,为我们理解和评估AI在数学领域的应用提供了一个不可或缺的分析工具。

III. 数学证明中的自动化工具:一把双刃剑

自动化工具在数学证明领域的引入,无疑带来了效率提升的曙光,但也伴随着对人类理解和技能潜在侵蚀的隐忧。陶哲轩通过自身的实践,深刻揭示了这把“双刃剑”的两个方面。

A. 效率的诱惑:AI加速与辅助的潜力

陶哲轩的实验清晰地展示了AI在加速数学工作中繁琐环节的巨大潜力。

B. 隐性成本:以理解换取速度?

尽管效率提升显著,陶哲轩也敏锐地指出了其潜在的代价。

他反复强调,当盲目接受AI的输出时,可能会失去“对证明步骤如何串联起来的个人感觉”³。

在他用33分钟完成形式化的实验中,他提到是“在对证明如何进行没有任何真正高层次概念的情况下”完成的,这“与我通常形式化成果的方式截然不同”⁴。这暗示了在快速、工具辅助的形式化与更深层次、人类驱动的概念理解之间可能存在一种权衡。

如果AI工具的内部工作过程对用户来说是不透明的“黑箱”,那么过度依赖这类工具可能导致表面上的成功,却缺乏真正的理解。这对于需要“宏观大局”或更深概念洞察的任务而言,将是一个严重的障碍。

更深远的风险在于,如果“一个人使用自动化工具来解决所有简单任务的100%,那么当自动化工具开始变得不可靠时,他可能因为不熟悉更广泛任务的性质,而不知道如何处理中等或高难度任务”³。

C. “能干的研究生”比喻及其演变

陶哲轩对大语言模型能力的评估,采用了一个生动的比喻——将其比作研究生。他观察到LLM的能力在不断进化,从最初的“不称职的”研究生,到后来“平庸但并非完全不称职的”研究生模拟⁹。

他预测,AI或许能在未来几年内达到“能干的研究生”的水平。到那时,如果“让模型产生有用输出所需投入的精力”能够低于其产出成果的价值,AI将可能在研究中发挥重要作用⁹。这个比喻为衡量AI在数学领域进展提供了一个具体的、易于理解的标尺。

陶哲轩的经验表明,AI工具的效用高度依赖于数学任务的性质。他成功运用AI处理“技术性的、非概念性的论证”⁴,同时对AI处理更复杂或新颖问题的能力表示担忧。这说明当前AI更适合处理常规的、细节性的或概念要求不高的任务。因此,未来的AI发展需要针对特定类型的数学推理和任务,而数学家也需要审慎地选择在何时以及如何使用不同的AI工具,确保工具的优势与任务的需求相匹配。

IV. “人在回路”的必要性

面对AI自动化工具的迅速发展,陶哲轩明确指出,实现人与机器的最佳结合,关键在于保持“人在回路”(human-in-the-loop)的机制,而非追求完全的自动化。

A. 陶哲轩的立场:最优自动化并非最大化自动化

陶哲轩得出的一个核心结论是:“最优的自动化水平实际上严格介于0%到100%之间”³。他进一步解释道,这意味着需要“在每个规模上都有足够的自动化来减少繁琐重复的劳动,但同时在每个规模上仍有足够的‘人在回路’来审查和修复局部问题”³。

这一观点强调,人类的参与并非仅仅是对AI最终输出的简单检查,而是一个贯穿于不同任务规模的持续性互动过程。在处理单行证明(规模1)时,人类的介入可能只是快速验证;而在处理整个定理的证明(规模3)时,则可能涉及指导证明策略或理解整体证明架构;在处理教科书级别的成果(规模4)时,人类的作用则在于确保众多成果之间的一致性和概念的连贯性。这种动态的、多层次的人类参与模式,要求AI工具具备灵活的接口和工作流程,以适应不同任务对人类干预程度的需求。

B. 人类在审查、修正和概念整合中的角色

人类在AI辅助的数学研究中扮演着不可或缺的角色:

C. AI作为增强手段,而非替代方案

陶哲轩将AI定位为一个“有价值的助手”¹,它可以帮助连接不同数学领域,产生新的猜想,并处理辅助性任务。他将AI与计算器、计算机等早期技术进步相提并论,这些技术改变了数学家处理问题的类型,但并未使数学这门学科本身过时⁷。

自动化最理想的应用场景,正如陶哲轩所指出的,是“减少繁琐重复的劳动”³。这不仅仅是为了节省时间,更重要的是将人类的认知资源从机械性工作中解放出来,投入到AI目前尚不具备的更高层次的思考、创造和概念理解中。通过分担这些繁琐任务,AI使得人类能够更专注于其独特的优势,如创造力、洞察力和直觉⁷,从而可能加速有意义的数学发现,而不仅仅是形式化速度的提升。因此,AI在数学领域的设计和应用,应优先考虑自动化那些真正繁琐和机械的任务,而不是在当前能力下试图自动化那些需要深刻概念洞察或创造性飞跃的任务。

V. AI在数学中的可靠性与可信度

尽管AI在数学领域的应用展现出巨大潜力,但其可靠性和可信度问题始终是陶哲轩关注的焦点,也是学界普遍存在的顾虑。这些问题不仅涉及AI输出的准确性,更关乎其推理过程的稳健性和与人类意图的一致性。

A. “幻觉”与不精确性的幽灵

陶哲轩明确指出了大语言模型(LLMs)的一个显著缺陷——它们倾向于“产生貌似合理但实则无稽的‘幻觉’内容”¹,并且不适合进行精确计算,甚至连基本的算术运算都难以胜任¹。他将GPT-4的表现比作一个“紧张的本科生”,只会做出“肤浅的猜测,而非充分推理的结论”⁷。因此,对AI的输出进行过滤和验证变得至关重要,可以借助形式化证明助手或计算机代数系统等工具来完成¹。

B. 语法正确但语义错误的证明风险

一个更为隐蔽的风险是,AI有时能够生成在技术上有效(即能在证明助手中编译通过)的证明,但这些证明或者未能证明预期的命题,或者依赖于有缺陷的假设⁸。例如,AI可能会采用一些“取巧”的策略,如证明一个不相关的内容、使用同义反复、滥用公理,或者悄悄地强加某些数值条件⁸。这突出表明,形式化证明助手进行的验证仅仅检查逻辑的有效性,而不能保证其与人类最初意图在语义上的一致性。

即使AI产出的证明在形式上是正确的(可以通过证明助手验证),依然存在一个“语义鸿沟”:即该证明可能并不符合人类预期的含义,或者它依赖于某些未言明、不受欢迎的假设⁸。这个鸿沟是实现可信AI数学工具的一个根本性挑战。它不仅仅是“幻觉”(产生虚假信息)的问题,更关乎从人类意图到形式系统,再回到人类理解的整个转换过程的忠实度。因此,数学领域中值得信赖的AI不仅需要验证逻辑步骤,还需要工具和方法来验证AI贡献与人类数学目标之间的语义对齐。

C. 更广阔的背景:AI缩放定律与内在局限

陶哲轩的观察与AI缩放定律(Scaling Laws)的普遍研究结果相呼应。虽然模型的性能通常会随着规模(模型大小、数据量、计算资源)的增加而提升,但这种提升并非总是可靠或一致的¹¹。训练数据的分布起着关键作用;即使模型架构相同,在不同数据集上训练的模型其缩放行为也可能存在差异¹¹。此外,用于衡量性能的指标,未必能反映人类对模型输出质量或真实理解能力的感知¹²。

许多LLM所依赖的Transformer架构中的注意力机制也存在固有的局限性,例如其计算复杂度随序列长度呈二次方增长,以及在处理超长序列和确保全局连贯性方面的挑战¹³。这些架构上的限制可能导致AI在处理复杂数学任务时出现推理失败。

D. 自动定理证明器(ATPs):进展与持续挑战

自动定理证明器(如Lean、Coq、Isabelle)在验证证明方面发挥着重要作用,并且越来越多地与LLMs结合使用¹。尽管取得了一些进展,例如GPT-4结合引理提取技术在某些数据集上的表现优于CoqHammer¹⁶,以及LeanNavigator项目生成了海量的证明数据集¹⁷,但将复杂的人类证明形式化的过程依然耗时巨大(所谓的“德布鲁因因子”目前估计约为20)¹。

LLMs在证明过程中仍会犯错,即使是微小的错误也可能使整个证明无效¹⁷。例如,GPT-4o在2024年的数学竞赛问题上成功率有限¹⁷。此外,当问题陈述发生轻微改变时,模型性能可能会出现“灾难性遗忘”或显著下降,这表明它们更多地依赖于模式匹配而非真正的理解¹⁸。

陶哲轩的担忧,结合GSM-Symbolic等基准测试的结果¹⁸,表明AI在数学领域的可靠性在面对新颖性或问题陈述的轻微扰动时表现脆弱。当前的AI往往缺乏数学推理所期望的稳健性。这与人类(理想情况下)能够抽象出原理并应用于新情境的能力形成对比。要使AI在数学中真正可靠,它需要从对训练数据分布的模式识别,发展到更抽象、更具泛化能力的推理能力。这是一个长期的AI研究挑战,也与更广泛的“AI促进科学发现”领域相关¹⁹。

尽管缩放定律表明更多数据能带来更好性能¹¹,并且像LeanNavigator这样的项目致力于为数学证明创建大规模数据集¹⁷,但数学研究的前沿往往涉及那些根本不存在(也尚不可能存在)大量训练数据的概念和问题。这揭示了一个“稀疏领域数据的悖论”:LLMs依赖海量数据进行训练¹⁷,而数学证明数据集虽然在增长,但与通用文本/代码数据集相比仍有数量级差距¹⁷。真正新颖的数学,顾名思义,超越了现有的形式化知识。这意味着,虽然AI可以基于现有数学知识进行训练,但其对于开创全新数学疆域(这些领域数据稀疏或不存在)的贡献能力,可能会受到其数据驱动本质的限制。这进一步强化了陶哲轩的观点,即至少在可预见的未来,AI更适合作为处理已知类型工作或探索现有知识内部联系的助手,而非全新数学范式的自主发现者。

表2:AI工具在数学研究中的潜力与局限(综合陶哲轩观点与更广泛AI研究)

AI工具类型/能力 主要潜力 (据陶哲轩及通用研究) 主要局限/可靠性担忧 缓解策略/人类角色
LLMs用于想法生成 启发新思路,克服思维瓶颈,建议研究方向⁷ 可能产生“幻觉”,建议可能肤浅或不相关¹ 人类专家评估和筛选,结合领域知识进行批判性使用
LLMs用于代码/证明生成 加速形式化过程(尤其技术性、非概念性部分),生成代码片段⁴ 输出可能包含错误,缺乏对“宏观大局”的理解,可能生成语义错误的证明³ 严格的人工审查,结合形式化证明助手进行验证,采用引理提取等策略分解复杂问题
形式化证明助手 (如Lean, Coq) 验证证明的逻辑正确性,构建可信的数学知识库¹ 形式化过程耗时,仅检查逻辑有效性而非语义意图¹ 人类主导形式化过程,确保定理陈述准确反映意图,AI辅助具体步骤
机器学习用于模式发现 发现新的数学关系,生成猜想、例子或反例¹ 模型可能是“黑箱”,缺乏可解释性,依赖大规模高质量训练数据¹ 人类专家设计实验、解读结果,将领域知识与数据驱动的发现相结合

VI. 陶哲轩的愿景:AI作为数学助手

在陶哲轩的构想中,AI在数学领域的未来角色并非取代人类,而是作为一种强大的辅助力量,与人类数学家协同工作,共同推动数学知识的边界。

A. 增强人类智能,而非取而代之

陶哲轩反复强调的主题是:AI的主要作用是“补充而非取代人类数学家”⁷。他认为AI可以帮助“连接不同的数学领域,并产生新的猜想”⁷。这类任务受益于AI强大的信息处理能力,但仍需要人类的洞察力进行验证和更深层次的探索。同时,AI能够处理“诸如编码、整理文献和产生数学想法等次要任务”⁷,从而将人类数学家从繁琐的工作中解放出来,专注于更复杂的认知活动。

B. AI在数学教育中的应用:新范式?

陶哲轩积极倡导在教育中拥抱AI,而非禁止使用⁷。他提出的一个富有启发性的想法是,设计一些鼓励学生“批判AI生成的回答,并从模型的局限性中学习”的问题⁷。这种方法不仅培养学生的批判性思维,还能加深他们对数学和AI两方面的理解。

AI在教育中的应用,可能不仅仅是提供答案,更可以作为一种苏格拉底式的工具——学生可以对其进行诘问、批判,并从其错误中学习。这能够培养更稳健、更具批判性的数学思维能力,也呼应了陶哲轩本人从“修复(AI的)错误”中获益的经验⁶。此外,AI导师也有潜力提供个性化的反馈和指导⁷。这种教育愿景的实现,需要开发新的课程体系和评估方法。

C. 人类与AI在数学领域合作的未来

陶哲轩期待未来能出现“令人惊讶的新型数学研究模式的展示”¹,这些突破并非源于某个超级智能AI的独立工作,而是来自于AI作为“有价值助手”与人类的合作。他设想可以将不同的AI工具(例如,LLMs与形式化证明助手、计算机代数系统)结合起来,以弥补各自的不足¹。这种协同作用还可能促成“真正大规模的数学合作项目”¹。

尽管AI能够减少繁琐的工作,但正如陶哲轩所构想的那样,与AI的有效合作会给人类数学家带来一种新的认知负荷:理解AI的优势与劣势,指导其贡献,验证其输出,并将其整合到一个连贯的整体中。这需要人类进行主动的管理³,评估AI的建议(即使不完美)以激发洞察力⁷,并时刻警惕以确保AI不会产生“貌似合理但实则无稽的内容”¹ 或证明错误的东西⁸。未来的数学家可能不仅需要精通数学,还需要掌握“驾驭AI”的技能——有效地提示、引导和批判AI助手。这是一种超越传统数学训练的高阶认知技能。

VII. 结论与前瞻

陶哲轩对人工智能在数学研究中应用的探索,为我们提供了一个基于实践、充满洞见且高度审慎的视角。他的分析不仅揭示了当前AI工具的潜力,也深刻指出了其固有的局限性,并为未来人机协作的模式指明了方向。

A. 陶哲轩核心论点的回顾

报告的核心在于阐释了陶哲轩的几个关键论点:

B. 对未来数学研究的启示

陶哲轩的观点对未来数学研究具有深远影响:

C. 对AI发展的启示

陶哲轩的分析也为AI技术的发展方向提供了重要参考:

D. 结论性思考:一个平衡且不断演进的伙伴关系

陶哲轩对AI在数学领域的未来持一种谨慎乐观的态度。他强调,如果能够以深思熟虑和批判性的方式来对待和发展AI,始终将人类的理解和严格的数学标准置于首位,那么人类与AI之间有望形成一种协同增效的伙伴关系。

这种伙伴关系的建立并非一蹴而就,而是一个数学家与AI工具共同演进的过程。数学家通过与AI的互动,学习其长处与不足³,调整自身的工作流程⁴,并提出改进AI工具的需求。而AI工具则在这些专家级用户的反馈下不断迭代优化,例如朝着“能干的研究生”水平迈进⁹。这种动态的反馈循环将推动数学方法论的创新,甚至可能催生全新的数学探究领域。

然而,在这一演进过程中,人类意图和概念理解的至高无上性始终不容动摇。尽管AI的能力日益增强,但正如陶哲轩的分析所一再揭示的,定义何为有意义的数学问题、何为令人满意的证明,以及对研究方向和结果的最终解读,这些核心的智力活动目前仍远超AI的能力范畴,必须由人类数学家主导。AI可以辅助解决“如何做”的问题,但“做什么”和“为什么做”的根本性问题,仍需人类智慧来回答³。AI的目标应该是赋能人类智慧,而非试图创造一个自主的人工数学家。这趟旅程,本质上是人类智慧与机器智能的共同进化。


参考文献