哥德尔(Kurt Friedrich Gödel;1906~1978)在现代逻辑上的成就是独特而伟大的。事实上,哥德尔的成就不仅是一座学术纪念碑,更是长久屹立于学术历史中的地标。逻辑学科因为哥德尔的成就而彻底改变其本质与发展可能性。
在哥德尔的伟大成就中,他的不完备定理(Incompleteness Theorems)是数理逻辑中的基本结果,宣示形式系统的内在局限性,尤其是那些能够表达基本算术的系统。第一定理表明,任何足够强大且一致的形式系统都不可能完备,这意味着该系统内会有无法使用自身证明的真命题。第二定理进一步指出,没有一个系统能够证明自身的一致性。
大型语言模型(LLM),如GPT-4,可以协助数学定理的证明,但与传统方法相比,它们仍有明显的限制。这些模型可以提出想法、建议步骤或提供解释,这些都可能在证明构建过程中发挥作用。它们能处理某些符号运算并形式化某些证明,特别是那些遵循已知模式或来自数学文献中的证明。
然而,LLM无法从零开始进行复杂或新颖定理的深度推论,因为它们的回应基于数据模式,而非形式逻辑推导。
一些专门设计来证明定理的AI系统,如Coq、Lean和Isabelle,依赖严格的形式逻辑,并能生成完全角式化的证明,且这些证明可经过验证确保其正确性。相比之下,大型语言模型缺乏对逻辑和数学结构的形式理解。然而哥德尔的定理表明,某些真理无法由这些AI系统确立,且复杂系统的一致性无法从系统内部证明。
AI无法「打破」哥德尔定理,因为这些定理是逻辑学的基本结果。它们适用于任何具有一定复杂性的形式系统,并且已被证明无误。由于AI运行依赖形式逻辑,它同样受到哥德尔不完备定理的根本限制。
尽管AI无法打破哥德尔的定理,但它能帮助探讨这些定理的影响,模拟不同的逻辑系统,并研究这些限制在各类数学框架中的具体表现。然而,AI无法独立证明复杂或新颖的定理,也无法突破哥德尔不完备定理所设下的限制。
哥德尔说:「我只相信先验的真理。世界的意义在于愿望与事实的分离。数学要麽对人类心智而言过于庞大,要麽人类心智不仅仅是一部机器。事物本身与谈论事物之间是有区别的(I only believe in a priori truth. The meaning of world is the separation of wish and fact. Either mathematics is too big for the human mind or the human mind is more than a machine. There is a difference between a thing and talking about a thing.)
在AI的协助下,我们或许能够进一步探索数学的深邃领域,扩展人类心智的理解范围。
现为国立阳明交通大学资工系终身讲座教授暨华邦电子讲座,曾任科技部次长,为ACM Fellow、IEEE Fellow、AAAS Fellow及IET Fellow。研究兴趣为物联网、移动计算及系统模拟,发展出一套物联网系统IoTtalk,广泛应用于智能农业、智能教育、智能校园等领域/场域。兴趣多元,喜好艺术、绘画、写作,遨游于科技与人文间自得其乐,着有<闪文集>、<大桥骤雨>。