對(duì) AI 研究者來說，數(shù)學(xué)既是一類難題，也是一個(gè)標(biāo)桿，能夠成為衡量 AI 技術(shù)的發(fā)展重要尺度。近段時(shí)間，隨著 AI 推理能力的提升，使用 AI 來證明數(shù)學(xué)問題已經(jīng)成為一個(gè)重要的研究探索方向。著名數(shù)學(xué)家陶哲軒就是這一方向的推動(dòng)者，他曾表示：未來數(shù)學(xué)家可以通過向類似 GPT 的 AI 解釋證明，AI 會(huì)將其形式化為 Lean 證明。這種助手型 AI 不僅能生成 LaTeX 文件，還能幫助提交論文，從而大幅提高數(shù)學(xué)家的工作效率和便利性。

如今，已經(jīng)誕生了 Gemini 2.0 Flash Thinking 和 o1/o3 等強(qiáng)大推理模型，那么用 AI 來進(jìn)行形式化數(shù)學(xué)推理又已經(jīng)走到了哪一步呢？

Meta FAIR 和斯坦福大學(xué)等多所機(jī)構(gòu)的一篇新的立場(chǎng)論文（position paper）或許能為你給出這個(gè)問題的答案。

• 論文標(biāo)題：Formal Mathematical Reasoning: A New Frontier in AI
• 論文地址：https://arxiv.org/pdf/2412.16075

本文一作楊凱峪在 X 上表示，AI4Math 的下一步是使用證明助手等形式化系統(tǒng)來實(shí)現(xiàn)形式化數(shù)學(xué)推理。他也在推文以及論文中感謝了陶哲軒等數(shù)學(xué)家提供的反饋。

Meta 研究科學(xué)家田淵棟也分享轉(zhuǎn)發(fā)了這篇立場(chǎng)論文，并表示很期待看到 AI 能基于現(xiàn)有的互聯(lián)網(wǎng)數(shù)據(jù)在數(shù)學(xué)階梯上能到達(dá)何種高度。

這篇論文的內(nèi)容相當(dāng)豐富，機(jī)器之心將在此介紹該論文的主要內(nèi)容結(jié)構(gòu)，尤其是該團(tuán)隊(duì)對(duì)多個(gè)相關(guān)研究方向的分級(jí)策略。這些分級(jí)可以幫助我們更好地界定 AI 在形式化數(shù)學(xué)推理方面的進(jìn)展。下圖為該綜述的目錄截圖。

自 AI 誕生之初，研究者就夢(mèng)想著構(gòu)建能夠自動(dòng)進(jìn)行數(shù)學(xué)推理的 AI 系統(tǒng)。歷史上，首個(gè)此類 AI 程序是 Newell 和 Simon 打造的 Logic Theorist（邏輯理論家），這個(gè)定理證明系統(tǒng)能夠證明《數(shù)學(xué)原理》中的 38 條定理。

自那之后已過去數(shù)十年，AI 的中心已經(jīng)從符號(hào)方法轉(zhuǎn)移到了機(jī)器學(xué)習(xí)，并出現(xiàn)了一個(gè)新領(lǐng)域：用于數(shù)學(xué)的統(tǒng)計(jì)式人工智能（AI4Math）。

這是一個(gè)非常吸引人的領(lǐng)域。原因不難理解，很多推理和規(guī)劃任務(wù)本質(zhì)上都是數(shù)學(xué)問題。另外，數(shù)學(xué)在定量學(xué)科中起著基礎(chǔ)性作用，因此 AI4Math 有可能給科學(xué)、工程和其他領(lǐng)域的人工智能帶來革新。也正因?yàn)檫@些原因，LLM 開發(fā)者通常會(huì)把數(shù)學(xué)問題求解能力作為一個(gè)核心衡量指標(biāo)，人們也在努力創(chuàng)造能在數(shù)學(xué)問題上比肩甚至超越人類的 AI 系統(tǒng)。

