Imandra的聯合創始人兼聯合首席執行官Denis Ignatovich在交易，風險管理，定量建模和復雜交易系統設計方面擁有十多年的經驗。在創立Imandra之前，他領導了德意志銀行倫敦的中央風險交易台，在那裡他認識了AI在金融領域中所發揮的關鍵作用。在此期間，他的見解有助於塑造Imandra的金融產品套件。丹尼斯（Denis）對金融交易平台計算邏輯的貢獻包括幾項專利。他擁有倫敦經濟學院的計算機科學與金融學院碩士學位。
Imandra是一種由AI驅動的推理引擎，它使用神經主體AI自動化複雜算法的驗證和優化，尤其是在金融交易和軟件系統中。通過將符號推理與機器學習相結合，可以提高安全性，合規性和效率，從而幫助機構降低風險並提高AI驅動決策的透明度。
是什麼激發了您和Grant Passmore博士與共同創立的Imandra，您的背景如何影響公司的願景？
大學畢業後，我進行了定量交易，最終在倫敦。格蘭特（Grant）在愛丁堡（Edinburgh）攻讀博士學位，然後搬到劍橋（Cambridge）進行自動邏輯推理的應用，以分析自動駕駛儀系統安全性（涉及非線性計算的複雜算法）。在我的工作中，我還處理了許多非線性計算的複雜算法，我們意識到這兩個字段之間存在著深厚的聯繫。金融創建這種算法的方式確實是有問題的（許多有關“算法”的新聞報導強調了），因此我們著手通過使用自動化的邏輯工具來賦予工程師的能力來改變這一問題，以將嚴格的科學技術帶入軟件設計和開發。但是，我們最終創造的是行業不可或缺的。
您能解釋什麼是神經符號AI以及它與傳統AI方法的不同嗎？
AI領域具有兩個領域：統計（包括LLMS）和符號（又稱自動推理）。統計AI在識別模式和進行翻譯的情況下使用從其訓練的數據中學到的信息而令人難以置信。但是，邏輯推理很糟糕。符號AI幾乎完全相反 – 它迫使您非常（數學上）與您要嘗試的工作非常精確，但是它可以使用邏輯來以（1）在邏輯上一致的方式進行推理，並且（2）不需要培訓數據。將AI的這兩個區域結合在一起的技術稱為“神經符號”。這種方法的著名應用是DeepMind的Alphafold項目，該項目最近獲得了諾貝爾獎。
您認為在領導神經符號AI革命的領導時，Imandra脫穎而出？
有許多令人難以置信的符號推理者（在學術界中，大多數）針對特定的生態位（例如蛋白質折疊），但是Imandra使開發人員具有前所未有的自動化分析算法，該算法比這些工具具有更大的應用程序和更大的目標受眾。
Imandra的自動推理如何消除常見的AI挑戰，例如幻覺並改善對AI系統的信任？
通過我們的方法，LLM被用來將人類的要求轉化為正式邏輯，然後通過完整的邏輯審計跟踪進行推理引擎進行分析。儘管使用LLM可能會發生翻譯錯誤，但向用戶提供了對輸入如何翻譯的邏輯說明，並且可以通過第三方開源軟件驗證邏輯審核。我們的最終目標是帶來可行的透明度，在該透明度上，AI系統可以在邏輯上可以獨立驗證的方式來解釋其推理。
伊曼德拉（Imandra）被高盛（Goldman Sachs）和達帕（Darpa）等人使用。您能否分享一個真實的示例，說明您的技術如何解決一個複雜的問題？
在我們的瑞銀未來的Future of Finance競賽第一名中，強調了Imandra的現實世界影響的一個很好的公開典範（使用Imandra代碼的詳細信息在我們的網站上）。在為瑞銀（UB）編碼他們提交給SEC的監管文件的案例研究時，Imandra在算法描述中確定了一個基本和微妙的缺陷。缺陷源於必須滿足的微妙邏輯條件，這些條件必須在訂單書中進行排名，這是人類無法“手動”檢測到的。該銀行授予我們第一名（全球620多家公司中）。
您在德意志銀行的經驗如何塑造了Imandra在金融系統中的應用，而您到目前為止看到的最有影響力的用例是什麼？
在德意志銀行，我們處理了許多非常複雜的代碼，這些代碼基於各種ML投入，風險指標等做出了自動交易決策。作為任何銀行，我們也必須遵守眾多法規。我和我意識到的是，這在數學層面上與他為自動駕駛安全所做的研究非常相似。
除了金融外，您認為哪些行業具有從神經肯定AI中受益最大的潛力？
We’ve seen AlphaFold get the Nobel prize, so let’s definitely count that one… Ultimately, most applications of AI will greatly benefit by use of symbolic methods, but specifically, we’re working on the following agents that we will release soon: code analysis (translating source code into mathematical models), creating rigorous models from English-prose specifications, reasoning about SysML models (language used to describe systems in safety-critical industries) and business process automation.
Imandra的區域分解是一個新穎的特徵。您能解釋一下它的工作原理及其在解決複雜問題方面的意義嗎？
每個工程師在編寫軟件時都會想到的問題是“什麼邊緣情況？”。當他們的工作是質量保證時，他們需要編寫單元測試案例，或者他們編寫代碼並考慮是否正確實施了要求。 Imandra帶來了科學嚴謹的問題來回答這個問題 – 它將代碼視為數學模型，並象徵性地分析其所有邊緣案例（同時產生有關覆蓋範圍完整性的證明）。此功能基於一種稱為“圓柱代數分解”的數學技術，我們已將其“提升”到整個算法。它為我們的客戶節省了無數小時，並發現了關鍵錯誤。現在，我們將此功能帶給各地的工程師。
Imandra如何與大型語言模型集成，以及為生成AI解鎖哪些新功能？
LLM和Imandra共同努力，以正式化人類的輸入（無論是源代碼，英語散文等），關於它的原因，然後以易於理解的方式返回輸出。我們使用代理框架（例如langgraph）來協調這項工作，並作為客戶可以直接使用或集成到其應用程序或代理商中的代理商。這種共生工作流解決了使用僅使用LLM的AI工具的許多挑戰，並將其應用程序擴展到了先前看到的培訓數據之外。
您對Imandra的長期願景是什麼，您如何看待它改變行業的AI應用程序？
我們認為，神經肯定技術將為我們實現AI的承諾鋪平道路。對於AI的大多數工業應用，符號技術是缺少的成分，我們很高興能成為AI下一章的最前沿。
感謝您的出色採訪，希望了解更多的讀者應該訪問Imandra。
