Denis Ignatovich, medeoprichter en mede-CEO van Imandra – Interviewreeks

Denis Ignatovich, medeoprichter en mede-CEO van Imandra, heeft meer dan een decennium ervaring in handel, risicobeheer, kwantitatief modeleren en complexe handelssysteemontwerp. Voordat hij Imandra oprichtte, leidde hij de centrale risicohandelsafdeling van Deutsche Bank (DB ) London, waar hij de cruciale rol van AI in de financiële sector onderkende. Zijn inzichten tijdens deze periode hielpen bij het vormgeven van Imandra’s suite van financiële producten. Denis’ bijdragen aan computationele logica voor financiële handelsplatforms omvatten meerdere octrooien. Hij heeft een MSc in Finance van de London School of Economics en diploma’s in Computer Science en Finance van UT Austin.

Imandra is een AI-gebaseerd redeneerengine die neurosymbolische AI gebruikt om de verificatie en optimalisatie van complexe algoritmen te automatiseren, met name in financiële handel en software-systemen. Door symbolische redenering te combineren met machine learning, verbetert het de veiligheid, naleving en efficiëntie, waardoor instellingen risico’s kunnen verminderen en transparantie kunnen verbeteren in AI-gedreven besluitvorming.

Wat inspireerde u en Dr. Grant Passmore om Imandra mede op te richten, en hoe hebben jullie achtergronden de visie voor het bedrijf beïnvloed?

Na mijn studie ging ik in de kwantitatieve handel en belandde ik in Londen. Grant deed zijn PhD in Edinburgh en verhuisde vervolgens naar Cambridge om te werken aan toepassingen van geautomatiseerde logische redenering voor de analyse van de veiligheid van autopilotsystemen (complex algoritmen die niet-lineaire berekeningen omvatten). In mijn werk had ik ook te maken met complexe algoritmen met veel niet-lineaire berekeningen en we realiseerden ons dat er een diepe verbinding bestond tussen die twee gebieden. De manier waarop de financiële sector dergelijke algoritmen creëerde, was echt problematisch (zoals veel nieuwsverhalen over “algo-glitches” laten zien), dus we wilden dat veranderen door ingenieurs in de financiële sector te voorzien van geautomatiseerde logische tools om strikte wetenschappelijke technieken toe te passen bij de ontwikkeling van software. Maar wat we uiteindelijk creëerden, is branche-onafhankelijk.

Kunt u uitleggen wat neurosymbolische AI is en hoe het verschilt van traditionele AI-benaderingen?

Het gebied van AI heeft (zeer ongeveer!) twee gebieden: statistisch (waaronder LLM’s) en symbolisch (ook wel geautomatiseerde redenering). Statistische AI is geweldig in het identificeren van patronen en vertalen met behulp van de informatie die het heeft geleerd van de data waarop het is getraind. Maar het is slecht in logische redenering. Symbolische AI is bijna het exacte tegenovergestelde – het dwingt u om heel precies (wiskundig) te zijn over wat u probeert te doen, maar het kan logica gebruiken om op een manier te redeneren die (1) logisch consistent is en (2) geen trainingsdata nodig heeft. De technieken die deze twee gebieden van AI combineren, worden “neurosymbolisch” genoemd. Een beroemde toepassing van deze benadering is het AlphaFold-project van DeepMind, dat onlangs de Nobelprijs won.

Wat denkt u dat Imandra onderscheidt in de leiding van de neurosymbolische AI-revolutie?

Er zijn veel geweldige symbolische redeneraars (meestal in de academische wereld) die specifieke niches aanpakken (bijv. eiwitvouwing), maar Imandra voorziet ontwikkelaars van de mogelijkheid om algoritmen te analyseren met ongekende automatisering, wat veel bredere toepassingen en een groter doelpubliek heeft dan die tools.

Hoe elimineert Imandra’s geautomatiseerde redenering veelvoorkomende AI-uitdagingen, zoals hallucinaties, en verbetert het het vertrouwen in AI-systemen?

Met onze benadering worden LLM’s gebruikt om menselijke verzoeken te vertalen naar formele logica, die vervolgens wordt geanalyseerd door de redeneerengine met een volledige logische audittrail. Terwijl vertaalfouten kunnen optreden bij het gebruik van de LLM, wordt de gebruiker een logische verklaring gegeven van hoe de invoer is vertaald en kunnen de logische audits worden geverifieerd door derden met open-source software. Ons uiteindelijke doel is om actiegerichte transparantie te bieden, waarbij AI-systemen hun redenering kunnen verklaren op een manier die onafhankelijk logisch verifieerbaar is.