AI4Math 的重要性吸引了大量研究者，他們開始使用來自自然語(yǔ)言處理（NLP）領(lǐng)域的技術(shù)來開發(fā)數(shù)學(xué) LLM。

一種常用方法是使用數(shù)學(xué)數(shù)據(jù)來對(duì) LLM 進(jìn)行持續(xù)預(yù)訓(xùn)練，比如可以使用來自 arXiv 論文和 MathOverflow 網(wǎng)頁(yè)的數(shù)據(jù)，然后在精心選擇的數(shù)學(xué)問題數(shù)據(jù)集（其中會(huì)提供詳細(xì)的分步解決方案）上對(duì)模型進(jìn)行微調(diào)。該團(tuán)隊(duì)稱之為非形式化（informal）方法。

類似于通用 LLM，數(shù)學(xué) LLM 的配方也很簡(jiǎn)單，秘訣往往在于數(shù)據(jù)的整編。在 GSM8K、MATH、AIMO Progress Prize 等常用基準(zhǔn)上取得進(jìn)展的數(shù)學(xué) LLM 通常包含精心整編的訓(xùn)練數(shù)據(jù)集、思維鏈等推理時(shí)間技術(shù)、自我一致性和工具使用能力。

然而，直到本文寫作時(shí)，非形式化方法得到的 AI 的數(shù)學(xué)能力基本都不超過 AIME 的高中數(shù)學(xué)水平。

那么，問題就來了：非形式化方法的規(guī)模擴(kuò)展之路還能走多遠(yuǎn)？它能讓數(shù)學(xué) LLM 解決更具挑戰(zhàn)性的競(jìng)賽問題（例如，IMO、國(guó)際數(shù)學(xué)奧林匹克）甚至還在研究中的數(shù)學(xué)問題嗎？

從高中到更高級(jí)的數(shù)學(xué)，非形式方法面臨的難題無法僅僅通過規(guī)模擴(kuò)展解決。

首先，訓(xùn)練數(shù)學(xué) LLM 需要高質(zhì)量的數(shù)據(jù)，而高質(zhì)量高等數(shù)學(xué)數(shù)據(jù)很稀缺。對(duì)于新的研究數(shù)學(xué)問題，不可能在互聯(lián)網(wǎng)上找到類似問題的解答或大規(guī)模手動(dòng)標(biāo)注數(shù)據(jù)。如果沒法擴(kuò)大數(shù)據(jù)規(guī)模，就不可能充分享受到 LLM 的 Scaling Law。

第二，很多高等數(shù)學(xué)的解并不是數(shù)值，因此難以通過比較 ground truth 來進(jìn)行評(píng)估。例如證明問題需要一系列復(fù)雜的推理步驟。

LLM 還有個(gè)臭名昭著的幻覺問題，會(huì)生成看起來可行的推理步驟，因此評(píng)估模型輸出或收集有用反饋的難度非常大。

這些問題都難以通過擴(kuò)大非形式化方法的規(guī)模來解決。

如果訓(xùn)練時(shí)間擴(kuò)展不夠用，那我們還需要什么呢？OpenAI o1 展示了一個(gè)可能方向：在推理時(shí)間擴(kuò)展非形式化方法，比如將搜索與神經(jīng)驗(yàn)證器組合起來緩解推理幻覺。

雖然這種方法吸引了很多人的眼球，但它究竟能不能有效解決高等數(shù)學(xué)問題還有待解答。

而本篇立場(chǎng)論文關(guān)注的則是一個(gè)較少被探索的補(bǔ)充方法：形式化數(shù)學(xué)推理（formal mathematical reasoning。

該團(tuán)隊(duì)表示，形式化數(shù)學(xué)推理是指立足于形式化系統(tǒng)的數(shù)學(xué)推理，而形式化系統(tǒng)包括但不限于一階 / 高階邏輯、依賴類型理論和帶有形式規(guī)范注釋的計(jì)算機(jī)程序。

