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 都需要进行协调一致的更改，以支持新的签名方案。
