NEAR、112ドルのAI証明生成実行後にプロトコルのセキュリティを目指す

NEARプロトコルは、111.85ドルの提出時モデルコストで672の数学問題を解決したと報告した後、プロトコルとコアスマートコントラクトにAI支援の形式検証を適用する計画を示しました。

概要

• NEARはプロトコルとコアスマートコントラクトにAI支援の形式検証を適用する計画です。
• NEAR AIは、提出時モデルコスト111.85ドルで672のPutnamBench問題を解決したと報告しています。
• 生産検証には、正確なソフトウェアモデル、定義された要件、および展開された実装をカバーする証明が必要です。
• 形式検証は、テストやコードレビューを補完し、保証は指定された特性と仮定に限定されます。

NEARプロトコルは、10月16日の発表で、研究がソフトウェアが定義されたルールに従っていることを証明する際に必要な専門的作業と計算コストを削減することを目指していると述べました。

形式検証は、ソフトウェアが定義されたルールに従っていることを証明します。
私たちの目標は、より多くの開発者にとって手頃な価格にすることです。NEAR AIの自動証明生成の進展は、私たちをより近づけています。
次は、NEARプロトコルとコアスマートコントラクトへの適用です。 https://t.co/MqFxz4B166
--- NEARプロトコル (@NEARProtocol) 2026年10月19日

計画された適用は、ネットワークのプロトコルとコア契約、エコシステム開発者向けのツールを含みます。NEARは、生産検証を目標とし、完了したベンチマーク作業は自動数学証明生成に関するものです。

NEARは証明生成を生産ソフトウェアに移行する計画

NEARの発表によると、研究を実行中のソフトウェアに適用するには3つの段階があります。開発者はプログラムを数学的に表現し、満たすべき特性を定義し、それらの特性が保持されることを示す証明を構築する必要があります。

NEAR AIの最近のベンチマーク結果は、第三段階の進展を示しています。発表によれば、生産作業にはソフトウェアの動作の正確なモデルと、証明とユーザーが依存する実装との明確な関連がまだ必要です。

NEARは、特定の会計ルールをカバーする証明と、全体のアプリケーションが安全であることの保証を区別しています。契約は、転送中に残高を保持することができる一方で、認可されたアカウントのみがそれを開始できるという別の証明が必要です。

NEARの共同創設者であるIllia Polosukhinは、AI生成ソフトウェアからのリスクと、攻撃者が弱点を特定するのを助けるツールに関連付けています。

"AIの未来とAI生成コードは刺激的ですが、その動作の検証可能で数学的な保証を達成した後に限ります。"

発表は、Polosukhinのソフトウェアセキュリティに関する文書からの声明を再現しています。NEARは、形式検証がテスト、コードレビュー、運用セキュリティの実践を補完すべきであると述べています。

111.85ドルの結果は数学的証明を測定

NEARの発表は、AIエージェントがPutnamの学部数学競技に基づくベンチマークであるPutnamBenchから672のLean問題を解決したと報告しています。報告された平均コストは、提出に使用されたモデル価格で問題ごとに約0.17ドルでした。

プロジェクトの公開リポジトリは、結果を670の上流問題と、欠陥のある形式化の2つの問題の修正バージョンとして説明しています。NEARは、報告された支出がシステム開発の全コストを除外しており、生産契約の検証価格を見積もっていないと述べています。

リポジトリでは、同じ使用を後でリストされたDeepSeekのオフピーク価格で再生する場合、331ドルかかると報告しています。その方法論には、成功しなかった試みも含まれていますが、著者はコスト計算から除外したKimiを使用した別の並行実験を特定しています。

リポジトリは、未完成の証明に対するチェックと、証明される数学的声明の変更を説明しています。最も長い実行は3日以上続いたと報告されています。

PutnamBenchと並んで、NEARはそのチームがLean Eval v1正式化リーダーボードで合計解決数において1位に達したと発表しました。この発表では、ランキングの測定基準が明確にされており、最初の解決やユニークな解決とは区別されています。

NEARによると、数学的ベンチマークはソフトウェア検証に必要な能力を行使するものであり、開発者はソフトウェアの要件を数学的な表現に変換します。同社は、これらの結果を展開されたコードの特性を証明する作業とは区別しています。

形式的証明は開発者が選択するルールに依存する

NEARの転送例では、従来のテストが選択されたトランザクション、例えば二つのアカウント間で五つのトークンを移動することをチェックします。証明は、数学モデルによってカバーされたすべての成功した転送がアカウントの合計残高を保持することを確立できます。

発表では、開発者が最初に要件を選択し、関連するソフトウェアの動作を数学的に表現し、チェックに提案された証明を提出することが説明されています。その結果得られる保証は、使用される定義と仮定に依存します。

NEARのアプローチは、オープンソースのプログラミング言語および証明アシスタントであるLeanを使用しています。AIエージェントは証明を提案し、Leanを実行し、そのフィードバックを検査し、試みを修正することができます。一方、Leanのカーネルは証明がその論理ルールに従っているかどうかをチェックします。

NEARによれば、失敗した試みは必ずしもソフトウェアの欠陥を特定するわけではありません。要件が間違っている可能性もあり、実装がそれに違反している可能性もあり、エージェントが有効な証明を見つけられない可能性もあります。

形式的検証はすでにNEARエコシステム内で文書化されたアプリケーションを持っています。Certoraの3月30日のTemplarに関する評価は、NEARに展開された貸付プロトコルのRust契約の手動レビューとその市場契約の形式的仕様および検証を説明しています。Certoraの評価ページは、証明された特性と発見された問題を完全な報告書の主題として特定しています。

他のブロックチェーンチームもAI支援の検証を追求している

5月、Aptos LabsはMove契約における動的ディスパッチを含むAI支援の形式的検証のサポートを説明しました。発表の報道によると、同社のワークフローはAI生成の仕様をMove Proverと共に使用しています。

Ethereumの共同創設者であるVitalik Buterinは、AIツールと機械検査された証明の類似の組み合わせについて議論しました。crypto.newsが以前報じたように、彼の5月のコメントはEthereumのロードマップ全体にわたるアプリケーションを特定し、コンセンサス、量子耐性暗号、ゼロ知識システムを含んでいます。

Buterinは、1つのレイヤーを証明することが全体のシステムが意図した通りに動作することを確立するわけではないと警告しました。彼の議論は、高レベルの仕様から低レベルの実装までの検証をカバーしました。

NEARの別のセキュリティ研究は、量子耐性の署名に取り組んでいます。Near Oneの5月の提案は、米国国立標準技術研究所によって承認されたML-DSA標準を使用してFIPS-204署名サポートを選択しました。

5月の提案では、2026年第2四半期末のテストネット目標が説明されました。Near Oneは、ウォレットソフトウェア、ハードウェアウォレット、エンドポイント、およびAPIが新しい署名スキームをサポートするために調整された変更を必要とすると述べました。