這種形式化系統(tǒng)可提供驗(yàn)證模型推理并提供自動(dòng)反饋的環(huán)境。它們不同于現(xiàn)代 LLM 使用的「工具」，因?yàn)樗鼈兛梢越V泛命題的真與假，并且還是可證明的。此類系統(tǒng)提供的反饋可以緩解數(shù)據(jù)稀缺問題；此外，此類系統(tǒng)還可以進(jìn)行嚴(yán)格的測(cè)試時(shí)間檢查，以抵抗幻覺。

相比之下，非形式化數(shù)學(xué)是指教科書、研究論文和在線數(shù)學(xué)論壇中常見的數(shù)學(xué)文本。非形式化數(shù)學(xué)會(huì)將自然語(yǔ)言與符號(hào)（例如 LATEX）交織在一起，但這些符號(hào)沒有自我包含的形式語(yǔ)義，而是依靠非形式文本來傳達(dá)其含義的重要部分。

AlphaProof 和 AlphaGeometry 是這一想法成功的兩個(gè)突出例子。在此之前，很多研究者嘗試過使用 LLM 來解決奧數(shù)級(jí)數(shù)學(xué)問題，但都失敗了。上述系統(tǒng)的關(guān)鍵區(qū)別在于原則性地使用了符號(hào)表示和證明檢查框架。其中，符號(hào)組件（AlphaProof 的 Lean、AlphaGeometry 的特定領(lǐng)域幾何系統(tǒng)）的作用是執(zhí)行神經(jīng)網(wǎng)絡(luò)的推理步驟并生成高質(zhì)量的合成數(shù)據(jù)，從而實(shí)現(xiàn)前所未有的數(shù)學(xué)推理能力。

AlphaProof 和 AlphaGeometry 之前，已經(jīng)有許多文獻(xiàn)做好了鋪墊 —— 它們探討了形式化方法和機(jī)器學(xué)習(xí)在數(shù)學(xué)任務(wù)中的協(xié)同使用。具體涉及的主題包括神經(jīng)定理證明、自動(dòng)形式化（autoformalization）等。

LLM 的出現(xiàn)大大加速了這一領(lǐng)域的研究。例如，由于缺乏用于微調(diào)的已對(duì)齊非形式化 - 形式化對(duì)，自動(dòng)形式化長(zhǎng)期以來一直都進(jìn)展緩慢。LLM 可以通過合成數(shù)據(jù)或執(zhí)行無微調(diào)自動(dòng)形式化來緩解此問題。因此，人們開始認(rèn)識(shí)到自動(dòng)形式化在引導(dǎo)神經(jīng)定理證明器方面的潛力。LLM 也是定理證明的強(qiáng)大工具；事實(shí)上，最近已有方法利用 LLM 來預(yù)測(cè)證明步驟并修復(fù)有缺陷的證明，同時(shí)還無需基于形式化證明數(shù)據(jù)進(jìn)行明確訓(xùn)練。

圍繞 LLM 和形式化推理的研究基礎(chǔ)設(shè)施正在迅速成熟。Lean 這種用于編寫形式化證明的語(yǔ)言在數(shù)學(xué)家中越來越受歡迎，并催生了形式化研究數(shù)學(xué)和通用數(shù)學(xué)庫(kù)?，F(xiàn)在已有多個(gè)框架可支持 LLM 和 Lean 之間的交互。這些框架支持基于人工編寫的形式化證明提取訓(xùn)練數(shù)據(jù)，以及通過與形式化環(huán)境的交互進(jìn)行定理證明。

除了 Lean 之外，Coq 和 Isabelle 等證明語(yǔ)言的多語(yǔ)言基礎(chǔ)設(shè)施也已在構(gòu)建中 。

最后，LLM 已被用于協(xié)助人類數(shù)學(xué)家編寫形式化證明 ，這可能會(huì)啟動(dòng)一個(gè)數(shù)據(jù)飛輪，其中不斷增長(zhǎng)的人類編寫的形式化數(shù)學(xué)數(shù)據(jù)會(huì)產(chǎn)生更強(qiáng)大的 LLM，從而讓人可以更輕松地創(chuàng)建更多數(shù)據(jù)。