Imandra wordt gebruikt door Goldman Sachs (GS ) en DARPA, onder anderen. Kunt u een echt voorbeeld geven van hoe uw technologie een complex probleem heeft opgelost?

Een geweldig voorbeeld van de reële impact van Imandra is te zien in onze UBS Future of Finance-wedstrijd, waar we de eerste prijs wonnen (de details met Imandra-code zijn op onze website te vinden). Terwijl we een casestudy voor UBS maakten die een reglementaire document codificeerde dat ze bij de SEC hadden ingediend, ontdekte Imandra een fundamentele en subtiele fout in de algoritmebeschrijving. De fout kwam voort uit subtiele logische voorwaarden die moesten worden vervuld om bestellingen in een bestelboek te rangschikken – iets wat voor mensen onmogelijk was om “met de hand” te detecteren. De bank beloonde ons met de eerste prijs (uit meer dan 620 bedrijven wereldwijd).

Hoe heeft uw ervaring bij Deutsche Bank de toepassingen van Imandra in financiële systemen gevormd, en wat is de meest impactvolle use case die u tot nu toe heeft gezien?

Bij Deutsche Bank hadden we te maken met veel complexe code die automatische handelsbeslissingen nam op basis van verschillende ML-invoer, risico-indicatoren, enz. Als elke bank moesten we ook voldoen aan talloze regelgevingen. Wat Grant en ik realiseerden, was dat dit, op wiskundig niveau, heel erg leek op het onderzoek dat hij deed naar de veiligheid van autopilotsystemen.

Behalve in de financiële sector, welke branches zien u als having het grootste potentieel om te profiteren van neurosymbolische AI?

We hebben AlphaFold de Nobelprijs zien winnen, dus laten we die zeker meerekenen… Uiteindelijk zullen de meeste toepassingen van AI enorm profiteren van het gebruik van symbolische methoden, maar specifiek werken we aan de volgende agents die we binnenkort zullen uitbrengen: code-analyse (vertalen van broncode naar wiskundige modellen), het creëren van strikte modellen uit Engelstalige specificaties, redeneren over SysML-modellen (taal gebruikt om systemen in veiligheidscritische branches te beschrijven) en automatisering van bedrijfsprocessen.

Imandra’s regio-decompositie is een novum. Kunt u uitleggen hoe het werkt en wat de betekenis ervan is bij het oplossen van complexe problemen?

Een vraag die elke ingenieur zich afvraagt wanneer hij software schrijft, is “wat zijn de randgevallen?”. Wanneer hun taak kwaliteitscontrole is en ze unit tests moeten schrijven of wanneer ze code schrijven en nadenken over of ze de eisen correct hebben geïmplementeerd. Imandra brengt wetenschappelijke rigor om deze vraag te beantwoorden – het behandelt de code als een wiskundig model en analyseert symbolisch alle randgevallen (terwijl het een bewijs produceert over de volledigheid van de dekking). Deze functie is gebaseerd op een wiskundige techniek genaamd ‘Cylindrical Algebraic Decomposition’, die we hebben “opgetild” naar algoritmen in het algemeen. Het heeft talloze uren bespaard voor onze klanten in de financiële sector en kritieke fouten aan het licht gebracht. Nu brengen we deze functie naar ingenieurs overal.

Hoe integreert Imandra met grote taalmodellen, en welke nieuwe mogelijkheden ontgrendelt dit voor generatieve AI?

LLM’s en Imandra werken samen om menselijke invoer (of het nu broncode, Engelstalige tekst, enz. is) te formaliseren, te redeneren en vervolgens de uitvoer te retourneren op een manier die gemakkelijk te begrijpen is. We gebruiken agente-frames (bijv. Langgraph) om dit werk te orkestreren en de ervaring te leveren als een agent die onze klanten rechtstreeks kunnen gebruiken of integreren in hun toepassingen of agents. Deze symbiotische workflow adresseert veel van de uitdagingen van het gebruik van LLM-only AI-hulpmiddelen en breidt hun toepassing uit tot voorheen ongeziene trainingsdata.

Wat is uw langetermijnvisie voor Imandra, en hoe ziet u het transformeren van AI-toepassingen in verschillende branches?

We denken dat neurosymbolische technieken de basis zullen vormen die de weg vrijmaakt voor ons om de belofte van AI te realiseren. Symbolische technieken zijn het ontbrekende ingrediënt voor de meeste industriële toepassingen van AI en we zijn enthousiast om aan de vooravond van dit volgende hoofdstuk van AI te staan.

Bedankt voor het geweldige interview, lezers die meer willen leren, kunnen Imandra bezoeken.