The Nomura Institute of Glycosciece Blog

野村一也　「科学を学ぶ人のために」　九大野村研ホームページの拡張版です

新しい、科学、工学、物理学用のAI―Lanyon AIが登場しました！

投稿日: 投稿者: root

物理学に使える新しい画期的なAIが登場したそうです。Lanyon AIというものです。宣伝の文章が以下にのっています。このLanyon AIというのはMathematicaで有名なWolframの共同研究者でWolframと「新しい物理学」の研究を進めていた一般相対性理論などの研究者Jonathan Gorard(プリンストン大学）がCEOをつとめる会社が開発したものです。Lanyon AIの登場を告げる宣伝文はこちらから読むことができます。https://lanyon.ai/blog/welcome/　
この宣伝文では、Lanyon AIという新しく開発されたAIが、科学、エンジニアリング、ミッションクリティカルなタスク（航空宇宙や原子力など）に向けた、数学的に証明された「絶対に間違えない」新世代のAIであることが強調されています。

今までのAIとの違いはというと：
今までのAIもコードやその正しさを証明するプログラムを書くことはできましたが、「実装したコード」と「正しさの証明」を別々に生成するため、両者に矛盾が生じるリスク（例：コードは「＋」なのに証明は「－」になっている等のミス）がありました。Lanyon AIは、「構築段階から正しい（Correctness by Construction）」というアプローチをとっています。AIが不完全な人間の言葉でコードを書くのではなく、後述する独自の単一言語（DSL）で「仕様」を書き出し、そこから「コード」と「証明」を同時に自動生成します。もし仕様が厳密に証明できない場合は、そもそもコードが生成されないため、構造的にエラーや矛盾を起こすことが不可能になっています。

Lanyon AIの特徴は100%の構文的正確性です。
生成されるコードとデータは数学的に正しいことが証明されており、文法や仕様と実装の不一致といったミスを犯すことが「数学的に不可能」です。そのため少しの計算ミスも許されない宇宙開発、航空宇宙工学、クリーンエネルギーなどの分野において、信頼できる物理シミュレーションや計算基盤を提供できます。また、圧倒的なスピードと低コストも大きな特徴です。従来の最先端AIモデルと比べて、ほんのわずかな計算コストとトークン数で動作します。AIは数十行の仕様を書くだけでよく、それをシステムが一瞬で数万行のコードや証明に拡張するため、1秒間に数千行の正しい数学的証明を書くほどの超高速処理が可能です。
この宣伝文での Neurosymbolic approach（ニューロシンボリック・アプローチ）というのは、「ニューラルネットワーク（昨今のAI）」と「シンボリックAI（昔からの記号的・論理的AI）」のいいとこ取りをしたハイブリッド方式のことです。これまでのLLM（AI）は、アイデアを出したり文章を作ったりする「創造性」は豊かですが、計算や論理的思考においては嘘（ハルシネーション）をつくことがありました。一方、昔ながらのプログラム（シンボリック）は「創造性」はゼロですが、決められた計算や論理ルールは「絶対に間違えない」という特徴があります。Lanyonはこの両方を組み合わせ、「AI（LLM）がクリエイティブにアイデアや仕様を提案し、それをルールベースのアルゴリズム（シンボリック）が厳格に計算・証明して形にする」という仕組みを実現しています。LEANやRocq, Agdaなどという証明支援システムを利用してチェックするようです。

また、この宣伝文にあるDomain Specific Language (DSL：ドメイン特化言語)というのは、何でもできる汎用的なプログラミング言語（PythonやC++など）ではなく、「特定の分野（ドメイン）の目的を達成するためだけに作られた専用の言語」のことです。Lanyon AIは、数学や物理学を記述するためだけに特化した独自の言語（DSL）を持っています。この言語は非常に洗練され、情報が凝縮されているため、AIはこのDSLを使ってたった「数十行」の短い指示（仕様）を書くだけで済みます。汎用言語でダラダラと長いコードを書く必要がないため、AIが処理を間違える隙がなくなり、結果として超高速かつ低コストな処理が可能になっています。注意点としては、宣伝文の注釈にもある通り、Lanyon AIが保証しているのは「仕様と実装が100%一致する（構文的な正確性）」という点であり、「人間の曖昧な意図を完璧に汲み取れるか（意味的な正確性）」については現在も研究中とのことです。

こちらのGitHubには６つほど、Lanyon AIの応用例がのっています。
https://github.com/lanyonai

たとえば以下のツイートをご覧ください。
オイラー方程式の研究例ですが、「人間なら数ヶ月から数年かかるであろう『完璧に証明されたプログラムと数学的証明』の構築を、たった3分弱で終わらせたそうです。
1次元（1D）、2次元（2D）、3次元（3D）の空間における「等温オイラー方程式」と「完全な圧縮性オイラー方程式」を解くプログラムを、すべて合わせて約179秒で生成しました。1つの条件につき、わずか13秒〜54秒しかかかっていません。また単に動くコードを書いただけではなく、そのコードが物理法則に対して「絶対に間違っていない」ことを証明するためのコード（Lean 4という定理証明言語）を10,750行も生成しました。これには270の定義と156の定理が含まれています。さらに証明だけでなく、実際にシミュレーションを動かすためのC言語のコードを6,876行生成しました。このC言語コードは上記のLean 4によって「端から端まで正しさが証明（End-to-end formally verified）」されているものです。
つまり、「超高速・大ボリューム・バグ率0%」という、従来のプログラミングやAIでは到底不可能な離れ業をやってのけたという例のようです。