AI 在形式化數(shù)學(xué)推理方面大有機(jī)會(huì)，因而研究繁盛。AI 在形式化數(shù)學(xué)推理方面的新興機(jī)會(huì)導(dǎo)致了研究活動(dòng)的蓬勃發(fā)展。正如最近的一項(xiàng)調(diào)查給出的那樣，該領(lǐng)域的發(fā)表文獻(xiàn)數(shù)量在 2023 年幾乎翻了一番，并且很可能在 2024 年再翻一番。通過將自動(dòng)形式化與強(qiáng)化學(xué)習(xí)相結(jié)合，AlphaProof 成為第一個(gè)在 IMO 中獲得銀牌的人工智能。

該領(lǐng)域的進(jìn)展也可直接應(yīng)用于形式化驗(yàn)證（formal verification） ，這是一個(gè)核心的計(jì)算機(jī)科學(xué)問題，傳統(tǒng)上一直是形式化數(shù)學(xué)最重要的應(yīng)用之一。雖然形式化驗(yàn)證可以得到極其穩(wěn)健和安全的軟件和硬件系統(tǒng)，但從歷史上看，除了安全性至關(guān)重要的應(yīng)用之外，形式化驗(yàn)證其實(shí)很少用，因?yàn)槠洳渴鸪杀咎摺I 可以通過自動(dòng)化形式化和證明工作來大幅降低這一成本。這可能導(dǎo)致未來大規(guī)模生產(chǎn)的軟件和硬件系統(tǒng)比現(xiàn)在更加穩(wěn)健。

該團(tuán)隊(duì)表示：「出于所有這些原因，我們相信基于 AI 的形式化數(shù)學(xué)推理已經(jīng)到達(dá)了一個(gè)轉(zhuǎn)折點(diǎn)，未來幾年將取得重大進(jìn)展。然而，仍有大量工作要做?！?/span>

本立場(chǎng)論文概述了該領(lǐng)域在數(shù)據(jù)和算法方面面臨的難題，以及未來進(jìn)步的可能路線。

AI4Math 與形式化數(shù)學(xué)推理

數(shù)學(xué)推理是 AI 領(lǐng)域的前沿研究方向。本節(jié)首先將介紹 AI4Math 的非形式化方法及其局限性。然后將介紹在推進(jìn) AI4Math 方面，形式化數(shù)學(xué)推理是一條有希望的道路。這一節(jié)涵蓋的內(nèi)容包括：

當(dāng)前最佳的數(shù)學(xué) LLM 以及它們的局限性，目前的難題包括數(shù)據(jù)稀缺、缺乏驗(yàn)證正確性的手段。

用于形式化數(shù)學(xué)推理的 AI：這一節(jié)將介紹從非形式化到形式化的轉(zhuǎn)向、證明助理和 Lean 等。

數(shù)學(xué) AI 的其它方向：AI4Math 范圍很廣，還包含其它許多研究方向，比如使用神經(jīng)網(wǎng)絡(luò)來近似函數(shù)等等。

用于形式化數(shù)學(xué)推理的 AI 的最新進(jìn)展

AI 已在形式數(shù)學(xué)推理方面取得了實(shí)質(zhì)性進(jìn)展。本節(jié)首先將討論兩個(gè)關(guān)鍵任務(wù)的進(jìn)展：自動(dòng)形式化和定理證明。然后將抽樣兩個(gè)相鄰領(lǐng)域 —— 自然語(yǔ)言和代碼生成 —— 它們可受益于形式化方法實(shí)現(xiàn)的可驗(yàn)證推理。

在自動(dòng)形式化方面，本文介紹了基于規(guī)則的自動(dòng)形式化、基于神經(jīng)和 LLM 的自動(dòng)形式化、自動(dòng)形式化的應(yīng)用。

在神經(jīng)定理證明方面，本文介紹了專家迭代、從錯(cuò)誤中學(xué)習(xí)、非正式證明草圖、庫(kù)學(xué)習(xí)、前提選擇和檢索等主題。

