ImandraX：神经符号人工智能推理和自动逻辑验证的突破

Imandra Inc.，一家革命性的人工智能公司，宣布发布ImandraX，其最新的神经符号人工智能推理进展。这一里程碑式的发布引入了最先进的证明自动化、反例生成和决策程序，设定了人工智能驱动的逻辑分析的新行业标准。

随着人工智能系统越来越多地在金融、国防、医疗保健和自主系统等行业的关键应用中发挥作用，对可信、可解释和数学严谨的推理的需求前所未有。ImandraX通过将强大的自动推理与人工智能代理、验证框架和现实世界的决策模型相结合，推动了人工智能的边界。

Imandra Inc.：人工智能驱动逻辑推理的先驱

Imandra Inc.是一家全球的人工智能公司，专门从事为金融、国防和安全关键行业提供Reasoning-as-a-Service®平台，用于自动逻辑推理。其先进的人工智能解决方案包括Imandra Markets®和Imandra Connectivity®，为关键应用提供严格的形式验证、设计自动化和合规工具。基于自动推理的深度进展，Imandra使企业能够自信地应用逻辑、准确和可审计的人工智能驱动的洞察。
Imandra致力于为世界上最关键的算法带来严谨性和治理。该公司建立了一个云级别的自动推理系统，允许组织利用数学逻辑进行人工智能推理。凭借对开发可信和可解释人工智能的强烈关注，Imandra的技术被全球的研究人员、企业和政府机构所依赖。

提高人工智能推理的标准

Denis Ignatovich，Imandra Inc.的联合创始人和联合首席执行官，表示，“ImandraX是使高级符号推理成为人工智能工作流的核心部分的变革性步骤。通过为人工智能代理提供强大的自动逻辑推理和形式验证能力，我们正在推动智能系统的边界。”
Dr. Grant Passmore，Imandra Inc.的联合创始人，补充说，“ImandraX是多年研究和在一些最苛刻的行业中实际部署的成果，包括金融、国防和人工智能。我们的客户和合作伙伴依赖Imandra的自动推理来确保关键系统的安全性和可靠性，从金融交易所到自主代理。有了ImandraX，我们不仅使严格的推理变得可及，我们还使其成为下一代人工智能驱动的决策的必备条件。”

ImandraX的关键创新

ImandraX引入了几项开创性的功能，包括：

• 证明自动化的突破 – 通过引入混合离散和连续递归函数的新技术，推进了逻辑推理。这种创新使得新IEEE P3109标准的正式模型和验证成为可能，该标准适用于小型（<16位）二进制浮点格式，对神经网络量化和蒸馏至关重要。
• 神经网络安全验证 – 支持首个正式验证的神经网络安全属性验证证明检查器，利用高阶有界模型检查和归纳推理，确保人工智能模型安全地按预期运行。
• 状态空间区域分解 – 为区域分解任务提供了4倍以上的加速，显著提高了金融用户在FIX连接测试和其他关键应用中的效率。
• 开发者体验增强 – 新引入的VS Code插件允许并行证明开发，允许并发作业在Imandra的推理云中运行，并简化了形式验证工作流程。
• 无缝AI集成 – ImandraX无缝集成Imandra的新Python API，允许AI代理框架中的平滑采用，为下一波神经符号人工智能推理代理铺平了道路。

解决人工智能最具挑战性的逻辑问题

Denis Ignatovich表示，“ImandraX建立在大规模工业自动推理应用的基础上。版本X结合了新的推理算法、开创性的架构特性和与代理人工智能的无缝集成，包括Langgraph库。”

神经网络和人工智能驱动的决策模型必须面对一系列挑战，包括可解释性、可验证性和安全性。许多当前的人工智能模型，特别是那些用于深度学习的人工智能模型，作为”黑盒子“运行，使得理解或验证它们的决策过程变得困难。在高风险行业中，如金融、医疗保健和自主系统，这种不透明性带来了重大风险，因为人工智能的决策可能会产生深远的现实世界后果。

对于依赖神经网络的行业来说，确保强壮性和安全性至关重要。 Ignatovich解释说，“神经网络越来越多地被用于安全关键行业，因此确保它们按预期运行并对嘈杂输入具有鲁棒性至关重要。ImandraX的推理能力和整体形式验证基础设施使其能够验证神经网络属性，同时检查第三方定理证明器生成的证明的正确性。”

为什么这对金融、国防和自主系统至关重要

金融、国防和自主系统等行业在精度、可靠性和合规性方面有着极高的要求。这些领域的监管标准不断演变，需要人工智能驱动的解决方案满足严格的监督要求。未能遵守这些法规可能会导致法律后果、财务损失和安全隐患。

Ignatovich进一步解释说，“这些行业必须遵守严格的监管和安全属性，但它们的复杂性已经远远超过了人类的理解能力。Imandra的证明自动化和状态空间区域分解，结合LLM集成，允许开发人员和工程师深入分析系统行为，确保合规性，并严格测试人工智能驱动的系统。”
在金融市场中，人工智能算法负责实时交易决策、欺诈检测和风险管理。即使是小的差异也可能产生巨大的影响，因此形式验证和自动推理对于维护系统完整性至关重要。同样，在国防领域，自主系统必须在严格的约束下运行，确保人工智能驱动的决策符合任务目标和安全协议。
自主系统，包括自动驾驶汽车和无人机，依赖于必须在不可预测的环境中导航并确保乘客安全和遵守法规的人工智能模型。确保这些人工智能驱动的系统在所有可能的情况下都能可靠地运行，需要传统方法无法提供的严格测试方法。ImandraX通过提供自动逻辑验证来填补这一空白，使得基于场景的彻底测试成为可能，并降低了与人工智能不可预测性相关的风险。

神经符号人工智能和人工智能驱动决策的未来

Ignatovich强调，“我们认为神经符号方法是人工智能演进的下一步。传统的统计模型，例如LLM，缺乏基本的逻辑推理。ImandraX弥补了这一缺陷，提供了分析复杂算法的无与伦比的自动化——这是人工智能今天的主要应用之一。”