ImandraX: ニューロシンボリック AI 理論と自動論理検証のブレークスルー

Imandra Inc.、自動論理推論を革命している AI 会社は、最新のニューロシンボリック AI 理論である ImandraX をリリースしました。このランドマーク リリースでは、プルーフ オートメーション、カウンターエクサンプル生成、デシジョン プロシージャなどの最先端の機能を導入し、AI ドリブンの論理分析の新しい業界標準を設定しました。

AI システムが、金融、防衛、ヘルスケア、自律システムなどの業界でミッション クリティカルなアプリケーションを増やしているため、信頼性が高く、説明可能で、数学的に厳密な推論の需要は今までで最高です。ImandraX は、強力な自動推論を AI エージェント、検証フレームワーク、リアルワールドの意思決定モデルと統合することで、AI の境界を拡大します。

Imandra Inc.: AI ドリブンの論理推論の先駆者

Imandra Inc. は、金融、防衛、セーフティ クリティカルな業界での自動論理推論のための Reasoning-as-a-Service® プラットフォームを先駆的に開発しているグローバル AI 会社です。その先進的な AI パワード ソリューションには、Imandra Markets® および Imandra Connectivity® が含まれ、ミッション クリティカルなアプリケーション向けに厳密な形式検証、設計オートメーション、コンプライアンス ツールを提供します。自動推論の深い進歩に基づいて構築された Imandra は、ビジネスが論理的、正確で、監査可能な AI ドリブンの洞察を自信を持って適用できるようにします。
Imandra は、世界で最も重要なアルゴリズムに厳密性とガバナンスをもたらすことに尽力しています。同社は、クラウドスケールの自動推論システムを構築し、組織が AI 推論のための数学的論理を利用できるようにしました。信頼性が高く 説明可能な AI の開発に強い重点を置く Imandra のテクノロジーは、世界中の研究者、企業、政府機関に頼られています。

AI 理論の水準を高める

Denis Ignatovich、Imandra Inc. の共同創設者兼共同 CEO は、“ImandraX は、先進的なシンボリック理論を AI ワークフローの核心部分にするという変革的なステップです。強力な自動論理推論と形式検証機能を AI エージェントに搭載することで、知能システムが達成できることの境界を拡大しています。”
Dr. Grant Passmore、Imandra Inc. の共同創設者 は、“ImandraX は、最も厳しい業界を含む研究と実世界での展開の数年間の集大成です。金融、防衛、AI を含む。我々の顧客とパートナーは、Imandra の自動推論に依存して、金融取引所から自律エージェントまで、ミッション クリティカルなシステムの安全性と信頼性を確保しています。ImandraX では、厳密な推論を利用可能にしているだけでなく、次世代の AI パワードな意思決定のために不可欠にしているのです。”

ImandraX の主な革新

ImandraX には、以下のような画期的な機能が導入されています：

• プルーフ オートメーションのブレークスルー – 混合離散および連続再帰関数の新しい技術を導入し、データ型上の論理推論を進歩させます。この革新により、ニューラル ネットワークの量子化と蒸留に不可欠な小さな (<16 ビット) バイナリ 浮動小数点形式の新しい IEEE P3109 標準の最初の形式モデルと検証が可能になります。
• ニューラル ネットワークの安全性検証 – ニューラル ネットワークの安全性特性検証の最初の形式検証済みプルーフ チェッカーを提供し、より高いオーダーのバウンド モデル チェッキングと帰納を利用して、AI モデルが安全に、かつ意図したとおりに動作することを保証します。
• ステート スペース リージョン分割 – リージョン分割タスクの効率を 4 倍以上向上させ、FIX 接続テストやその他のミッション クリティカルなアプリケーションでの金融ユーザーにとっての大幅な効率化を実現します。
• 開発者エクスペリエンスの強化 – 新しく導入された VS Code プラグインにより、並列プルーフ開発が可能になり、Imandra の推論クラウドで同時にジョブを実行できるようになり、形式検証ワークフローが簡素化されます。
• シームレスな AI 統合 – ImandraX は、Imandra の新しい Python API とシームレスに統合され、AI エージェント フレームワークへのスムーズな導入が可能になり、次世代のニューロシンボリック AI 理論エージェントの舞台を整えます。

