今天小編分享的科學經驗：DeepSeek加持，北大幾何模型達IMO金牌水平！32個CPU核心和1塊4090就能實現滿血解題，歡迎閱讀。
國產 AI 幾何模型性能達 IMO 金牌水平，打平谷歌 DeepMind 最新 AlphaGeometry 系列——
TongGeometry，使用的策略網絡和價值網絡還來自微調版本的DeepSeek-Coder。
它能解決 IMO-AG-30 題中的所有 30 題，在 IMO-AG-50 上也能解決 42 題，而人類金牌選手平均水平分别為：25.9、40.9。
例如，下面是 TongGeometry 提出的一道 IMO2024 幾何題的解法，與标準答案完全一致：
TongGeometry不僅能解題還會出題，所出的題目甚至獲得了權威數學競賽認可。
就在去年全國高中數學聯賽預賽北京地區的考試中，就有 TongGeometry 出的幾何題；由美國 IMO 競賽教練組組織的一項美國民間數學競賽 USEMO，也收錄了 TongGeometry 出的兩道幾何題在他們的競賽短表中。
TongGeometry 由北京通用人工智能研究院打造，下文是更多細節。
DeepSeek 加持神經網絡基礎
IMO 是面向全球 200 多個國家，最頂尖高中生，所舉辦的最有影響力的數學競賽。這項競賽要求參賽選手對代數、數論、幾何、組合四項類型的問題有深刻的理解。其中，幾何學問題，又常常因為其優美的圖形性質，受到眾多參賽選手和數學愛好者們的熱議。
△Th é bault 定理，2003 年前曾一度被西方認為是最難證明的幾何定理之一
業界通常認為，能夠代表國家參加該項賽事并獲得金牌，是個人在數學研究歷程上的莫大榮譽。菲爾茲獎得主陶哲軒（Terence Tao）教授，就曾經是該項賽事最年輕的金牌得主。
△陶哲軒教授參加 IMO 比賽歷史記錄
對比賽而言，幾何題的難點就在于如何恰到好處地添加輔助線，使得原先難以推理出來的結論，能夠借助輔助的點、線、圓來得到。構建這些推理的橋梁，是解決這類問題的關鍵。
通常，非常困難的問題需要添加數條輔助線才能完成定理的證明。
谷歌 DeepMind AlphaGeometry 最早提出了使用結合語言模型和邏輯引擎解決此類問題的方案。
在他們的方案中，語言模型負責提出可能的輔助線，推理引擎則負責檢查添加輔助線後所能產生的結論是否是我們正在尋找的。如果所需要證明的定理仍然不在其中，系統則需要繼續搜索可能的輔助線構造方案。
在最新的工作中，AlphaGeometry 宣稱其工作超越了奧林匹克競賽金牌得主的平均水平，能夠解決 IMO-AG-30 數據集上的所有 30 題，并能解決 IMO-AG-50 上的 42 題。
而人類金牌選手的平均水平分别是，25.9 和 40.9。
△AlphaGeometry 系列工作在數據集上的表現
在 AlphaGeometry 最新工作公布後，北京通用人工智能研究院的 TongGeometry 工作也浮出水面。
相比較 AlphaGeometry1/2，TongGeometry 有如下改進：
摒棄算數推理（AR），僅僅使用歸納數據庫方法（DD）
嚴格構造對稱圖形，确保幾何圖形上的優美性
使用馬爾可夫鏈構造樹形狀搜索結構，并使用人類數據啟發數據生成樹的搜索方向
利用策略網絡（Policy）和價值網絡（Value）聯合 Beam Search 進行解題
純粹的歸納數據庫方法
相比較 AlphaGeometry，TongGeometry 摒棄了 DD+AR 的方法，轉而只使用 DD。
據悉，AR 方法由于計算慢，效率低，在實際測試中的嚴重影響性能。TongGeometry 使用的 DD 方法，包含類似 AlphaGeometry 使用的 10 個核心謂詞：共線（equine），共圓（eqcircle），等長（cong），中點（midp），平行（para），垂直（perp），等角（eqangle），等比（eqratio），相似（simtri），全等（contri）。
這套謂詞表示邏輯，能夠覆蓋 IMO 2000-2024 年的所有幾何題目中的 86.8%。
△歸納數據庫方法構造對稱圖形，确保幾何圖形保持美觀
相比于 AlphaGeometry 僅僅使用随機化的構造方案，TongGeometry 在設計問題搜索時就優先考慮對稱圖形。這種方法來自開源項目 GeoGen。在正式比賽中，多見大量對稱圖形。
因此，使用對稱方法生成數據，能夠在有限數據的情況下，盡可能确保數據符合問題的分布。
△TongGeometry 生成的對稱圖形使用人類數據啟發搜索方向
除了在問題構造的時候優先考慮對稱結構，TongGeometry 在問題生成的時候還将使用人類數據中獲得的分布，指導數據生成方向。
TongGeometry 從往屆 IMO，CMO，以及各大比賽中總共收集 196 題，并使用這個小數據集構造數據。從結果看，這一方法能夠產生大量難度上數倍于現有 IMO 題目的構型。
△使用人類數據進行啟發，TongGeometry 生成的數據難度可數倍于 IMO 現有題目難度利用策略網絡和價值網絡聯合搜索
TongGeometry 在解題過程中，使用了類似 Reinforcement Learning 的 Policy 和 Value 兩個網絡。
Policy 網絡用于提出可能的解題搜索方向。而 Value 網絡用于從 Policy 網絡提出的所有可能搜索方向中，篩選出最有用的幾種方向。
結合 Beam Search 和後端的邏輯推理引擎，TongGeometry 的解題策略能夠形成一個閉環。
△策略網絡和價值網絡聯合搜索解題
此外，TongGeometry 使用的策略網絡和價值網絡都來自微調版本的 DeepSeek-Coder。可以說，DeepSeek 也在默默地助力 TongGeometry 的發展。
△DeepSeek-Coder 在列，作為 TongGeometry 的神經網絡基礎
在性能測試上，TongGeometry 技術報告顯示，TongGeometry 能夠解決 IMO-AG-30 題中的所有 30 題。
根據北京通用人工智能研究院的最新介紹，在 IMO-AG-50 上，TongGeometry 也能解決 42 題。注意到 TongGeometry 的技術報告公布于 2024 年 12 月份，誰才是第一個超過人類金牌選手平均水平的幾何解題工具，還尚值得商榷。
△TongGeometry 在 2024 年 12 月公布的技術報告中的性能指标解題 / 出題樣樣精通
TongGeometry 除了是一個解題達人，還是一個出題教練。TongGeometry 的訓練數據包含許多很有價值的幾何關系發現，其中不乏大量具有鏡像對稱和旋轉對稱的美麗構型。
根據報告，這些題目的難度可能數倍于現有的 IMO 競賽題目。
此外，TongGeometry 所出的題目還獲得了數學競賽的認可。在 2024 年全國高中數學聯賽預賽北京地區的考試中，TongGeometry 所出的幾何題就正式亮相。
△TongGeometry 在全國高中數學聯賽北京卷和美國奧林匹克競賽中的供題
去年北京地區的考生，可能神不知鬼不覺地已經經歷了一次來自 AI 的測試。另外，由美國 IMO 競賽教練組組織的一項美國民間數學競賽 USEMO，也收錄了 2 題幾何題在他們的競賽短表中（shortlist）。
△北京卷賽題幾何部分記錄高效推理，性能提升 18 倍
相比 AlphaGeometry 需要 246 個 CPU 核心和 4 塊英偉達 V100 的高性能計算集群才能在 90 分鍾解決一題相比，TongGeometry只需要 32 個 CPU 核心和 1 塊 4090 就能實現滿血解題。
在這一配置下，TongGeometry最多用時僅僅需要 38 分鍾。
△AlphaGeometry 将解體時間控制在 90 分鍾需要使用 246 核心 CPU 和 4 塊英偉達 V100 的高性能計算集群
相比 AlphaGeometry 使用 246*90 核心分鍾相比，TongGeometry 僅僅需要 32*38 核心分鍾，性能提升 18 倍有餘。在這個配置要求下，你的黑神話主機，都能用來學習幾何了。
△TongGeometry 僅僅使用 32 個 CPU 核心和 1 塊 4090 就能将解題時間控制在 38 分鍾内
論文鏈接：https://arxiv.org/pdf/2412.10673
— 完 —
投稿請工作日發郵件到：
标題注明【投稿】，告訴我們：
你是誰，從哪來，投稿内容
附上論文 / 項目主頁鏈接，以及聯系方式哦
我們會（盡量）及時回復你
一鍵關注 點亮星标
科技前沿進展每日見
一鍵三連「點贊」「轉發」「小心心」
歡迎在評論區留下你的想法！