此外，這一節(jié)還介紹了自然語(yǔ)言中的驗(yàn)證推理、形式系統(tǒng)驗(yàn)證和驗(yàn)證生成。

挑戰(zhàn)與未來的方向

這一節(jié)，該團(tuán)隊(duì)分享了幾個(gè)仍待解決的挑戰(zhàn)和有希望的研究方向，包括形式化數(shù)學(xué)推理的數(shù)據(jù)和算法、協(xié)助人類數(shù)學(xué)家和證明工程師的 AI 工具，以及集成 AI 和形式化方法來生成可驗(yàn)證代碼。

數(shù)據(jù)

數(shù)據(jù)稀缺是首要問題。潛在的解決方案包括:

• 從教科書、論文和講義中自動(dòng)形式化非形式化數(shù)學(xué)內(nèi)容
• 基于數(shù)學(xué)公理生成合成的猜想和證明
• 從不同的證明框架和代碼等數(shù)據(jù)豐富的領(lǐng)域遷移知識(shí)

算法

在這個(gè)方面，又有許多亟待解決的問題，該團(tuán)隊(duì)也提出了一些解決的設(shè)想：

問題 1：如何讓 AI 能夠自動(dòng)地將非形式化的內(nèi)容轉(zhuǎn)換成形式化的數(shù)學(xué)語(yǔ)言？

• 建立自動(dòng)形式化語(yǔ)句的評(píng)估指標(biāo)
• 將形式化過程分解為小步驟
• 加強(qiáng)與形式系統(tǒng)的交互

問題 2：如何改進(jìn)數(shù)學(xué)推理的模型架構(gòu)？

• 增強(qiáng)多步推理、長(zhǎng)文本處理、抽象和分層規(guī)劃能力
• 通過合成基準(zhǔn)診斷推理失敗之處
• 利用檢索和搜索等推理技術(shù)輔助模型

問題 3：如何有效地搜索證明？

• 對(duì)搜索進(jìn)行擴(kuò)展以利用更多的測(cè)試時(shí)間計(jì)算；
• 對(duì)模型、搜索算法和超參數(shù)進(jìn)行系統(tǒng)性評(píng)估；
• 用于評(píng)估證明目標(biāo)并為其設(shè)定優(yōu)先級(jí)的價(jià)值模型。

問題 4：如何利用定理證明中的層次結(jié)構(gòu)？

• 將大型、高級(jí)證明目標(biāo)逐步分解為較小的目標(biāo)。

問題 5：如何學(xué)習(xí)數(shù)學(xué)抽象？

• 學(xué)習(xí)在成熟的證明助手中構(gòu)建新的定義、引理和策略。

問題 6：如何利用現(xiàn)有的數(shù)學(xué)知識(shí)？

• 為形式數(shù)學(xué)推理量身定制的檢索器；
• 處理動(dòng)態(tài)增長(zhǎng)的知識(shí)庫(kù)。

問題 7：如何協(xié)調(diào)專家方法和通用方法？

• 識(shí)別跨領(lǐng)域聯(lián)系的通用方法；
• 針對(duì)各個(gè)領(lǐng)域的有效性的專家方法以及與數(shù)學(xué)家合作的專家方法；
• 將通用方法和專家方法結(jié)合起來，例如為 LLM 配備特定領(lǐng)域的工具。

用于輔助人類數(shù)學(xué)家的工具

這方面的主要問題是：AI 如何更好地協(xié)助人類研究形式化數(shù)學(xué)？

這個(gè)方面的難題和潛在研究方向包括：

• 資源、激勵(lì)措施和工程開發(fā)，以提高可用性和用戶友好性；
• 研究數(shù)學(xué)家如何使用形式化工具的行為；
• 支持大規(guī)模分布式協(xié)作的工具。

形式驗(yàn)證和已驗(yàn)證生成

這方面的主要問題是：AI 如何輔助人類開發(fā)正確和安全的軟件？

