文 觀察者網專欄作者 潘禺
今年，一場數學競賽初賽結果的出圈傳播，導致了媒體的聚焦和全社會的討論。而在該事件不久之後，其實還有另外一場數學競賽的結果，具有深遠的影響和重要的意義，在媒體上得到的關注卻小得多。那就是2024年的國際數學奧林匹克競賽 （IMO），主角中同樣有科技網際網路巨頭的身影，Google DeepMind的人工智慧AlphaProof和AlphaGeometry 2，答對了6道題中的4道，首次達到了IMO銀牌獲獎者的水平。
AlphaProof解決了2道代數問題和1道數論問題，包括本屆IMO中最難的問題，只有5名參賽者解決了這個問題。AlphaGeometry 2證明了幾何問題，而2個組合問題AI沒能解決。每道題最高可得7分，總共最高42分。人工智慧的最終得分為28分，在解決的每個問題上都獲得了滿分，相當於銀牌類別的最高水平，因為今年的金牌從29分開始。
這一結果表明，AI處理複雜數學推理能力有了顯著飛躍。而數學推理是人類認知能力的一個重要方面，推動了科學發現和技術進步。
對中國來說，這一結果也意味著重大的機遇和挑戰。
下一個在中國能廣泛應用於實際場景的AI領域是哪裡呢？有潛力的肯定包括智能網聯車和文體教等，這些也是國內企業投入的重點。中國社會歷來高度重視教育，家庭在教育上的投入巨大，學區房、課外輔導、留學費用等占到了許多家庭支出的大頭。AI對教育的改變，將深刻衝擊中國社會，數學這一被中國人視為重中之重的基礎學科，又是我們觀察這種影響的一個窗口。
從計算到證明
雖然數學一直被稱為人類心智的榮耀，但人類使用機器作為數學的輔助，有著幾千年的歷史。
早在公元前2400年，類似算盤這樣的工具就已經被發明。17世紀的科學家和發明家布萊茲·帕斯卡（Blaise Pascal）發明了早期的機械計算器，這種機器可以進行簡單的加減運算。20世紀60年代，第一台電子計算器問世。早在20世紀70年代到80年代，世界上的部分高中和大學考試就開始允許學生使用計算器，90年代起，許多國家的教育體系開始正式將計算器作為教學工具，並編寫了相應的課程，鼓勵學生使用計算器進行複雜運算。
美國的SAT數學考試在1994年首次允許學生使用計算器。目前，世界許多國家的標準化數學考試，如AP數學考試、SAT、ACT以及國際數學競賽，允許考生使用特定類型的計算器。用計算器可以幫助學生專注於數學概念的理解，而非繁瑣的計算，這已經沒有太大爭議。中國的基礎數學教育以嚴格和系統著稱，中國學生在PISA這類國際數學評估中的表現十分優異，儘管我們注重學生的計算能力，但也並不在高考中排斥計算器的使用。
機器幫助人類解決數學計算，無論在日常生活、教學還是科研領域，都已經被普遍接受。強大的數學計算工具如MATLAB、Mathematica、Maple已經是許多人工作的必備，適合簡單數學運算和統計分析的Excel更是普及。而在數學證明上，目前機器也在發揮越來越大的作用，這正是巨大變革可能產生的開始。
這次在IMO 2024，數學家陶哲軒做了一場演講，回顧了從早期計算工具到現代的機器學習，數學研究的範式轉變。他談到了許多例子，心智觀察所在這裡結合自己的理解做一些總結和評論。
第一個例子是表格。數學領域的許多重要成果都是通過數論中的表格首次發現的，許多猜想也是通過大量的表格發現的。表格可以理解為資料庫，計算機的一個基本用途就是建立這些有用的資料庫。比如，很多數學家，包括陶哲軒自己，使用一個叫做「整數序列在線百科全書」（Online Encyclopedia of Integar Sequences，OEIS）的資料庫。
第二個例子是科學計算。比如用計算機來建模各種事物，求解大量線性方程或偏微分方程，這幾乎是現代科學研究和工程應用的基石，從天氣預報到風洞實驗，從新材料和藥物的研發到期權定價、核反應堆設計，其應用無處不在。
另一種科學計算是SAT求解器，可以解決一些邏輯難題（布爾可滿足性問題），其原理是通過檢查大量的布爾變量，尋找是否存在一組變量的賦值，使得整個布爾公式為真。通俗地說，比如給你1000個陳述，有的是真的，有的是假的，再給你一些限制條件、變量和法則，讓你證明某些句子的組合邏輯上是真的。通過把數學問題，比如畢達哥拉斯三元組問題，轉換為布爾邏輯問題，利用SAT求解器強大的組合求解能力，能夠有效尋找整數解。
第三個例子是形式化證明輔助。四色定理（任一地圖只用四種顏色就能讓相鄰的國家染上不同的顏色）和開普勒猜想（在三維空間中最有效地堆疊球體，以最大限度填充空間）的證明，都是計算機輔助證明的著名例子。
為了更加簡潔地形式化複雜的證明過程，數學家開始使用Lean平台，Lean將數學命題用形式化語言表達並通過計算機驗證，使得每一個推理步驟都可以自動檢查。這為數學研究提供了極大的便利，也降低了證明複雜定理的出錯率。目前本科數學課程中的基礎內容，比如微積分、群論或拓撲學的基本概念等，都已經被形式化，更多數學領域的內容也在被加入到這個庫中。
數學家Peter Scholze就利用Lean試圖形式化驗證自己的高深數學理論，這些理論需要高層次數學背景和對非常抽象的概念的理解，涉及到對現代代數幾何、範疇論、同調代數和拓撲學的深入掌握。Scholze對自己的證明存有疑慮，也沒有人有本事詳細查看其中的細節。Lean的形式化證明如果能夠成功，意味著形式化數學能處理現代數學的前沿問題。用Lean證明費馬大定理的項目，目前也已經獲得資助並啟動。
陶哲軒自己則致力於以眾包方式來用Lean探索數學。其方法是為大型的複雜證明編寫一個藍圖，將證明分解成數百個小步驟，每個步驟都可以單獨形式化，然後組合起來，最後將長達數萬行的形式化證明轉換回人類可讀的版本，最後這步也是計算機自動生成的。
這樣的好處是，證明過程更加開放，讓數學家們可以更好地分工合作，每個人處理任務圖中自己負責的部分，通常是自己擅長解決的，而不需要理解整個證明。由於Lean可以自動檢查，就能保證每個人的工作達到質量標準。另外，遇到修改，編譯器會自動指出關聯的地方，不需要像傳統的方式重寫整個證明，效率大大提高。
最後一個例子就是當下炙手可熱的機器學習。
AI的數學能力
ChatGPT這樣的大語言模型在簡單的算術計算上會犯錯，因為模型並不是從基本原理推導出答案，而是根據輸入猜測最可能的輸出，這種方法有時候並不奏效。GPT-4的研究人員測試了數百道國際數學奧林匹克（IMO）級別的問題，成功率只有1%，只有一個被簡化後的特定問題答對了。大型語言模型在生成回答時依賴於訓練數據中學習到的模式，儘管訓練數據集非常龐大，但它們可能不包含足夠的邏輯推理或數學證明的示例。
DeepMind的AlphaProof和AlphaGeometry 2這兩個更專門的系統，這次的表現就好得多。
AlphaProof是用於形式化數學推理的系統，結合了預訓練的語言模型和AlphaZero強化學習算法，也就是之前自學掌握了西洋棋、將棋和圍棋的算法。它在Lean中訓練自己證明數學陳述，並通過自動將自然語言陳述翻譯成形式化的數學語言陳述，創建了一個不同難度的形式化問題庫。AlphaProof通過在Lean中搜索可能的證明步驟來生成候選解決方案，然後證明或反駁它們。在IMO比賽前幾周內，它證明或反駁了數百萬問題進行自我訓練，涵蓋不同的難度和廣泛的數學領域。
AlphaGeometry是一個神經符號系統，由神經語言模型和符號推導引擎組成，它們協同工作以查找複雜幾何定理的證明。一個系統提供快速、 「直觀 」的想法，而另一個系統則提供更深思熟慮、更理性的決策。
這有點像諾貝爾經濟學獎得主丹尼爾·卡尼曼在《思考，快和慢》一書中提出的人類思維的兩種系統，快速思考系統是一種快速、直覺式的思維方式，慢速思考系統是一種緩慢、邏輯性強、需要集中注意力的思維方式。
AlphaGeometry 2採用的符號引擎比上一代快兩個數量級。當遇到新問題時，使用一種新的知識共享機制來實現不同搜索樹的高級組合，以解決更複雜的問題。在今年的比賽之前，AlphaGeometry 2可以解決過去25年中83%的歷史IMO幾何問題，而上一代為53%。在今年的IMO 2024中，AlphaGeometry 2在收到形式化後的問題後，19秒內解決了第4題（下圖，要求證明 ∠KIL 和 ∠XPY 之和等於 180°，AlphaGeometry 2 提議構造 E，即 BI上的一個點，使 ∠AEB = 90°）。
訓練AlphaGeometry並不是依靠人工的示例，AlphaGeometry首先生成了10億個幾何對象的隨機圖形，並詳盡地推導出每個圖形中點和線之間的所有關係，找到每個圖形中包含的所有證明，然後逆向工作以找出需要哪些額外的幾何結構（如果有）來得出這些證明。數據經過過濾，排除相似示例，產生一個包含1億個不同難度獨特示例的最終訓練數據集。有了這麼多添加新幾何結構而得到證明的例子，AlphaGeometry的語言模型，就能夠在遇到奧數幾何題時，為添加新結構提出很好的建議。
我們的教育做好準備了嗎
教育對個人成長、社會進步和國家發展都至關重要，人工智慧對教育的影響已經來臨，過去的運作模式和利益結構早晚都將受到衝擊。但或許是因為既有格局的根深蒂固，國內對這方面的討論還不多，但只要想想，同樣長期具備壟斷性的傳媒行業發生了多大變化，就很難忽視這種改變的前景。
人工智慧已經深刻改變了媒體，當人們使用TikTok、抖音、今日頭條之類的應用獲取信息時，算法主導了內容的個性化推薦和分發。這一結果對傳媒行業的影響非常明顯，報紙、電視台等傳統壟斷機構無法再占據流量最大的傳播渠道。
在教學上，AI同樣已經做到了通過分析學生的學習進度、錯誤模式和知識漏洞，提供個性化的學習路徑和習題練習。
比如，Khan Academy就使用機器學習算法，根據學生的答題記錄提供個性化的題目推薦，使學習更具針對性。AI平台ALEKS通過自動化反饋機制幫助學生在練習中獲得即時指導，並通過不同題型進一步鞏固知識。在線平台DreamBox Learning提供自適應數學練習系統，學生的進度可以依據他們的實時表現進行調整，確保學習曲線與能力相匹配。
如今，Google DeepMind在高難度的競賽解題上取得突破，意味著對數學這樣最重要的基礎學科，通過AI的加持，使優質教育資源能充足提供，不再稀缺，技術上的障礙已經基本掃清。
Google正在基於Gemini開發一種自然語言推理系統，這意味著將不需要依賴人類專家將數學問題翻譯成形式化的語言進行處理，能與其它AI系統順利集成。當AI以自然語言解決數學問題後，科教系統的面貌必將改變。
中國教育有三大夢想，因材施教、教育公平和減負。
AI的發展能否帶來社會公平，這歷來是一個有爭議的問題。對於網際網路科技公司來說，用戶的增加意味著技術成本的攤薄。雖然話不能說絕對，但從過去的經驗看，AI提供的教育資源，與別的網際網路服務一樣，也很可能是往普及方向發展的。這意味著，除了帶來因材施教，AI將促進教育公平。
在減負上，AI也能發揮巨大作用。就像計算器對數學考試的影響，導致部分價值不大的計算在教學和考試中被捨棄，而更專注於考察數學思維、概念的理解和運用。AI的影響也有希望進一步優化教學和考試內容，減輕中國學生在某些解題套路上依靠「題海戰術」達到「肌肉記憶」的內卷性消耗。
關注數學的人可能都知道今年國內的一些輿情。某競賽初賽結果的爭議徹底出圈了，某數學大師領銜的某書院的爭議，則一直在小圈子內流傳。但由於涉及到中國教育的金字塔結構和招考錄取的指揮棒，後者對家長和學生的影響面其實並不小。
如果把這兩件事放在一起看，這都說明了數學競賽的門檻很高，數學研究的門檻更高，這條道路只適合極少數的人。這背後牽涉的討論非常複雜，但這個結論大致不差。
為了挑選出這少數人，需要多數人的陪跑。這種陪跑不僅發生在基礎教育階段，很多數學競賽的獲獎者，在因此避開高考，獲得了頂級學府的錄取後，最終也都沒有選擇從事數學研究的道路，這也是網上「IMO金牌與菲爾茲獎」的老生常談了。偏偏數學又是如此重要，社會在一定程度上容忍了投機與內卷的情況，而形成了鼓勵「天才少年」的風氣。但對每一個個體來說，內卷的代價要獨自承受，成長選擇的容錯率都是有限的，缺少退路的攀登難以長久，「一將功成萬骨枯」的情況傷害社會的總體利益，國家努力給教輔降溫，阻止家庭為爭奪教育資源而「升級軍備競賽」，背後也有這樣的考量。
教育是強國之基，教育資源和住宅用地一樣，人為製造出稀缺性，也許能夠造成短期的產業繁榮，卻可能埋下看不見的長久隱患，比如已經被一再討論的原始創新不足問題。考慮人口結構的變化和高學歷人口的規模，和住房一樣，中國優質教育資源稀缺的時代終將過去。
目前，還很難說AI提供的充盈教育資源與個性化輔導，能不能動搖中國教育的金字塔結構，也不清楚教育領域的「今日頭條」，這樣的規則破壞者和秩序顛覆者會在什麼時候出現。但最新的AI技術進展，一定會鼓勵創業者與投資者摩拳擦掌，技術將又一次走在從業者和政策制定者的前面。
來源|心智觀察所
推薦閱讀