陶哲轩转发、菲尔兹奖得主领衔：AI正在颠覆数学家的工作方式| 美国数学学会特刊 https://www.qbitai.com/2024/04/133814.html 梦晨 陶哲轩：“这个领域发展太快了” 这些文章读起来很有趣，尽管使我自己即将发表的一篇文章显得多余……这个领域发展太 快了！ 作者阵容非常豪华，包括菲尔兹奖得主Akshay Venkatesh、华裔数学家郑乐隽、电脑科学 家Ernest Davis等多位知名学者。 其中郑乐隽表示，如果最终机器能做得比人类更好，那就很好，她将乐意退出数学领域去 弹钢琴。 他们提出的观点包括： AI的数学能力不完全反映人类的认知过程，依赖训练资料中的模式，而不是真正理解问题 的本质。 合成数学如合成拓朴学和合成微分几何学，提供了一种全新的数学实践方式，让数学家专 注於更深层的概念和问题。 互动式证明系统与软体工程中的“规范驱动开发”，可以降低数学家的认知负荷、促进数 学家之间的合作。 形式化证明科技可能改变数学证明的本质、颠覆数学家的工作方式。 数学届不应被科技公司主导的议程所绑架。 在开篇，编委会写道： 纯粹的数学家习惯於享有很大程度的研究自主和智力自由，这是一种脆弱而宝贵的遗产， 可能会因机器的盲目使用而被扫除。 另一方面，对同一技术进行深思熟虑和深思熟虑的方法可能会极大地丰富我们的学科。 学科应该如何发展是由我们自己决定的，因此我们邀请数学界认真思考和讨论专刊中提出 的问题，并聆听其他领域同行对这些问题进行了深入思考。 现在，是数学家们了解并推动这场辩论，并决定学科未来方向的时候了。 AI能自动证明定理吗？ 计算机已经在数学中发挥了重要作用，尤其是在计算效率方面的提升，但是否能够帮助人 类进行数学推理？有一天它们是否会自主进行推理？ 数学家Kevin Buzzard概述了神经网路、电脑定理证明器和大型语言模型的最新发展。 Kevin Buzzard现任英国伦敦帝国学院数学教授，专门研究算术几何和朗兰兹纲领。 回顾整个计算工具的历史，最早Computer一词还指人类作为“计算员”，他们的成就不应 被低估。 17世纪早期，苏格兰数学家John Napier建构了第一个对数表，他提出如果有更多「计算 员」来帮忙，就可以进一步推进这项工作。 另一个代表性成果是Felkel和Vega在18世纪70年代发表的整数因式分解表，这使得研究素 数分布成为可能，最终导致了素数定理的证明。 早期电子计算机出现後，机器在高速运算方面已经远超人类，Computer一词的意思也改变 了。 如剑桥大学在1957年购买了EDSAC II计算机，用於海洋学计算，为现代板块构造理论奠定 基础。 这个阶段计算机还只是一个工具，即使目前的计算机也难以像人类一样进行数学推理和定 理证明。 神经网路可以用来搜寻定理、猜测新定理和寻找反例，如发现了拓朴学中关於结点和边的 关系的新定理，以及在表示论中发现了关於Kazhdan-Lusztig多项式的新结果，但对於证 明深奥复杂的定理还有其限制。 自动定理证明系统（ATP）可以自动证明一些复杂的定理，如罗宾斯猜想。但ATP生成的证 明往往过於冗长，难以被人类理解。 互动式定理证明系统（ITP）可以用来验证定理的正确性，帮助发现和修正数学文献中的 错误，如数学家Peter Scholze在液体张量实验（Liquid Tensor Experiment）中承认自 己无法掌握所有涉及的数学对象和概念，最终在Lean系统帮助下完成。 大模型如ChatGPT虽然可以产生相关数学内容，但容易产生错误。 Buzzard建议大模型与 ITP等系统结合使用，透过大模型产生初步证明，然後由ITP进行验证，从而提高可靠性。 Buzzard认为，这些新兴技术可以帮助数学家突破认知障碍，探索更复杂、更新颖的数学 领域，并最终改变数学家的工作方式，使他们能够将更多时间和精力投入到数学思维和理 解上。 另外三篇文章，从不同角度探讨了这些新兴技术如何帮助数学家应对日益增长的复杂性， 并开拓新的数学领域。 数学的形式化转向 逻辑学家Jeremy Avigad讨论了自20世纪初以来，数学定义和证明可以在具有精确语法和 使用规则的形式系统中表示。 Jeremy Avigad任卡内基美隆大学哲学和数学教授，在数理逻辑和基础、形式验证和互动 式定理证明以及数学哲学和历史领域做出了贡献。 他认为这种转向可能改变数学的本质，依赖机器验证的证明可能减少了数学家对直观理解 和洞察的重视，从而可能影响数学发现的过程和数学思想的发展。 纯数学中的抽象边界与规范驱动开发 数学家Johan Commelin和Adam Topaz探讨了抽象边界（Abstraction Boundaries）如何在 互动式定理证明器的帮助下，帮助控制数学研究中的复杂性。 Johan Commelin任荷兰乌特勒支大学助理教授，Adam Topaz阿尔伯塔大学助理教授，两人 研究兴趣的交点是代数几何，共同参与了液体张量试验。 抽象边界是指在数学研究和定理证明过程中，将数学物件的实作细节与其外在属性和行为 进行形式区分的界限。这种界限使得数学家可以在不依赖具体实现细节的情况下，使用和 推理这些数学对象。 抽象边界的概念在软体工程中非常常见，例如透过C语言的头档、物件导向程式设计中的 公共方法或函数式程式设计中的typeclass来实作。 基於抽象边界的「规范驱动开发」方法，不仅降低了认知负荷，还促进了数学家之间的合 作，使得工作可以轻松分配给具有不同专长的合作者。 奇异新世界：定理证明助手与合成基础 数学家Michael Shulman认为，现有的电脑程式如Lean证明助手，能够验证数学证明的正 确性，但它们专门的证明语言对许多数学家来说是一道门槛。 Michael Shulman任圣地牙哥大学副教授，研究领域为范畴论与代数拓朴。 现有的电脑证明助手能够验证数学证明的正确性，但它们专门的证明语言对许多数学家来 说是一道门槛。大模型有潜力降低这个门槛，使数学家能够以更熟悉的语言与证明助手互 动。 这可能允许数学家使用由模型支持的证明助手探索根本上全新的数学领域，现有的证明助 手已经在同伦类型论（homotopy type theory）等领域发挥了这一作用。 目前的人工智慧可以做严肃的数学吗？ 纽约大学电脑科学家Ernest Davis指出，目前AI在解决文字描述的数学问题上，无法可靠 地结合基础数学和常识推理。 AI透过三种主要方法尝试解决数学问题，但每种方法都有其优点和限制。 直接产生答案，适用於简单数学问题。 产生可执行程式码，已在实践中取得成功。 翻译成逻辑规范，对於复杂问题仍有挑战。 他认为AI在解决数学奥林匹克问题时可能会依赖训练资料中的模式，而不是真正理解问题 的本质，这与人类透过直觉和逻辑推理解决问题的方式有显着差异。 AI真正解决数学问题需要三类知识：基础数学、语言理解和世界常识。例如理解硬币的价 值和物理特性。常识在解决问题时经常被忽视，但实际上是至关重要的。 基准测试集是评估AI系统效能的重要工具，但它们可能无法全面涵盖AI的所有能力。 但同时他也指出，尽管AI在处理基础问题时有限制，但这可能不会影响其进行高阶数 学研究的能力。 一方面，高阶数学研究可能不需要与解决基础问题相同的常识推理能力。 另一方面，在棋类游戏上，即使AI无法理解棋局的基本概念，在棋局分析和策略制定上的 能力能远远超越人类棋手。 数学家如何看待AI？ 关於自动化与数学研究的一些想法 菲尔兹奖得主Akshay Venkatesh探讨了数学自动化对数学研究的影响。他指出，机器可能 大大增强数学解决问题的能力，但也会彻底改变数学的核心问题和价值观，使其难以被人 类所认知。 他分析了当前数学界决定「什麽是重要」的机制，如期刊、奖项、数学理论在应用领域得 到认可、教育体系、聘用和资助过程等，都不足以解释数学界相对较高的共识水平。 他认为「证明」这种特殊的学术交流方式能引发一致同意，类似自由市场中讯息传播的机 制。 AI会导致当前数学界对「重要性」的判断剧变。 机器如何使数学更包容 数学家郑乐隽（Eugenia Cheng）认为，科技已经在改变人们研究数学的方式，可以利用 这些技术让数学更加包容，而不是让数学家变得多余。 郑乐隽在谢菲尔德大学任教，除了范畴论研究和本科教学之外，她的目标是消除世界上的 「数学恐惧症」。 她分析了科技如何影响数学教学、提出问题、协作、传播以及研究： 教学：标准的「粉笔和黑板」式讲授变得没有必要，她开始采用互动性更强的教学方式。 同时对学生来说，记忆现在已经无关紧要，应当将大脑留给更有趣的事情 提出问题：技术使得任何人都可以在网路上提问并获得答复，但继承和放大了数学界的精 英主义和竞争性。 协作：科技大大便利了远端协作，使地理位置不再是障碍。电子白板等工具也大大增强了 协作的便利性。 传播：网路使论文传播普及，不再局限於有限的纸本期刊。这让论文发表过程更加公开透 明，论文品质而非发表管道成为关键。 研究：透过智慧型手机随时随地展开研究，不受地点限制。搜寻引擎等也让她不必记住所 有事实，可以随时查阅。 总的来说，郑乐隽认为科技可以让数学变得更包容，只要数学家善用这些技术，而不是固 步自封。 同时她也提出，如果最终机器能做得比人类更好，那很好，她将乐意退出数学领域去弹钢 琴。 机器时代下的证明 数论学家Andrew Granville关注证明的本质以及电脑证明与人类证明之间的关系。 他认为，纯数学中的「客观性」并非如我们所想那样牢不可破。 定义和概念的困难：现代数学中许多概念没有单一明确的定义，有许多可能的定义和诠释 。这就难以谈「客观」。 公理系统的限制：根据哥德尔不完备定理，即使采用一致的公理系统，也无法证明所有关 於整数的正确语句。这说明「客观的」数学基础是有限制的。 历史演进的影响：不同时代数学家对「数学证明」的理解和标准有所不同，这反映了客观 性标准的变化。 他探讨了电脑自动证明可能同时带来的挑战和机会。电脑证明可以帮助确认人类直观证明 的正确性，提高可信度。但电脑证明可能取代人类，成为「黑箱」证明。但这种证明可能 缺乏人类应有的可理解性和适应性。 Granville希望未来的电脑证明能够吸收人类证明的优点，在形式化的基础上保持足够的 灵活性和易理解性。 自动化迫使数学家反思自己的价值观 哥伦比亚大学数学家Michael Harris强调数学需要吸收其他学科、尤其是人文社科的经验 。 他建议经常反思学科的价值追求和物质基础，有助於数学家在面对自动化等挑战时，更好 地扞卫数学的核心价值。 此外，他也警示数学界不应被科技公司主导的议程所绑架，科技公司的价值取向与数学家 的价值取向并不完全一致，数学家应保持独立思考的勇气，而不是被动接受来自产业的价 值导向。 更多精彩内容7月发布 特刊的第二部分将於2024年7月发布，内容将包括： 自动化与哲学： 形式化所引发的许多问题并不新鲜。 McLarty的文章描述，庞加莱在一个多世纪前就在讨 论「推理机器」。庞加莱已经关注到形式化证明与数学实践之间的关系，这一主题在de Toffolli的文章中得到了进一步的探讨。 科技改变思维 DeDeo的文章检验了自动证明对数学家认知过程的潜在影响。 深度学习与数学的互动 Bengio和Malkin的文章考虑了进行数学研究对机器学习带来的特定挑战。 Fraser和 Poggio的文章则提出了与深度学习数学基础相关的问题。 敬请期待～ 期刊地址： https://www.ams.org/journals/bull/2024-61-02/ 参考连结： [1]https://mathstodon.xyz/@tao/112221953164171331 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 219.87.176.211 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1712552957.A.814.html