計算の「正しさ」を数学的に証明する｜ADIC理論とデモ公開（検証可能計算・厳密数値計算・Σ₁証明書）

イントロ：ADICによる検証可能計算—厳密数値計算とΣ₁証明書でcorrectness proofを実装する

GhostDrift数理研究所のマニーです。

私たちは「Ghost Drift」現象の解明に向け、その基盤となる新しい計算エンジンの開発を進めてきました。 本日、その中核となる数理モデル「ADIC (Analytically Derived Interval Computation)」の理論背景と、実際にブラウザ上で動作する技術デモを公開しました。

現代のコンピュータは非常に高速ですが、実はその計算結果の「厳密な正しさ」を保証することは困難です。 ADICは、計算機科学における「構成的解析」という数学的理論を応用し、計算の全プロセスにおいて「間違いがないこと」を証明しながら実行する新しいシステムです。

今回公開したのは以下の2つのリソースです。

理論編：構成的解析に基づく検証系の存在定理 https://ghostdrifttheory.github.io/adic-core-JP/

こちらでは、ADICの数学的な基礎付けについて解説しています。 計算結果が正しいことを示す「証明書（レジャー）」がどのように生成されるのか、そのロジックをまとめています。GhostDrift理論が目指す、無限の精度を有限の世界に落とし込むための理論的支柱です。

実践編：ADIC技術デモと検証レジャー https://ghostdrifttheory.github.io/ghostdrift-adic-demo-JP/

理論だけではイメージしづらい「検証された計算」を体感できるデモです。 通常の電卓モードと、ADICによる検証モードを切り替えて比較できます。 また、あえて計算機にバグを発生させる「カオス注入機能」も搭載しました。通常の計算機なら見過ごしてしまう微細なエラーを、ADICがいかにして検知し、弾くのか。その様子を視覚的にご確認いただけます。

エネルギー制御や金融モデルなど、極限の信頼性が求められる領域において、この「計算保証」という概念は必須となると考えています。

文系・理系の枠を超えた新しい「ゴースト理論」の最前線として、ぜひご覧ください。