Denis Ignatovich，Imandra联合创始人兼联合首席执行官 – 采访系列

Denis Ignatovich，Imandra联合创始人兼联合首席执行官，拥有超过十年的交易、风险管理、量化建模和复杂交易系统设计经验。在创立Imandra之前，他曾领导德意志银行伦敦的中央风险交易台，并在此期间认识到人工智能在金融领域的重要作用。他的见解在此期间帮助塑造了Imandra的金融产品系列。Denis在金融交易平台的计算逻辑方面的贡献包括多项专利。他拥有伦敦经济学院的金融硕士学位和德克萨斯大学奥斯汀分校的计算机科学和金融学位。

Imandra是一种人工智能推理引擎，使用神经符号人工智能来自动化复杂算法的验证和优化，特别是在金融交易和软件系统中。通过将符号推理与机器学习相结合，它提高了安全性、合规性和效率，帮助机构减少风险并提高人工智能驱动决策的透明度。

是什么启发你和Grant Passmore共同创立Imandra，你们的背景如何影响了公司的愿景?

大学毕业后，我进入了量化交易领域，最后来到了伦敦。Grant在爱丁堡完成了他的博士学位，然后搬到剑桥，研究自动逻辑推理在autopilot系统安全分析中的应用（涉及非线性计算的复杂算法）。在我的工作中，我也处理过很多复杂算法，具有大量非线性计算，我们意识到这两个领域之间存在深刻的联系。金融领域创建这些算法的方式确实存在问题（如许多新闻报道中所讨论的“算法故障”），因此我们出发去改变这一点，通过为金融领域的工程师提供自动逻辑工具，引入严格的科学技术来设计和开发软件。然而，我们最终创建的东西却是行业中立的。

你能解释什么是神经符号人工智能，以及它与传统的人工智能方法有什么不同?

人工智能领域大致分为两个领域：统计学（包括LLM）和符号学（也称为自动推理）。统计人工智能非常擅长识别模式和使用从训练数据中学习的信息进行翻译。但是，它在逻辑推理方面很差。符号人工智能则相反，它迫使你在尝试做的事情上非常精确（数学上），但它可以使用逻辑来推理，这种推理是（1）逻辑一致的和（2）不需要训练数据。将这两个人工智能领域结合起来的技术称为“神经符号”。一个著名的应用是DeepMind的AlphaFold项目，最近获得了诺贝尔奖。

你认为是什么让Imandra在领导神经符号人工智能革命方面脱颖而出?

有很多令人难以置信的符号推理工具（大多数在学术界），它们针对特定的领域（例如蛋白质折叠），但Imandra使开发人员能够分析算法具有前所未有的自动化，这比那些工具具有更广泛的应用和更大的目标受众。

Imandra的自动推理如何消除常见的人工智能挑战，例如幻觉，并提高人工智能系统的可信度?

使用我们的方法，LLM将人类的请求翻译成正式逻辑，然后由推理引擎分析，提供完整的逻辑审计。虽然使用LLM可能会出现翻译错误，但用户会得到一个关于如何翻译输入以及逻辑审计可以由第三方开源软件验证的逻辑解释。我们的最终目标是提供可行的透明度，使人工智能系统能够以独立逻辑可验证的方式解释其推理。

Imandra被高盛和DARPA等公司使用。您能分享一个Imandra技术解决复杂问题的真实例子吗?

Imandra技术的真实世界影响的一个很好的公开例子是我们在UBS未来金融挑战赛中获得第一名（详细信息和Imandra代码在我们的网站上）。在为UBS创建一个案例研究时，编码了他们提交给SEC的监管文件，Imandra发现了算法描述中的一个基本且微妙的缺陷。该缺陷源于需要满足的微妙逻辑条件，以便在订单簿中对订单进行排名——这是人类无法“手动”检测到的东西。该银行授予我们第一名（超过620家全球公司）。

您在德意志银行的经验如何影响Imandra在金融系统中的应用，您看到的最有影响力的用例是什么?

在德意志银行，我们处理了大量复杂的代码，这些代码基于各种机器学习输入、风险指标等做出自动交易决策。作为任何银行一样，我们还必须遵守许多法规。Grant和我意识到，这从数学角度来说与他为autopilot安全研究的内容非常相似。

除了金融以外，您认为哪些行业有最大的潜力从神经符号人工智能中受益?

我们已经看到AlphaFold获得诺贝尔奖，所以让我们肯定会计算这个…… 最终，大多数人工智能的应用都将通过使用符号方法而受益，但我们正在研究以下即将发布的代理：代码分析（将源代码转换为数学模型）、从英语说明创建严格模型、对SysML模型进行推理（用于安全关键行业的语言）和业务流程自动化。

Imandra的区域分解是一个新特性。您能解释它如何工作以及在解决复杂问题中的意义吗?

每个工程师在编写软件时都会思考的一个问题是“什么是边缘情况？”当他们的工作是QA，需要编写单元测试用例，或者他们正在编写代码，思考是否正确实现了要求。Imandra为这个问题带来了科学严谨性——它将代码视为数学模型，并对其所有边缘情况进行符号分析（同时生成关于覆盖范围完整性的证明）。该功能基于一种称为“圆柱代数分解”的数学技术，我们将其“提升”到更大的算法。它为我们的金融客户节省了无数时间，并揭示了关键错误。现在，我们正在将此功能带给所有工程师。

Imandra如何与大型语言模型集成，并且这为生成人工智能解锁了哪些新功能?

LLM和Imandra共同工作，将人类输入（无论是源代码、英语说明等）形式化，推理并以易于理解的方式返回输出。我们使用代理框架（例如Langgraph）来编排此工作，并以客户可以直接使用或集成到其应用程序或代理中的代理形式交付。这种协同工作流程解决了使用仅LLM人工智能工具的许多挑战，并将其应用扩展到以前看到的训练数据之外。

您对Imandra的长期愿景是什么，您如何看待它在各个行业中转变人工智能应用?

我们认为神经符号技术将成为实现人工智能承诺的基础。符号技术是大多数人工智能工业应用中缺失的成分，我们很高兴能够站在这一新的人工智能篇章的前沿。

感谢这次精彩的采访，希望了解更多的读者可以访问Imandra。