大語言模型時代的形式化數學。

原標題：對話DeepSeek研發團隊前成員辛華劍：如何用大模型把數學家從細節中解放出來｜甲子光年
文章來源：甲子光年
內容字數：18388字

大語言模型時代的形式化數學：辛華劍演講要點

本文總結了辛華劍在UKTI.HUB發表的演講《大語言模型時代的形式化數學》的核心內容，探討了形式化數學的歷史、挑戰、以及大語言模型(LLM)在該領域的應用和未來展望。

1. 形式化數學的歷史與當代挑戰

   形式化數學旨在用精確的符號語言表達數學陳述和證明，其歷史可追溯至萊布尼茨的“普遍語法”和希爾伯特的計劃。然而，當代數學面臨著工程化挑戰：證明篇幅過長、知識管理困難、驗證成本高昂等。例如，開普勒猜想的證明長達300頁，驗證耗時12年。陶哲軒認為，形式化數學結合AI，可使數學研究更高效、協作和規模化，未來甚至可一次性證明數百或數千條定理。

2. 形式化數學作為解決方案

   形式化數學提供了一種解決方案，通過使用Coq、Lean、Isabelle和Mizar等形式化系統，將數學問題轉化為計算機可驗證的形式。借助證明助手軟件(如Isabelle和HOL Light)，可以保證證明的正確性，并有效管理龐大的數學理論體系，例如陶哲軒的Lean blueprints項目。

3. 大語言模型在形式化數學中的應用

   近年來，LLM在解決科學問題和算法競賽上的能力顯著提升，例如OpenAI的模型和DeepMind的AlphaProof。DeepSeek-Prover系列模型，尤其V1.5版本，在形式化定理證明基準上表現突出，并展示了模型“先思考再作答”的能力。其訓練方法包括大規模自動形式化方法來合成證明數據，進行迭代訓練。 未來，LLM有望在提出數學猜想、發現數學抽象、構建完整的數學知識庫等方面取得突破。

4. LLM在形式化數學中的挑戰與局限

   當前LLM在形式化數學應用中仍面臨挑戰，例如數據稀缺、自然語言與形式語言的翻譯難題、形式系統的復雜性等。 需要進一步提升模型的Agent能力，使其能夠在大規模代碼庫上有效工作。

5. LLM對數學研究及其他領域的影響

   LLM的應用將對數學研究、工業規模驗證、數學教育以及一般應用產生深遠影響。它有望幫助數學家快速驗證猜想，加速形式化驗證的普及，保存和傳承數學知識，并促進數學工具在更廣泛領域的應用。

6. 問答環節要點

   問答環節涵蓋了DeepSeek的創新之處、算力利用率的提升、MCTS在模型訓練中的作用、LLM的幻覺問題、AI對科研工作的潛在影響等方面，辛華劍提供了深入的見解和分析。

總而言之，辛華劍的演講強調了形式化數學的重要性及其與LLM結合的巨大潛力。雖然挑戰依然存在，但隨著技術的進步，LLM有望推動數學研究和相關領域的性發展。

聯系作者

文章來源：甲子光年
作者微信：
作者簡介：甲子光年是一家科技智庫，包含智庫、社群、企業服務版塊，立足中國科技創新前沿陣地，動態跟蹤頭部科技企業發展和傳統產業技術升級案例，推動人工智能、大數據、物聯網、云計算、新能源、新材料、信息安全、大健康等科技創新在產業中的應用與落地。