单题 17 美分破局：NEAR 用 DeepSeek 重构代码审计成本

据 Woofun AI 消息， 团队利用中国开源模型 ，成功解出 基准测试中的全部 672 道数学难题，总耗时成本仅为 111.85 美元。

这一结果将单题平均成本压缩至 0.17 美元，相较于使用 OpenAI GPT-5.6 方案所需的 44.5 美元单题成本，实现了高达 250 倍的成本降幅。这并非一次简单的算力展示，而是 试图通过极致的成本优化，将原本昂贵且小众的'形式化验证'技术转化为普惠型基础设施的关键一步。

PutnamBench 并非普通的数学题库，而是基于北美顶级本科数学竞赛 William Lowell Putnam 的题目构建的严苛基准。其核心挑战在于'可验证性'：AI 不能仅输出文字答案，必须使用 这种主流证明助手语言，编写出无语法漏洞、无逻辑跳跃且能被机器 100% 验证通过的严格证明代码。NEAR Protocol 联合创始人 及官方公布的数据显示，NEAR AI 的 Agent 在这一高难度任务中实现了满分通关。作为对比，其他主流大模型在同等测试下的表现则显得昂贵得多：使用 Anthropic 的 Claude Opus 5 方案，单题成本仍需 3.52 美元；而使用 OpenAI 的 GPT-5.6，单题成本更是高达 44.5 美元。

Woofun AI 整理数据显示，NEAR 采用 V4 的方案，不仅完成了全部解答，更将成本压低至 GPT-5.6 的二百五十分之一。这种巨大的成本差异，揭示了开源模型在特定垂直领域（如形式化证明）相对于闭源商业模型的潜在优势。

公链团队投入资源攻克数学难题，其终极目标并非教育市场，而是加密行业最核心的痛点——智能合约安全。在 Web3 世界中，智能合约承载着数亿甚至上百亿美元的资金，传统的人工代码审计依赖专家经验寻找漏洞，效率低且存在盲区。而形式化验证则是利用严密的数学逻辑，一行行证明代码在所有可能状态下均不会出错，从而提供数学意义上的绝对安全保证。

然而，长期以来，形式化验证因需要顶级安全专家介入且周期漫长，导致其成本极高，通常只有资金雄厚的头部项目才能负担得起，形成了'贵且慢'的行业壁垒。NEAR AI 的这次测试，实质上验证了利用开源 AI 模型批量生成可靠数学证明的技术可行性，并证明了其极低的边际成本。

目前，这套打通了 DeepSeek 和 Lean 4 的代码库已完全开源，NEAR 官方明确表示，下一步将直接将该低成本工具应用于 NEAR 协议自身以及核心智能合约的安全验证中。

从产业演进的角度看，这是一次典型的技术下放。如果开源 AI 能够稳定输出机器可验证的代码安全证明，意味着未来的普通开发者和小微项目团队，也可以在部署合约前，以几毛钱的成本跑一次形式化验证，从而大幅降低智能合约出错的概率。

尽管这与 NEAR 代币的短期价格涨跌没有直接关联，但在公链生态的底层竞争中，用几十美分去前置排雷，远比耗资百万进行事后补救更具真实的商业价值。这是继零知识证明普及之后，Web3 安全基础设施向'平民化'迈进的又一标志性事件，预示着智能合约的安全门槛将被彻底重塑。