哥德爾(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,廣泛應用於智慧農業、智慧教育、智慧校園等領域/場域。興趣多元,喜好藝術、繪畫、寫作,遨遊於科技與人文間自得其樂,著有<閃文集>、<大橋驟雨>。