這個(gè)方面的難題和潛在研究方向包括：

• 將形式化方法納入 AI 輔助的系統(tǒng)設(shè)計(jì)和實(shí)現(xiàn)中；
• 增強(qiáng) AI 進(jìn)行形式化軟件和硬件驗(yàn)證的能力；
• 將基于 AI 的生成與形式化驗(yàn)證結(jié)合起來。

評(píng)估標(biāo)準(zhǔn)

在解決問題的過程中，一個(gè)關(guān)鍵問題逐漸浮現(xiàn)：如何有效衡量進(jìn)展？

受自動(dòng)駕駛汽車自動(dòng)化等級(jí)的啟發(fā)，該團(tuán)隊(duì)提出了一個(gè)評(píng)估 AI 數(shù)學(xué)推理能力的分級(jí)框架。他們強(qiáng)調(diào)，在這個(gè)新興領(lǐng)域還需要建立更多新的基準(zhǔn)和評(píng)估方法。

定理證明能力

目前，AI 在形式數(shù)學(xué)領(lǐng)域的主要工作集中在自動(dòng)定理證明上。像 Lean 這樣的形式系統(tǒng)提供了巨大優(yōu)勢(shì) - 一旦找到證明，即使人可能沒完全理解，就能保證其正確性。

研究團(tuán)隊(duì)根據(jù)表 1 給出了 AI 形式定理證明的分級(jí)基準(zhǔn)。

在最基礎(chǔ)的 0 級(jí)水平，AI 能夠識(shí)別正確的形式證明。

到了 1 級(jí)，AI 系統(tǒng)可以提供潛在有用的數(shù)據(jù)，但還不能寫出證明。

2 級(jí)及以上的系統(tǒng)可以生成完整或部分證明。人類專家設(shè)計(jì)和編寫的固定證明策略和規(guī)則，AI 按照這些預(yù)設(shè)的策略執(zhí)行證明過程。

在 3 級(jí)水平，AI 系統(tǒng)能夠在一般領(lǐng)域自動(dòng)證明定理，但仍局限于簡(jiǎn)單定理。

4 級(jí)系統(tǒng)應(yīng)該能夠自主規(guī)劃和執(zhí)行形式化項(xiàng)目，分解大型結(jié)果，提出新的定義和定理，并在探索的過程中嘗試不同的解決方案。

5 級(jí)則意味著系統(tǒng)能夠解決超出人類水平的問題。

自然語(yǔ)言推理驗(yàn)證能力

研究團(tuán)隊(duì)首先提出了一個(gè)問題：如何在不完全形式化的情況下實(shí)現(xiàn)嚴(yán)謹(jǐn)?shù)耐评恚?/span>

他們發(fā)現(xiàn)，讓 AI 在形式系統(tǒng)和自然語(yǔ)言之間切換是一個(gè)很有前景的方向。這樣的 AI 系統(tǒng)應(yīng)該能夠進(jìn)行邏輯推理、數(shù)值計(jì)算，并以嚴(yán)謹(jǐn)且易懂的方式生成答案。

雖然推理過程可能不是嚴(yán)格的形式化證明，但其中的部分內(nèi)容仍可以在人工的監(jiān)督下以半自動(dòng)化的形式驗(yàn)證。該團(tuán)隊(duì)將這種能力稱為「自然語(yǔ)言驗(yàn)證推理」，并提出了一個(gè)分級(jí)框架 (表 2)。

在 0 級(jí)水平，AI 能夠用自然語(yǔ)言生成逐步推理過程，但不涉及驗(yàn)證。

到了 1 級(jí)，AI 系統(tǒng)在生成推理的同時(shí)具備了驗(yàn)證能力，可以評(píng)估每個(gè)推理步驟的正確性。

在 2 級(jí)，AI 系統(tǒng)能夠利用外部工具，執(zhí)行單靠神經(jīng)網(wǎng)絡(luò)難以學(xué)會(huì)的計(jì)算任務(wù)。

