Lanyon AI、正式に検証された科学コード向けに1,060万ドルの資金調達ラウンドを公表

Why it matters

Formal verification can make AI-generated scientific software auditable, but its value depends on whether the certified specification captures the engineer's real intent.

Jonathan Gorard, Ammar Hakim, and James "Jimmy" Junoは、Lanyon AIのための1,060万ドルの初期資金調達ラウンドを8月17日に公表し、AI生成の科学ソフトウェアが仕様どおりに機能することを証明させる試みに出資した。

Dimensionが本ラウンドを主導し、Industrious Venturesが参加したと、Lanyon AIの発表は述べている。ニュージャージー州プリンストンの研究ラボである同社は、航空宇宙、推進、原子力、物理シミュレーション、GPU最適化、およびAI推論を対象としており、もっともらしい答えが依然として危険となり得る領域に注力している。

このラウンドは、形式数学と計算プラズマ物理学から集められた創業チームに資本を供給する。GorardはLanyon AIのCEOで、以前はWolfram Researchで自動定理証明と量子計算に取り組み、Stephen Wolframと共にWolfram Physics Projectを共同設立した。HakimはLanyon AIのCTOでプリンストンの講師兼主任研究物理学者であり、その研究は核融合、宇宙プラズマ、トカマク乱流、偏微分方程式の機械学習などを含む。Junoはチーフサイエンティストで、Princeton Plasma Physics Laboratoryの研究者であり、Gkeyllプラズマシミュレーションフレームワークのコア開発者である。

彼らの賭けは、汎用のコーディングエージェントが間違った言語から出発しているという点にある。「なぜエージェントはまだ不完全な人間言語で推論し、コーディングしているのか？」とGorardは8月17日の発表で問いかけた。Lanyon AIは代わりに、数学、物理学、科学計算のために構築された凝縮された形式言語を使ってエージェントに推論させたいと考えている。

コードと証明のための一つの出典

Lanyon AIのアーキテクチャは、創造的作業を基盤となる言語モデルに割り当て、そのモデルがLanyon AIのドメイン固有言語による形式仕様を提案する。シンボリックコンパイラはその仕様を実装コードと機械検証可能な証明に同時に展開する。仕様が証明できない場合、Lanyon AIによればシステムはコードを保留し、再試行するという。

この設計は自動形式化システムの特定の弱点を狙っている。従来のエージェントはコードを書き、その後に別の実装を記述しながら型チェックされるLean証明を生成してしまう可能性がある。Lanyon AIはその失敗を「ミスフォーマライゼーション」と呼ぶ。両方の成果物を一つのソースから導出することは、証明がそれが認証するとされるコードから逸脱するのを防ぐことを意図している。

これまでに入手可能な最も強い証拠はLanyon AI自身から来ている。7月に公開された同社によるベンチマークでは、Junoが線形移流（linear advection）およびマクスウェル方程式ソルバーに関して最先端モデルをテストし、各モデルごとに3回の試行と、詳細なプロンプトと簡潔なプロンプトを用いた。Lanyon AIは、参照となる線形移流ソルバーは生成に約7秒とおよそ800トークンの出力を要し、マクスウェルソルバーは約23秒とおよそ600トークンを要したと報告した。

これらの数値は、8月の発表で行われた最先端モデルとの大雑把な比較よりも狭い主張を支持する。テストは同社のアーキテクチャに合致する科学的問題に関してLanyon AI自身が設計、実行、評価したものである。独立した再現実験は、同アプローチがより広範なエンジニアリング作業群でどのように性能を発揮するかをまだ確立していない。

Lanyon AIはまた、advection-diffusion、マクスウェル方程式、一般相対論的マクスウェル方程式、バーガース方程式、圧縮性オイラー方程式、および静電Vlasov方程式を扱う6つのソルバーリポジトリをGitHubに公開している。これらのリポジトリはCとLeanを使用しており、Lanyon AIの主張の背後にある形式検証作業の検査可能な例を研究者に提供する。

仕様が境界であり続ける

形式検証は実装が形式仕様に準拠していることを確立する。形式検証は、仕様がユーザーの実際の科学的意図、物理的仮定、またはデプロイ条件を捉えているかどうかを自動的に確立することはできない。

GorardはLanyon AIの7月の導入でその境界を認めている。彼は、コード、証明、仕様が一致するという構文的な保証と、ユーザーの自然言語の要求を正しい仕様に翻訳するという意味論的な問題を区別した。Lanyon AIは意味論的な正確さを未解決の研究領域として述べている。

その区別はLanyon AIが追求する産業において重要である。証明はソルバーを認証できても、エンジニアが正しい支配方程式、境界条件、材料特性、あるいは故障閾値を選んだかどうかという問いには答えを残す場合がある。したがってLanyon AIのプロダクト上の課題は、エンジニアと形式言語とのインターフェースに集中している。シンボリックコンパイラは、そのインターフェースが正しい仕様を出力した後になって初めて下流のすべてを監査できる。

市場はすでに技術的に野心的なチームを惹きつけている。Axiomatic AIは検証重視のエンジニアリングAIのために2026年3月に1,800万ドルのシードラウンドを公表し、HarmonicはAristotleシステムを形式数学的推論と検証済みソフトウェアに集中させている。Lanyon AIは実行可能なシミュレーションと数値手法により近い位置を切り開いており、HakimとJunoがプラズマ物理学向けソフトウェアを構築してきた経験を直接活用している。

出資者の顔ぶれも、その産業的方向性を反映している。Dimensionは科学と計算分野への投資をミッションとしていると説明し、Industrious Venturesはソフトウェアの誤りがハードウェアコストや安全要件と衝突する航空宇宙、エネルギー、製造業などの物理産業に注力している。

Lanyon AIはまだ完全に文書化された商業事業というよりは研究プログラムを提示している段階だ。公開資料は価格設定、顧客採用、一般的な製品リリースを確立していない。同社の会社ページでは形式検証、計算物理学、応用数学、AIインフラストラクチャの研究者やエンジニアを募集している。

創業者たちは一貫した技術的命題を提示し、検査可能な部分をつくるに足るコードを公開している。彼らの次の試験は、そのアーキテクチャを、生成されたコードに関する最も難しい誤りを制御仕様に転嫁することなくエンジニアが使えるシステムへと変えることだ。