機器之心報道
機器之心編輯部
Meta AI建構了一個神經定理證明器HyperTree Proof Search（HTPS），已經解決了 10 場國際數學奧林匹克競賽 (IMO) 中的數學問題。
數學定理證明一直被視為建構智能機器的關鍵能力。證明一個特定的猜想是真是假，需要使用符号推理等數學知識，比簡單的識别、分類等任務要難得多。
近日，Meta AI 建構了一個神經定理證明器 HyperTree Proof Search（HTPS），已經解決了 10 場國際數學奧林匹克競賽 (IMO) 中的問題，比以往任何系統都更多。此外，該 AI 模型的性能比數學基準 miniF2F 上的 SOTA 方法高出 20%，比 Metamath 基準上的 SOTA 方法高出 10%。
論文位址：https://arxiv.org/pdf/2205.11491.pdf
在一定意義上，定理證明要比建構 AI 來玩國際象棋等棋盤遊戲更具挑戰性。當研究者試圖證明一個定理時，可能移動的動作空間不僅很大而且有可能是無限的。相比較而言，在國際象棋或圍棋中，這些遊戲的一系列走法會被預測出來，即使算法沒有給出最好的走法也影響不大。而在定理證明中，當算法走入死胡同就沒辦法解決了，性能再好的求解器也隻是白費力氣。Meta AI的新方法解決了這個棘手的問題，LeCun也轉推稱贊。
我們用一個例子來說明 HTPS 的優勢：假設 a 和 b 都是質因子為 7 的自然數，并且 7 也是 a + b 的質因子，如果假設 7^7 可以整除(a + b)^7 - a^7 - b^7，那麼請證明 a + b 至少是 19。
假如讓人類來證明的話，他們大機率會用到二項式。而 HTPS 使用 Contraposition 方法，大大簡化了方程，然後再檢查多種不同的情況。
contrapose h₄,
simp only [nat.dvd_iff_mod_eq_zero, nat.add_zero] at *,
norm_num [nat.mod_eq_of_lt, mul_comm, nat.add_mod] at h₄,
如下圖為本文模型發現的證明示例，即在 miniF2F 中另一個 IMO 問題的證明：
更接近人類的推理
為了使用計算機編寫正式的數學證明過程，數學家最常用的方法是互動式定理證明器（ITP）。下圖 1 是互動式定理證明器 Lean 中的一個證明示例：
相應的證明樹如下：
給定一個要自動證明的主要目标 g，證明搜尋與學習模型和定理證明環境互動以找到 g 的證明超樹。證明搜尋從 g 開始逐漸擴充出一個超圖。當存在從根到葉子均為空集的超樹時，即為證明完成。
以下圖 5 證明過程為例，假設政策模型 P_θ 和批評模型 c_θ，以目标為條件，政策模型允許對政策進行抽樣，而批評模型估計為該目标找到證明的能力，整個 HTPS 的證明搜尋算法以這兩個模型為指導。此外，與 MCTS 類似，HTPS 存儲通路計數 N(g, t)（在節點 g 處選擇政策 t 的次數）和每個政策 t 針對目标 g 的總動作（action）值 W(g, t)。這些統計資料将用于選擇階段。
HTPS 算法疊代地重複圖 5 描述的選擇、擴充、反向傳播三個步驟來增長超圖，直到找到證明或者超出擴充預算。
Meta 在三個定理證明環境中開發和測試 HTPS：a）Metamath，b）Lean 和 c）Metamath。Metamath 附帶一個名為 set.mm 的資料庫，其中包含 30k 個人類編寫的定理。Lean 附帶一個由人類編寫的 27k 定理庫，稱為 Mathlib。最後，由于 Metamath 證明非常難以了解，因而 Meta 開發了自己的環境，稱為 Equations，僅限于數學恒等式的證明。
為了模仿人類思維，神經定理證明器需要将特定狀态和目前狀态（對問題的了解）聯系起來。Meta 首先從強化學習開始，該方法與現有的證明助手（proving assistants，例如 Lean）緊密結合。
Meta 将證明的目前狀态解釋為圖中的一個節點，并将每一個新步驟解釋為一條邊。此外，研究者意識到還需要一種方法來評估證明狀态的品質——類似于在棋盤遊戲中 AI 需要評估遊戲中的特定位置。
受蒙特卡洛樹搜尋 (MCTS) 啟發，Meta 采用在兩個任務之間進行循環：在給定證明狀态下使用的合理參數的先驗估計；給定一定數量的參數後的證明結果。
HTPS 是标準 MCTS 方法的變體，在該方法中，為了探索圖，Meta 利用關于圖的先驗知識來選擇一組葉進行展開，然後通過備份修正來改進初始知識。圖是逐漸探索的，關于圖結構的知識随着疊代得到細化。
實驗
每個實驗都在單一環境（例如 Lean、Metamath 或 Equations）上運作，并将模型與 GPT-f 進行比較，它代表了 Metamath 和 Lean 的最新技術。
在 Lean 中，該研究在 A100 GPU 上使用 32 個訓練器和 200 個證明器進行實驗。經過 1 天的訓練（即 (200 + 32) A100 天的計算），miniF2F 中的每個狀态（statement）平均被采樣 250 次，在 327 個狀态中已經有 110 個被解決。本文的模型在 miniF2F-test 中優于 GPT-f，具有大約 10 倍的訓練時間加速。
在 Metamath 中，該研究在 V100 GPU 上訓練模型，使用 128 個訓練器和 256 個證明器，表 3 報告了監督模型和線上訓練模型的結果。
在 Equations 中，該研究使用 32 個訓練器和 64 個證明器進行實驗，在這種環境下，模型很容易學習随機生成器的訓練分布，并解決所有綜合生成的問題。
參考連結：https://ai.facebook.com/blog/ai-math-theorem-proving/