Lanyon AIが物理コードの正当性を実証させるための1,060万ドルの資金調達ラウンドを公表

Why it matters

Lanyon AI is betting that scientific AI will be sold on verifiability rather than fluency. The hard part is proving that a formal specification reflects what an engineer intended.

Jonathan Gorard (@getjonwithit)、以前 Wolfram Research と Princeton に在籍した応用数学者は、AI生成コードへのより限定的なアプローチを取っている: ソフトウェアに、その正式な仕様が示すとおりに動作することを証明させることだ。

Lanyon AI、Gorard が計算物理学者の Ammar Hakim (@minmodammar) と James "Jimmy" Juno (@JunoRavin) と共同で設立した同社は、8月17日のプレスリリース で、7月に初回の$10.6 millionの資金調達を完了し、ステルス状態から表に出てきたと発表した。ラウンドは Dimension が主導し、Industrious Ventures とエンジェル投資家の Siqi Chen が参加したと Lanyon AI の発表は述べている。

Princeton, New Jersey に拠点を置く同研究所は、Lanyon とも呼ばれる AI エージェントを構築しており、科学的シミュレーションコードとそれに付随する数学的証明を生成する。Lanyon AI は当面、航空宇宙、推進、原子力エネルギーなど、表面的にもっともらしい答えでもエンジニアが基礎計算を検証できなければ役に立たない分野を対象にこのシステムを売り込んでいる。

Gorard、Hakim、Juno は Princeton Plasma Physics Laboratory での勤務中に出会ったと Industrious Ventures は同社の投資発表で述べている。彼らの研究は核融合炉やブラックホール周辺のプラズマ環境を扱っていた。Princeton の記録によれば、Gorard は 2024 年に Hakim が率いる多物理シミュレーションフレームワーク Gkeyll に取り組むために同大学の研究ソフトウェアエンジニアリング・グループに参加したとある。

Gorard は University of Cambridge の科学計算の MPhil を取得しており、以前は Cardiff University、Wolfram Research、Wolfram Institute で役職を務めていた。Lanyon AI によれば彼は Stephen Wolfram とともに Wolfram Physics Project の共同設立に貢献したという。Hakim の研究は流体力学、核融合、航空宇宙工学にわたり、Juno は実験室、宇宙、天体プラズマに注力してきた。

その経歴は資金調達の説明より前に始まる。Gorard と Hakim は 2025 年に双曲型偏微分方程式ソルバーのための形式検証パイプラインを発表した。3人はその後 2026 年 2 月に BEACONS を発表した。これは収束性、安定性、保存則といった性質について機械検証可能な保証を伴うニューラルソルバーを生成するためのフレームワークである。

Lanyon は創造性と検証を分離する

Lanyon AI のアーキテクチャは、言語モデルとシンボリックソフトウェアに異なる役割を割り当てる。LLM はドメイン固有の形式言語で仕様を提案する。決定論的なシステムがその仕様を実行可能な C コードと、定理証明言語である Lean の証明へと展開する。証明過程が失敗した場合、Lanyon AI は実装は生成されないと言う。

この区別が重要なのは、言語モデルにコードを書かせ、別途証明を出させると、別の失敗点が生まれるためである。すなわち証明がコードが実装する仕様とは異なる仕様を検証してしまう可能性がある。Lanyon AI のシステムは実装と証明を同じ形式的なソースから導出する。

この設計は、Lanyon AI の最大の主張が示すよりも限定的な保証を支えるものだ。Lanyon AI は7月のローンチ投稿の中で、当初エージェントは数学的にミスを犯すことができないと記述していた。注釈がその主張を限定しており、Lanyon AI は実装が形式仕様と一致することを保証する一方で、仕様がユーザーの自然言語の意図を捉えているかどうかを判断することは未解決の研究課題であるとした。

したがって実務上のリスクは上流に移る。生成されたコードは、エンジニアが実際に望んでいたことを表現していない仕様を忠実に実装する可能性がある。Lanyon AI の技術的な主張は、従来のコーディングエージェントと製品を区別する形式的保証を維持しつつ、その意味的なギャップを縮小することにかかっている。

Lanyon AI は同社の GitHub 組織を通じて、マクスウェル方程式、可圧縮オイラー方程式、移流拡散系、および静電的 Vlasov 方程式の形式的に検証されたソルバーなどのサンプル公開を開始した。リポジトリには確認可能なコードと Lean の証明が含まれるが、Lanyon AI のより広範な性能やコストの比較は依然として Lanyon AI が作成したベンチマークに基づいている。

投資家陣は研究と産業向け販売をカバーする

投資家の顔ぶれは創業者たちの課題に密接に対応している。Dimension は科学とコンピューティングに焦点を当てた研究志向の投資会社であると自称している。Industrious Ventures は航空宇宙、エネルギー、製造、国家安全保障など、Lanyon AI が営業を図る産業分野に幅広く投資している。

Gorard は創業者たちを「学界を出たばかりのオタク気質の理論家3人」と書き、そのため航空宇宙、原子力、防衛の顧客にアクセスする必要があったと述べた。Industrious Ventures はそうした関係を提供する。Dimension は、創業者が形式手法の研究を基に商用製品を開発する間、Lanyon AI が研究ラボとして活動できる余地を与えている。

Chen が最初の資金を提供した。Gorard によれば Chen の投資は、Lanyon AI の最初のオフィス、コンピュータ、および残りの資金調達プロセス中の法務顧問の費用を賄ったという。

$10.6 million は創業者たちに、何年にもわたる研究をプロダクション向けソフトウェアに転換し、高価な物理システムの近くで AI 生成のシミュレーションコードを運用することに同意する買い手を見つけるための時間を与える。Lanyon AI は証明をコードと並行して生成できることを示した。商業上の試金石は、エンジニアが仕様作成プロセスを十分に信頼して出力を使用するかどうかである。