Denis Ignatovich, Co-founder and Co-CEO of Imandra, has over a decade of experience in trading, risk management, quantitative modeling, and complex trading system design. Before founding Imandra, he led the central risk trading desk at Deutsche Bank London, where he recognized the critical role AI can play in the financial sector. His insights during this time helped shape Imandra’s suite of financial products. Denis’ contributions to computational logic for financial trading platforms include several patents. He holds an MSc in Finance from the London School of Economics and degrees in Computer Science and Finance from UT Austin.
Imandra is an AI-powered reasoning engine that uses neurosymbolic AI to automate the verification and optimization of complex algorithms, particularly in financial trading and software systems. By combining symbolic reasoning with machine learning, it enhances safety, compliance, and efficiency, helping institutions reduce risk and improve transparency in AI-driven decision-making.
What inspired you and Dr. Grant Passmore to co-found Imandra, and how did your backgrounds influence the vision for the company?
After college I went into quantitative trading and ended up in London. Grant did his PhD in Edinburgh and then moved to Cambridge to work on applications of automated logical reasoning for analysis of safety of autopilot systems (complex algorithms which involve nonlinear computation). In my work, I also dealt with complex algorithms with lots of nonlinear computation and we realized that there’s a deep connection between those two fields. The way that finance was creating such algorithms was really problematic (as highlighted by many news stories dealing with “algo glitches”), so we set out to change that by empowering engineers in finance with automated logical tools to bring rigorous scientific techniques to the software design and development. However, what we ended up creating is industry-agnostic.
Can you explain what neurosymbolic AI is and how it differs from traditional AI approaches?
The field of AI has (very roughly!) two areas: statistical (which includes LLMs) and symbolic (aka automated reasoning). Statistical AI is incredible at identifying patterns and doing translation using information it learned from the data it was trained on. But, it is bad at logical reasoning. The symbolic AI is almost the exact opposite – it forces you to be very precise (mathematically) with what you’re trying to do, but it can use logic to reason in a way that is (1) logically consistent and (2) doesn’t require data for training. The techniques combining these two areas of AI are called “neurosymbolic”. One famous application of this approach is the AlphaFold project from DeepMind which recently won the Nobel prize.
What do you think sets Imandra apart in leading the neurosymbolic AI revolution?
There are many incredible symbolic reasoners out there (most in academia) that target specific niches (e.g. protein folding), but Imandra empowers developers to analyze algorithms with unprecedented automation which has much greater applications and greater target audiences than those tools.
How does Imandra’s automated reasoning eliminate common AI challenges, such as hallucinations, and improve trust in AI systems?
With our approach, LLMs are used to translate humans’ requests into formal logic which is then analyzed by the reasoning engine with full logical audit trail. While translation errors may occur when using the LLM, the user is provided with a logical explanation of how the inputs were translated and the logical audits may be verified by 3rd party open source software. Our ultimate goal is to bring actionable transparency, where the AI systems can explain their reasoning in a way that’s independently logically verifiable.
Imandra is used by Goldman Sachs and DARPA, among others. Can you share a real-world example of how your technology solved a complex problem?
A great public example of the real world impact of Imandra is highlighted in our UBS Future of Finance competition 1st place win (the details with Imandra code is on our website). While creating a case study for UBS that encoded a regulatory document that they submitted to the SEC, Imandra identified a fundamental and subtle flaw in the algorithm description. The flaw stemmed from subtle logical conditions that have to be met to rank orders inside an order book – something that would be impossible for humans to detect “by hand”. The bank awarded us 1st place (out of more than 620 companies globally).
How has your experience at Deutsche Bank shaped Imandra’s applications in financial systems, and what’s the most impactful use case you’ve seen so far?
At Deutsche Bank we dealt with a lot of very complex code that made automated trading decisions based on various ML inputs, risk indicators, etc. As any bank, we also had to abide by numerous regulations. What Grant and I realized was that this, on a mathematical level, was very similar to the research he was doing for autopilot safety.
Beyond finance, which industries do you see as having the greatest potential to benefit from neurosymbolic 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’s region decomposition is a novel feature. Can you explain how it works and its significance in solving complex problems?
A question that every engineer thinks about when writing software is “what the edge cases?”. When their job is QA and they need to write unit test cases or they’re writing code and thinking about whether they’ve correctly implemented the requirements. Imandra brings scientific rigor to answer this question – it treats the code as a mathematical model and symbolically analyzes all of its edge cases (while producing a proof about the completeness of coverage). This feature is based on a mathematical technique called ‘Cylindrical Algebraic Decomposition’, which we’ve “lifted” to algorithms at large. It has saved countless hours for our customers in finance and uncovered critical errors. Now we’re bringing this feature to engineers everywhere.
How does Imandra integrate with large language models, and what new capabilities does this unlock for generative AI?
LLMs and Imandra work together to formalize human input (whether it’s source code, English prose, etc), reason about it and then return the output in a way that’s easy to understand. We use agentic frameworks (e.g. Langgraph) to orchestrate this work and deliver the experience as an agent that our customers can use directly, or integrate into their applications or agents. This symbiotic workflow addresses many of the challenges of using LLM-only AI tools and extends their application beyond previously seen training data.
What is your long-term vision for Imandra, and how do you see it transforming AI applications across industries?
We think neurosymbolic techniques will be the foundation that paves the way for us to realize the promise of AI. Symbolic techniques are the missing ingredient for most of the industrial applications of AI and we’re excited to be at the forefront of this next chapter of AI.
Thank you for the great interview, readers who wish to learn more should visit Imandra.
Credit: Source link
