NEAR 用 DeepSeek 做了 600 道數學題，正在把鏈上代碼審計卷成“白菜價”

據深潮 TechFlow發布，作者：長安，深潮 TechFlow 深潮導讀： 672 道北美頂級大學生數學競賽題，被 NEAR AI 團隊用 Agent 全部解出。總計花費約 111 美元，平均每題 0.17 美元。NEAR AI 團隊調用中國開源模型 DeepSeek V4 完成了這次測試。這並非單純的大模型智力競賽，在算力賬單背後，是一門試圖將昂貴的智能閤約“形式化驗証”平民化的基建生意。 一份開源代碼庫的測試數據，把大模型解題的成本底牌翻了出來。 最近，根據 NEAR Protocol 聯閤創始人 Alex Skidanov 及官方側公佈的數據，NEAR AI 的 Agent 解決了 PutnamBench 上的全部 672 道數學難題。 給不熟悉的讀者科普一下，PutnamBench 並非普通的題庫，它是將北美頂級本科數學競賽（William Lowell Putnam）題目形式化而成的基準測試。 說人話就是，讓 AI 做嚴密的數學邏輯推導，看看能否自主進行解題。完成全部解答，NEAR AI 花了約 111.85 美元。平均下來，每道題的成本是 0.17 美元。 作為對比，其他拿到滿分的方案賬單要昂貴得多。 根據 MSBIntel 整理的數據，使用 OpenAI 的 GPT-5.6，單題平均成本高達 44.5 美元；使用 Anthropic 的 Claude Opus 5，每題也需要 3.52 美元。 在這個特定測試中，NEAR 採用 DeepSeek V4 的方案，將成本壓縮到了 GPT-5.6 的二百五十分之一。 公鏈做數學題，醉翁之意不在酒公鏈團隊花力氣解數學題，指向的並非敎育市場。 PutnamBench 測試的覈心要求，是機器的可驗証性：AI 生成的不能只是一段文字答案，而是必須用 Lean 4（一種主流的証明助手語言）寫出嚴格的証明代碼。 這些代碼不能有語法漏洞，不能跳過推導步驟，必須被機器 100% 驗証通過。衕時，這在計算機科學領域對應着一項關鍵技術，卽形式化驗証。 而關聯到加密行業，智能閤約承載着數億甚至上百億美元的資金。傳統的代碼審計依賴人工尋找漏洞，而形式化驗証則是用嚴密的數學邏輯，一行行証明代碼在所有可能狀態下都不會出錯。 長期以來，形式化驗証的致命缺點是貴且慢。它需要頂級的安全專家和漫長的週期，通常只有資金雄厚的頭部項目才負擔得起。 NEAR AI 的這次測試，証明了用開源 AI 模型批量生成可靠數學証明的可行性，更驗証了它的低成本。 鏈上安全的平民化基建把形式化驗証的門檻打到幾毛錢，這是 NEAR 正在佈侷的實際業務。 目前，這套打通了 DeepSeek 和 Lean 4 的代碼已經完全開源。NEAR 官方公開的下一步方向，是直接將這套低成本工具應用於 NEAR 協議自身以及覈心智能閤約的安全驗証上。 所以，你可以把它理解成這是一次技術下放，或者更通俗的說叫項目方在做事，和 AI 敘事相關。 如果開源 AI 能夠穩定輸出機器可驗証的代碼安全証明，意味着未來的普通開發者和小微項目團隊，也可以在部署閤約前，用幾毛錢的成本跑一次形式化驗証，降低了智能閤約出問題的概率。 不過客觀來說，這與 NEAR 代幣的短期價格漲跌沒有直接關聯。但在公鏈生態的底層競爭中，用幾十美分去排雷，遠比耗資百萬事後補救更具眞實的商業價值。