数学(及科学)将是黄金时代还是黑暗时代?
[这是 Francesco Maggi 的客座帖子。本博客文章最初以不同的文件格式撰写,后通过人工智能转换而成。—— T.] 大语言模型(LLMs)及其周围构建的研究系统(通常称为“人工智能”)在生成数学证明方面展现了卓越的能力。虽然这些工具的质量和局限性仍然未完全理解,但它们加速发现和在数学以及更广泛的科学与技术领域实现非凡进步的潜力似乎是显而易见的。要充分利用这一潜力,需要将 LLMs 小心整合到各种 STEM 生态系统中,优先考虑赋予新一代科学家权力、发展新的 STEM 专业知识,以及维护开放、合作和独立的科学事业:这就是标题中的“黄金时代”情景。在“黑暗时代”情景中,科学和技术产出在短期内仍会显著增加,但与此同时,独立的人类科学活动将逐渐减弱,新的知识生产将越来越集中于少数人手中,他们变得越来越无法理解所生产的知识。真正的黑暗在于知识变得与人类理解相悖。现实可能会将这两种情景结合在一起。以下八点,我将探讨塑造这一结果的选择,从数学扩展到更广泛的科学,并以可行的提议结束。(1)技术突破是真实的!但是……显而易见,LLMs 已成为强大的研究工具。最近生成的 LLM 证明,比如带有强迫项的 Navier-Stokes 方程的有限时间爆炸解的构造,或准黎曼假设的提议证明,值得数学家们予以高度关注。评估它们的意义需要数学界不断独立的审查、解释和吸收。LLMs 在使用 Lean 书写证明时似乎最为适应。(Lean 是一种证明助手,允许计算机检查正式论证是否在指定的定义和公理下建立了所述主张。)对于那些我们真的希望 LLMs 帮助我们的困难定理,这些 Lean 证明极其冗长,代码行数可达数十万。似乎出现了一种趋势,即证明的 Lean 版本越长,其机器生成的“自然语言”翻译似乎越混乱和不忠实。我们不明白为什么 LLMs 在进行这种翻译时表现得如此糟糕,但截至目前,它们似乎的确在这一任务上陷入了挣扎。因此,对于真正重要的问题,LLMs 能给我们正确的 Lean 证明,但我们无法直接阅读,并且 messy 的自然语言翻译复杂到需要数学家深入研究才能导致人类理解。尽管这种特定的翻译问题在未来可能会改变,但它直接引导我们到一个基本问题:没有人类理解,我们为何在研究数学,甚至获取证明时关心的,除了基准 LLMs?数学是一种非常独特的人类产物。它似乎在我们认知的生物根源上深深扎根。我们识别(人、动物、物体);因此,我们计数,我们拥有数字。我们似乎具备空间和时间的先天概念,并用数字对其进行量化和测量。一些基本的算术和几何形式似乎几乎是人类的天赋。不同的文明构建了不同类型的数学,即使在最近的数学历史中,数学探究的领域观念也发生了巨大的扩展,有时甚至是意外的。(我们甚至可能处于一个存在人类数学和 LLM 数学的情况。这也许在语言层面上是正确的,但在更深刻的意义上也是如此,尽管说这个还为时尚早。)所以我不同意“机器可以证明定理,因此数学已经结束”的说法。没有理解数学的人类,字面上来说,根本没有人类数学——它是人类文化的重要组成部分。如果我们同意不应因难以理解的机器让我们的人本视角受到冲击而放弃数学,那么社会需要更多的数学家,而不是更少。像……多得多。(2)健康的科学怀疑和 LLMs 创造力的局限性。考虑到 LLMs 在数学领域取得的非凡成果,现在对其未来能力有了相当大的期待,此外,我认为在某些时候缺乏冷静理智,这对科学方法并不公正。非凡的表现应被视为待研究的现象,而不是对智能、创造力或甚至意识的推测性结论的证据。后者是科学研究中最困难的合法主题之一。
本站免费、广告极少。如果觉得有帮助,可以请我们喝杯咖啡 —— 任何金额都对持续运营有实际帮助。
☕请我喝杯咖啡