編輯:杜偉、大盤雞
本週二,我們報道了菲爾茲獎得主陶哲軒的一個開源專案 —— 在大模型的協助下編寫了一個概念驗證軟體工具,來驗證涉及任意正引數的給定估計是否成立(在常數因子範圍內)。
在專案中,他開發了一個用於自動(或半自動)證明分析中估計值的框架。估計值是 X≲Y(在漸近記法中表示 X=O (Y))或 X≪Y(在漸近符號中表示 X=o (Y))形式的不等式。
這才幾天的時間,這個估計驗證工具的 2.0 版本就來了!

陶哲軒對該工具進行了兩次全面改進。
首先,他將其改造成一個基礎的證明助手(proof assistant),同時能夠處理一些命題邏輯;接著,他根據評論者的反饋,將其改造成一個更加靈活的證明助手(在幾個關鍵方面特意模仿了 Lean 證明助手),它也由功能強大的 Python 符號代數包 sympy 提供支援。
陶哲軒認為現在得到了一個穩定的框架,並可以進一步擴充套件該工具。他最初的目標只是自動化(或半自動化)標量函式漸近估計的證明,但原則上可以繼續向該工具新增策略、新的 sympy 型別和引理,以處理範圍廣泛的其他數學任務。
該證明助手的 2.0 版本已經上傳到了 GitHub。同樣地,與自己以前的編碼一樣,陶哲軒最終「嚴重」依賴大語言模型的幫助來理解 Python 和 sympy 的一些細節,其中 Github Copilot 的自動補全功能尤其有用。
雖然該工具支援全自動證明,但陶哲軒決定現在更多地關注半自動互動式證明,其中人類使用者提供高階「策略」,然後證明助手執行必要的計算,直到證明完成。

GitHub 地址:https://github.com/teorth/estimates
根據專案簡介,這是一個利用 Python 開發的輕量級證明助手,其功能遠遜於 Lean、Isabelle 或 Rocq 等完整證明助手,但希望它能夠輕鬆用於證明一些簡短而繁瑣的任務,例如驗證一個不等式或估計是否由其他不等式或估計推匯出來。該助手的一個具體目標是為漸近估計(asymptotic estimates)提供支援。
具體實現過程
下載相關檔案後,即可在 Python 中啟動證明助手,只需輸入「from main import *」並載入一個預先製作的練習即可。以下是其中一個練習:

這是證明助手對以下問題的形式化描述:如果 x, y, z 是正實數,且 x<2y 且 y<3z+1,則證明 x<7z+2。
證明助手的工作方式是:使用者指示助手使用各種「策略」來簡化問題,直到問題得到解決。在本例中,該問題可以透過線性演算法求解,具體形式化為「Linarith ()」策略:

如果有人想更詳細地瞭解線性演算法的工作原理,可以使用「verbose」標誌(flag)來執行此策略。

有時,證明過程會涉及情況拆分,最終的證明會呈現出樹狀結構。這裡有個例子:其務是證明假設 (x>-1)∧(x<1) 且 (y>-2)∧(y<2) 蘊涵 (x+y>-3)∧(x+y<3):

這裡,根據使用的三種策略對證明進行「偽精益」描述:策略「cases h」 1 對假設「 h1」進行情況拆分,然後在兩種情況下分別應用「simp_all」策略來簡化。
該工具支援漸近估計。陶哲軒找到了一種在 Sympy 中實現量級形式化的方法。事實證明,Sympy 在某種意義上已經可以原生實現非標準分析:它的符號變數有一個「is_number」標誌,基本上對應於非標準分析中「標準」數的概念。
舉例而言,數字 3 的「sympy」版本「S (3)」有「S (3).is_number == True」,因此是標準的;而整數變數「n = Symbol ("n", integer=true)」有「n.is_number == False 」,因此是非標準的。
在「sympy」中,他能夠構建各種(正)表示式「X」的數量級「Theta (X)」,其屬性「 Theta (n)=Theta (1)」如下:如果「n」是標準數,然後使用這個概念來定義漸近估計,例如

(實現為 lesssim (X,Y))。接下來可以應用對數形式的線性算術來自動驗證一些漸近估計。這裡有個簡單的例子:給定一個正整數 N 和正實數 x,y,使得

且

,任務目標是得出結論

:

對數線性規劃求解器還可以透過相當強力的「分支」方法處理低階項。

陶哲軒計劃開始開發用於估計符號函式的函式空間範數工具,例如建立一些策略來部署諸如 Holder 不等式和 Sobolev 嵌入不等式之類的引理。Sympy 框架看起來足夠靈活,可以為這些型別的物件建立更多物件類。目前,他只有一個概念驗證引理來說明這個框架,即算術平均 – 幾何平均(arithmetic mean-geometric mean)引理。

陶哲軒最後表示,他對這個證明助手的基本框架非常滿意,因此願意接受進一步的建議或新功能的貢獻,例如引入新的資料型別、引理和策略,或者一些示例問題。這些問題應該很容易被這個助手解決,但目前由於缺乏合適的策略和引理而超出了它的能力。
數學形式化證明實驗紀實
而就在剛剛,陶哲軒又發了一個新專案。
他最近嘗試了一個小實驗:嘗試利用現代自動化工具(如 GitHub Copilot 和 Lean 證明助手)來半自動地形式化一個一頁紙的數學證明。這個證明來自他在 Equational Theories Project 中的合作者 Bruno Le Floch。

-
影片演示:https://www.youtube.com/watch?v=cyyR7j2ChCI
-
討論地址:https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2
-
GitHub 連結:https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean
陶哲軒嘗試「盲做」這個證明,即不真正理解證明結構的前提下,直接用工具去拼出形式化過程。他用約 33 分鐘完成了形式化過程。對他來說,這是一種很不一樣的工作方式 —— 不靠對整個證明的大局理解,而是完全依賴於工具處理邏輯細節。
在 Zulip 討論中,Bruno Le Floch 最初指出,在論文中「E1689-E2 的所有已知證明都是計算機輔助」這一說法太絕對了。他自己後來給出了一個更具可讀性的「人類版本」,雖有些步驟靈感來自 prover9,但整體不應算作純計算機證明。
陶哲軒回應:那我們可以更新 blueprint,並在論文中註明我們在專案中得到了一個非計算機生成的版本。
故事就此開始,陶哲軒選擇做一個實驗。「我嘗試完全基於 Bruno 的草稿,一步步進行形式化,過程非常依賴 Copilot 和 Lean 的 canonical 策略。」他將原稿拆解成細小邏輯單元,讓工具處理約一半細節,剩下的由自己手動填補,完成了一個可以透過驗證的 Lean 形式化證明,還錄了影片上傳到 YouTube。
實際證明, 雖然這種方法看起來有點機械,但對於結構不強、以技術推導為主的證明,是有效的。AI 工具可以代勞大量繁瑣推理,讓人專注於「如何表達」而不是「是否合理」。
這場實驗還暴露出一些 Lean 專案協作工具的問題。目前專案使用的 blueprint 工具只支援每個命題繫結一個證明版本。如果要同時記錄人類證明和 AI 生成的版本,會發生覆蓋,管理混亂。
如果你對這個話題感興趣,建議直接檢視 Zulip 討論區,瞭解更多一線協作細節。
© THE END
轉載請聯絡本公眾號獲得授權
投稿或尋求報道:[email protected]