京都大学 特定准教授 三内顕義氏がNyx Foundationに参画 ─ AIエージェントが決済する時代へ

ブロックチェーン決済と検証自動化で「AIエージェント経済」を支える。

一般社団法人 Nyx Foundation（所在地：東京都文京区、以下「Nyx Foundation」）は、このたび京都大学 理学部 学習物理学講座 特定准教授であり、国立情報学研究所 LLMセンター 客員准教授も務める三内顕義氏を、Principal AI Scientistとして迎えたことをお知らせいたします。

Nyx Foundationは、AIエージェントが人間に代わって取引・決済を担う「AIエージェント経済」の到来を見据え、ブロックチェーン決済を含む次世代プロトコルの安全性・信頼性を、形式検証（Lean等）とそのAIによる自動化によって担保する研究開発を推進してまいります。

三内氏の参画により、暗号・ブロックチェーン領域における数理の形式検証、AIエージェントの透明性と健全性の検証、ならびに検証プロセス自体をスケーラブルに自動化するAIエージェントの開発を加速させます。

AIエージェントが決済する時代へ

GoogleのAgent Paymentsプロトコルに代表されるようにAIエージェントが人間に代わって、あるいはAIエージェント同士で自動的に決済を行う未来は、技術進展と社会実装の流れから見ても不可避になりつつあります。

AIエージェントは日常の購買行動の代行にとどまらず、株式・通貨等の取引といった金融領域における意思決定と実行も担うようになることが想定されます。一方で、人間に紐づかない自律型AIエージェントは、クレジットカード等の「人間を前提とした決済手段」を保有できません。

この制約を踏まえると、プログラムによる執行と検証が可能なブロックチェーン上の決済は、AIエージェントにとって重要な代替手段となり得ます。こうした前提のもと形成されていくのが、AIエージェントが経済活動の主体となる「AIエージェント経済」です。

AIエージェント経済の課題

AIエージェント経済が立ち上がる際、重要な課題は大きく二つあります。

第一に、システムのセキュリティです。

すでに現代のデジタル社会でもセキュリティは中心課題ですが、AIエージェントを自動制御し、取引や決済を機械的に実行させる環境では、より一層の堅牢性が求められます。人間の目では見逃されうる脆弱性を、AIが探索・発見し悪用する可能性も否定できないためです。

第二に、AIエージェントの信頼性と透明性の確保です。

自動制御されたAIエージェントの行動を人間が逐一追跡・監督することは現実的ではありません。そのため、エージェントがどのようなルールに従い、どの範囲で何を実行できるのかを「検証可能な形」で示す仕組みが必要になります。こうした技術がなければ、AIエージェントの世界においても、人間社会と同様に契約不履行や詐欺、意図しない逸脱行動が発生し得ます。

これら二つの課題に対する有力なアプローチが、LeanやCoqに代表される形式検証です。形式検証は、数学的な証明に基づいて仕様やプログラムの挙動を検証し、システムの正当性を厳密に担保する方法論です。

例えば、AWSが開発したポリシー言語Cedarでは、Leanによる形式検証を通じてその信頼性を高める取り組みが行われています。また形式検証は、純粋数学や量子情報の分野でも活用が進んでおり、ケプラー予想の証明の形式化、P. Scholze氏らによるLiquid Tensor Experiment、量子一般化シュタインの補題に関する証明など、学術的にも大規模な成果が報告されています。

形式検証を導入することで、システムの数理的性質を含む仕様の整合性や、AIエージェントが生成したプロトコル設計・実装の健全性を、検証可能な形で担保することが可能になります。

そして、AIエージェント経済において特に重要となるのが、この検証プロセス自体をAIによって自動化し、スケールさせることです。AIエージェントは今後、ほぼ無数に立ち上がっていくことが見込まれます。一方で、形式検証は人手で行う場合に膨大な工数を要し、例えばLiquid Tensor Experimentにおいては証明の最後の5行だけで6万行のコードが、それより前に行われたケプラー予想の形式化においては10年という膨大な時間がかかっています。

こうした背景から、検証を人手のみに依存するアプローチでは、将来の規模に対応することが難しくなります。この課題に対し、三内氏が発表した prover agent では、数学の定理証明とその形式化を自動化することに成功しています。本技術は、数学オリンピックで金メダリストを取れる程の性能となっており、そのレベルの問題では一問あたり数十分程度で証明とその形式化を完成させることができます。これは形式検証をスケールさせるための基盤技術となる可能性があります。

Nyx Foundationは、AIエージェントが決済する時代に向けて、こうした技術をさらに発展・応用し、暗号分野における数理の形式検証、ブロックチェーンシステムの検証、AIエージェントの信頼性検証を自動で実行可能な、スケーラブルな検証AIエージェントの開発を推進してまいります。

京都大学 特定准教授 三内顕義氏 略歴

東京大学大学院数理科学研究科で博士号を取得

京都大学数理解析研究所特任助教、理化学研究所AIPセンター研究員/上級研究員を経て

現在京都大学理学部学習物理学講座特定准教授、および国立情報学研究所LLMセンター客員准教授

Nyx Foundationについて

一般社団法人 Nyx Foundation（所在地：東京都文京区）は、イーサリアム・ブロックチェーンに特化した私設の研究機関です。

すべての活動資金は寄付・研究助成金・スポンサーシップによって支えられています。そのような資金を原資にイーサリアムの重要課題を解決するための活動を継続してきました。

既にイーサリアム財団やブロックチェーン企業・大学との連携を進め、コロンビア・ビジネススクール等で成果を発表しています。