第 3 級(jí)的 AI 系統(tǒng)將可以使用外部工具進(jìn)行嚴(yán)格的邏輯推理。

在第 4 級(jí)，AI 系統(tǒng)能夠識(shí)別日常任務(wù)中的數(shù)學(xué)問題并使用嚴(yán)謹(jǐn)?shù)姆椒?。?duì)其進(jìn)行推理

自動(dòng)形式化的能力

該團(tuán)隊(duì)提出了一個(gè)自動(dòng)形式化能力評(píng)估體系，評(píng)估 AI 如何在數(shù)學(xué)知識(shí)的非形式化表述和形式化表述之間自動(dòng)轉(zhuǎn)換。

根據(jù)表 3，在最基礎(chǔ)的 0 級(jí)水平，AI 系統(tǒng)能夠存儲(chǔ)和檢驗(yàn)形式化知識(shí)，方便人工形式化。

在第 1 級(jí)，AI 將可以為自動(dòng)生成形式化的幾種草稿，并通過持續(xù)收集和存儲(chǔ)人類反饋來不斷改進(jìn)系統(tǒng)性能。

到了第 2 級(jí)，AI 應(yīng)能夠在兩者之間進(jìn)行穩(wěn)定且準(zhǔn)確的轉(zhuǎn)換，準(zhǔn)確度接近人類水平。

第 3 級(jí)的 AI 系統(tǒng)能夠在形式化的過程中推斷出缺失餓信息，并標(biāo)記出它無法補(bǔ)全的部分。

在第 4 級(jí)，AI 將具備遇到錯(cuò)誤或?qū)Σ簧系妮斎霑r(shí)自我糾正的能力。

最后在第 5 級(jí)，該團(tuán)隊(duì)預(yù)計(jì) AI 將能夠創(chuàng)造新的數(shù)學(xué)定義，有望降低證明的復(fù)雜度。

猜想能力

研究團(tuán)隊(duì)發(fā)現(xiàn)，在數(shù)學(xué)研究中，提出定理證明之前的猜想階段同樣重要。該團(tuán)隊(duì)認(rèn)為，AI 有望自主提出數(shù)學(xué)猜想。

根據(jù)表 4 的分級(jí)標(biāo)準(zhǔn)，0 級(jí)水平是指 AI 能夠針對(duì)特定問題或目標(biāo)結(jié)果提出相關(guān)猜想。更進(jìn)一步，在 1 級(jí)水平上，AI 就預(yù)計(jì)可以在給定研究領(lǐng)域內(nèi)自主提出猜想，而不必局限于某個(gè)具體定理了。

形式化驗(yàn)證與驗(yàn)證生成的結(jié)果

研究團(tuán)隊(duì)最新發(fā)現(xiàn)，把 AI 應(yīng)用到程序驗(yàn)證和系統(tǒng)開發(fā)時(shí)，面臨的挑戰(zhàn)與數(shù)學(xué)研究有很大不同。為了更好地理解這個(gè)領(lǐng)域，該團(tuán)隊(duì)設(shè)計(jì)了一個(gè) 4 級(jí)能力評(píng)估體系 (表 5)。

在最基礎(chǔ)的第 1 級(jí)，AI 已經(jīng)能夠完成一些簡(jiǎn)單的驗(yàn)證工作，比如檢查小段代碼是否正確，或者自動(dòng)生成一些簡(jiǎn)單的可驗(yàn)證代碼。

到了第 2 級(jí)，AI 的能力提升到可以幫助開發(fā)團(tuán)隊(duì)驗(yàn)證整個(gè)項(xiàng)目，并且能處理更復(fù)雜的問題。

第 3 級(jí)是一個(gè)重要突破，AI 不僅能生成代碼，還能提供證明并幫助維護(hù)系統(tǒng)。

在最高的第 4 級(jí)，AI 可以幫助開發(fā)人員制定技術(shù)規(guī)范，包括自動(dòng)生成規(guī)范文檔、解釋具體要求，以及幫助找出規(guī)范中的問題。