NEAR AI稱111美元解開PutnamBench全部672題證明

NEAR AI稱旗下「Lean」證明代理以總計111美元（約15萬韓元）的成本，解開數學形式證明基準測試「PutnamBench」中全部672道Lean 4題目。若這項數據能在相同條件下被覆核，將成為衡量AI代理成本效率的具體案例。

CryptoBriefing報導指出，NEAR AI的Lean代理解完PutnamBench全部題目，成本比競爭系統低250倍。不過評論：這項比較並未完整說明各系統採用的模型、執行預算、搜尋方式與重試機制是否統一在相同條件下比較，因此數字本身仍需謹慎看待。

目前可確認的核心事實，是NEAR AI提出「672題全數解出、總花費111美元」的主張。這項結果尚未被PutnamBench官方公開排行榜獨立收錄反映。

PutnamBench官方資料庫顯示，Lean 4版本的題目總數為672題。這項基準測試將美國與加拿大大學數學競賽「普特南（Putnam）」的題目轉換為Lean 4、Isabelle、Coq等形式語言，用來評估AI的自動定理證明能力。

形式證明的重點不只是AI答對與否，而是能否產出機器可驗證的證明過程。官方資料庫也提醒，不應把公開的證明程式碼直接當作驗證證據使用，這說明覆現流程與驗證方式與結果數字同樣重要。

NEAR AI此次主張之所以在NEAR Protocol（NEAR）生態系中具有意義，是因為NEAR AI長期把「可驗證AI」作為核心定位。NEAR官方AI頁面說明，使用者自有AI、信任執行環境（TEE）與即時驗證是其架構核心。

信任執行環境是一種在隔離硬體環境中處理資料、限制外部存取的技術。當這項技術與區塊鏈結合時，AI推論過程、支付與代理執行能被驗證到什麼程度，就成為關注焦點。

NEAR AI今年2月曾公布IronClaw、機密GPU市集（Confidential GPU Marketplace）與多模態機密推論等技術，強調打造能讓代理進行運算、交易與協作的基礎設施。這次PutnamBench的主張，等於為這套技術敘事再加上一組成本效率數字。

本社先前曾報導NEAR AI將NEAR質押與AI運算使用權綁定的架構，當時重點在於AI服務付費與隱私功能、而非一般質押收益；這次的主張則延續同一脈絡，強調可驗證AI基礎設施的效能成本。

形式證明領域的競爭其實早已展開。米斯特拉爾AI（Mistral AI）在7月2日的官方公告中表示，其模型Leanstral 1.5在PutnamBench達成587/672的成績。

米斯特拉爾AI同一份公告提到，每題成本約4美元（約5,400韓元）。另一家公司Logical Intelligence則表示，其Aleph Prover截至1月6日在PutnamBench解出668/672題，平均每解出一題成本約68美元（約9萬1800韓元）。

單就數字對比而言，NEAR AI總花費111美元的主張確實顯眼。評論：但各系統在模型架構、搜尋方式、執行預算與重試條件上並不相同，這類成本比較很難直接拿來判定技術優劣。

PutnamBench排行榜方面也表示，正在討論如何更完整地顯示各種方法所使用的運算預算。成本效率的評估，恐怕要等官方排行榜與各家研究說明採用同一套標準整理後，才會更加清楚。

NEAR AI這項成果會對NEAR Protocol（NEAR）價格或生態系需求帶來什麼影響，已超出目前可確認的報導範圍。眼下的焦點並非價格走勢，而是這套「可驗證AI」基礎設施在實際基準測試中展現出多少成本效率，以及這項結果能否被獨立覆現。