商傳媒｜葉安庭／綜合外電報導
隨著人工智慧（AI）生成程式碼的能力突飛猛進，全球正逐漸運行在連人類都難以完全理解的程式碼之上，引發各界對潛在系統性風險的擔憂。一向被視為穩定象徵的數學界，也開始正視這股挑戰，甚至有頂尖數學家因此轉投AI安全領域，呼籲建立全球性的軟體驗證基礎建設。
今年7月在美國費城舉行的國際數學家大會上，曾獲數學界最高榮譽「Fields Medal」的加拿大數學家雅各布·齊默爾曼（Jacob Tsimerman）公開表示，他將離開學術界，轉而投入人工智慧安全研究。他感嘆「世界正在改變」，認為傳統數學職涯的現有形式可能難以維持。
雅各布·齊默爾曼之所以做出此決定，部分原因來自數個月前的一項驚人經驗。今年6月，他與其他八位數學家受邀檢視一個AI模型，該模型宣稱已推翻長達80年的「Erdős單位距離猜想」。最終，這些數學家確認了AI的論證，並花了大量時間將機器的論證轉換成人類可理解的語言。這顯示出一個關鍵轉變：過去新發現的瓶頸是創造知識本身，現在卻變成人類確認的速度，因為AI能不斷產生新發現。
這種「人類難以理解的程式碼」可能帶來的風險已非紙上談兵。今年4月，AI公司Anthropic的Claude Mythos模型便成功在主要作業系統和瀏覽器中找出未知的漏洞。此外，美國國家安全局（NSA）局長曾對聯邦參議員馬克·沃納（Sen. Mark Warner）表示，一款工具在數小時內就「入侵了我們幾乎所有機密系統」。微軟（Microsoft）工程師也曾在某個廣泛使用的產品中發現90個關鍵漏洞。更令人警惕的是，早在2024年7月，一項單純的軟體更新失誤，而非網路攻擊，就曾導致全球航班停擺，甚至醫院營運中斷，凸顯現代社會運作對程式碼的依賴（即「程式碼與社會運作的關聯性」，指我們日常生活中的交通、醫療、通訊等各方面，都仰賴這些看不見的程式碼穩定運作）。許多開發者在撰寫程式碼時，也已習慣用自然語言提示（prompt）生成式AI來輔助寫作（即「vibe code」），這雖然加快了開發速度，但也產生了大量連開發者自己都無法完全理解的程式碼。
為應對這股挑戰，專家們提出「形式化驗證」（formal verification）作為解決方案。形式化驗證是一種透過數學方法證明軟體正確性的系統，要求程式碼、規格說明與數學證明環環相扣，只有當每個邏輯步驟都被自動檢查並確認無誤時，程式碼才能被接受。這能避免對程式碼的「盲目信任」。國際數學聯盟（International Mathematical Union）今年6月也通過《Leiden Declaration》，警示AI對證明可驗證性造成的威脅。儘管生成式AI工具已使形式化驗證更容易推廣，但接下來的挑戰是如何正確撰寫規格說明，這仍需仰賴人類的判斷力。這種嚴謹的驗證機制，雖無法阻止網路釣魚或全面確保AI模型安全，卻能有效排除關鍵軟體中大部分的程式錯誤，降低系統性風險（指當一個環節出錯就可能引發全面崩潰的危機，就像骨牌效應一樣）。
報導指出，美國應將這種數學嚴謹性視為國家級任務，建立起驗證軟體的公共基礎設施，包括開放的驗證元件與規格說明資料庫、制定標準與基準、開發更好的更新檢查工具，並推動相關訓練計畫。營運關鍵基礎設施的企業應從設計初期就納入稽核與形式化驗證機制，而非僅仰賴事後修補。數學界過去曾透過更精確的語言、更嚴格的標準與更好的驗證方法，度過數次信任危機。如今，隨著AI編寫的程式碼越來越多地支撐著世界運轉，軟體開發也需要一次類似的轉型。
