NEAR Protocol 已概述計劃，將在其協議與核心智能合約上應用 AI 輔助的形式化驗證，此前其報告在提交時模型成本為 111.85 美元的情況下解決了 672 個數學問題。
摘要
- NEAR 計劃在其協議與核心智能合約上應用 AI 輔助的形式化驗證。
- NEAR AI 報告在提交時模型成本為 111.85 美元的情況下解決了 672 個 PutnamBench 問題。
- 生產驗證需要準確的軟體模型、已定義的需求，以及涵蓋已部署實作的證明。
- 形式化驗證補充測試與程式碼審查，其保證僅限於指定的屬性與假設。
NEAR Protocol 在 10 月 16 日的公告中表示，其研究旨在減少證明軟體遵循既定規則所涉及的專家工作與運算成本。
計劃中的應用涵蓋該網路的協議與核心合約，以及供生態系統開發者使用的工具。NEAR 將生產驗證描述為一個目標，而其已完成的基準工作則涉及自動化數學證明生成。
NEAR 計劃將證明生成移入生產軟體
根據 NEAR 的公告，將該研究應用於運行中的軟體涉及三個階段。開發者必須以數學方式表示程式、定義其應滿足的屬性，並建構證明以顯示這些屬性成立。
NEAR AI 近期的基準結果展示了第三階段的進展。公告稱，生產工作仍需要準確的軟體行為模型，以及證明與使用者所依賴的實作之間的明確連結。
在其解釋中，NEAR 區分了涵蓋特定會計規則的證明與保證整個應用程式安全的證明。一份合約可能在轉帳期間維持餘額，同時需要另一份單獨的證明來證明只有授權帳戶才能發起轉帳。
NEAR 共同創辦人 Illia Polosukhin 將該研究與 AI 生成軟體及協助攻擊者識別弱點的工具所帶來的風險連結起來。
「AI 以及 AI 生成程式碼的未來令人振奮——但唯有當我們實現對其行為可驗證且數學上的保證時才行。」
該公告轉載了 Polosukhin 關於軟體安全文章中的陳述。NEAR 表示，形式化驗證應補充測試、程式碼審查與營運安全實務。
111.85 美元的結果衡量的是數學證明
NEAR 的公告報告稱，其 AI 代理解決了 PutnamBench 中的 672 個 Lean 問題，該基準基於 Putnam 大學數學競賽。在提交時所使用的模型價格下，報告的平均成本約為每個問題 0.17 美元。
該專案的公開儲存庫將此結果描述為 670 個上游問題加上兩個形式化有缺陷問題的修正版本。NEAR 表示，報告的支出不包括開發該系統的完整成本，也未估算驗證一份生產合約的價格。
在儲存庫中，團隊報告稱，以後來列出的 DeepSeek 離峰價格重播相同的使用量將花費 331 美元。其方法論包含不成功的嘗試，儘管作者指出了一項使用 Kimi 的獨立平行實驗，他們將其排除在成本核算之外。
該儲存庫描述了對未完成證明的檢查以及對所證明數學陳述的變更。它報告稱，最長的一次運行持續了超過三天。
除了 PutnamBench 之外，NEAR 表示其團隊在 Lean Eval v1 形式化排行榜上以總解題數排名第一。該公告明確說明了這一排名衡量標準，將其與首次解題數和唯一解題數區分開來。
根據 NEAR 的說法，數學基準測試鍛鍊了軟體驗證所需的一項能力，因為開發者需要將軟體需求轉化為數學陳述。該公司將這些結果與證明已部署程式碼屬性的工作區分開來。
形式化證明取決於開發者所選擇的規則
在 NEAR 的轉帳範例中，傳統測試檢查一筆選定的交易，例如在兩個帳戶之間轉移五個代幣。而證明則可以確立：數學模型所涵蓋的每一筆成功轉帳都保持了帳戶的合計餘額。
該公告解釋說，開發者首先選擇一項需求，以數學方式表達相關的軟體行為，然後向檢查器提交一份擬議的證明。由此產生的保證取決於所使用的定義和假設。
NEAR 的方法使用 Lean，這是一種開源程式語言和證明助理。AI 代理可以提出證明、執行 Lean、檢視其回饋並修改嘗試，而 Lean 的核心則檢查該證明是否遵循其邏輯規則。
根據 NEAR 的說法，一次不成功的嘗試並不一定意味著存在軟體缺陷。需求可能是錯誤的，實作可能違反了需求，或者代理可能未能找到有效的證明。
形式化驗證在 NEAR 生態系統內已有記錄在案的應用。Certora 於 3 月 30 日對部署在 NEAR 上的借貸協議 Templar 所作的評估，描述了對其 Rust 合約的手動審查，以及對其市場合約的形式化規範與驗證。Certora 的評估頁面指出，已證明的屬性和發現的問題是完整報告的主題。
其他區塊鏈團隊也在探索 AI 輔助驗證
今年 5 月，Aptos Labs 描述了對 AI 輔助形式化驗證的支援，涉及 Move 合約中的動態分派。根據對該公告的報導，其所述工作流程使用 AI 生成的規範搭配 Move Prover。
以太坊共同創辦人 Vitalik Buterin 曾討論過 AI 工具與機器檢查證明的類似組合。正如 crypto.news 先前報導的那樣，他在 5 月的評論指出了以太坊路線圖中的各項應用，包括共識、抗量子密碼學和零知識系統。
Buterin 告誡說，證明某一層並不能確立整個系統按預期運作。他的討論涵蓋了從高階規範到較低階實作的驗證。
NEAR 另一項獨立的安全研究涉及抗量子簽名。Near One 在 5 月的提案中選擇了FIPS-204 簽名支援，採用美國國家標準與技術研究院核准的 ML-DSA 標準。
該 5 月提案描述了在 2026 年第二季末實現測試網的目標。Near One 表示，錢包軟體、硬體錢包、端點和 API 將需要協調一致的變更，以支援新的簽名方案。
