作者：長安，深潮 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% 驗證通過。同時，這在計算機科學領域對應著一項關鍵技術，即形式化驗證。
而與加密行業相關，智能合約承載著數億甚至上百億美元的資金。傳統的代碼審計依賴人工尋找漏洞，而形式化驗證則是用嚴密的數學邏輯，一行行證明代碼在所有可能狀態下都不會出錯。
長期以來，形式化驗證的致命缺點是昂貴且緩慢。它需要頂級的安全專家和漫長的週期，通常只有資金雄厚的頭部項目才負擔得起。
The test of NEAR AI demonstrates the feasibility of using open-source AI models to generate reliable mathematical proofs in bulk, and also verifies its low cost.
Chain-based security for mass adoption infrastructure
將形式化驗證的門檻降低至幾毛錢，這是 NEAR 正在布局的實際業務。
目前，這套打通 DeepSeek 和 Lean 4 的代碼已經完全開源。NEAR 官方公開的下一步方向，是直接將這套低成本工具應用於 NEAR 協議自身以及核心智能合約的安全驗證上。
因此，你可以將其理解為一次技術下放，或更通俗地說，是項目方在推進與 AI 叙事相關的事務。
如果開源 AI 能夠穩定輸出機器可驗證的代碼安全證明，意味著未來的普通開發者和小微項目團隊，也可以在部署合約前，以幾毛錢的成本運行一次形式化驗證，降低智能合約出問題的機率。
不過客觀來說，這與 NEAR 代幣的短期價格漲跌沒有直接關聯。但在公鏈生態的底層競爭中，用幾十美分去排雷，遠比耗資百萬事後補救更具真實的商業價值。