AI の最も厳しい論理的課題に対処する

Denis Ignatovich は、“ImandraX は、大規模な産業応用の自動推論の数年間に基づいて構築されています。バージョン X には、新しい推論アルゴリズム、画期的なアーキテクチャ機能、および Langgraph ライブラリを含むエージェント AI とのシームレスな統合が含まれています。”

ニューラル ネットワークと AI ドリブンの意思決定モデルは、説明可能性、検証可能性、安全性などの課題に直面しています。特に ディープ ラーニング で使用される多くの現在の AI モデルは、”ブラック ボックス” として機能し、意思決定プロセスを理解または検証することが困難です。この不透明性は、金融、ヘルスケア、自律システムなどの高リスク業界では大きなリスクをもたらします。ここでは、AI の決定が現実世界で重大な影響を及ぼす可能性があります。

ニューラル ネットワークに依存する業界では、堅牢性と安全性を確保することが重要です。Ignatovich は、“ニューラル ネットワークは、安全性が重要な業界でますます依存されています。したがって、それらが意図したとおりに動作し、ノイズのある入力に対して堅牢であることを確認することは非常に重要です。ImandraX の数値計算について推論し、全体的な形式検証インフラストラクチャを可能にする機能により、ニューラル ネットワークの特性を検証し、第三者による定理証明器によって生成された証明の正しさも確認できます。”

これが金融、防衛、自律システムにとって重要な理由

金融、防衛、自律システムなどの業界は、精度、信頼性、コンプライアンスが最重要である環境で運営されています。これらの分野の規制基準は不断に進化しており、AI ドリブンのソリューションは厳格な監督要件を満たす必要があります。これらの規制に従わない場合、法的結果、財務損失、安全性の危険につながる可能性があります。

Ignatovich は、“これらの業界は、厳格な規制および安全性特性に従う必要がありますが、その複雑さは人間が完全に理解できる範囲を遥かに超えています。Imandra のプルーフ オートメーションとステート スペース リージョン分割、LLM 統合を組み合わせることで、開発者とエンジニアはシステムの動作を深く分析し、コンプライアンスを確保し、AI ドリブンのシステムを徹底的にテストできます。”
金融市場では、AI アルゴリズムがリアルタイムの取引決定、不正検出、リスク管理に責任を負っています。ささやかな不一致でも大きな影響を及ぼす可能性があるため、形式検証と自動推論はシステムの完全性を維持するために不可欠です。同様に、防衛では、自律システムが厳格な制約の下で動作し、AI ドリブンの決定がミッションの目的と安全性のプロトコルに一致することを保証する必要があります。
自律システム、包括して自律走行車やドローンを含むは、予測不可能な環境をナビゲートしながら、乗客の安全性と規制コンプライアンスを確保する必要がある AI モデルに依存しています。これらの AI ドリブンのシステムがすべての可能な条件下で信頼性を持って動作することを保証するには、従来の方法では提供できない徹底的なテスト手法が必要です。ImandraX は、シナリオベースのテストを可能にする自動論理検証を提供することで、AI の予測不可能性に関連するリスクを軽減します。

ニューロシンボリック AI と AI パワードな意思決定の未来

Ignatovich は、“私たちは、ニューロシンボリックなアプローチが AI の進化の次の大きなステップであると考えています。伝統的な統計モデル、たとえば LLM は、基本的な論理推論が欠けています。ImandraX は、このギャップを埋め、複雑なアルゴリズムの分析のための無与倫比な自動化を提供しています。これは、今日の AI の重要な応用の 1 つです。”