Denis Ignatovich, medgrundare och med-VD för Imandra – Intervjuserie

Denis Ignatovich, medgrundare och med-VD för Imandra, har över ett decennium av erfarenhet inom handel, riskhantering, kvantitativ modellering och design av komplexa handelssystem. Innan han grundade Imandra ledde han centrala riskhandelsbordet på Deutsche Bank (DB ) i London, där han insåg den avgörande roll som AI kan spela i den finansiella sektorn. Hans insikter under denna tid hjälpte till att forma Imandras svit av finansiella produkter. Denis bidrag till beräkningslogik för finansiella handelsplattformar inkluderar flera patent. Han har en masterexamen i finansiell ekonomi från London School of Economics och examina i datavetenskap och finansiell ekonomi från UT Austin.

Imandra är en AI-driven resonemotor som använder neurosymbolisk AI för att automatisera verifikation och optimering av komplexa algoritmer, särskilt inom finansiell handel och programvarusystem. Genom att kombinera symbolisk resonemang med maskinlärning förbättrar det säkerhet, regelefterlevnad och effektivitet, vilket hjälper institutioner att minska risker och förbättra transparensen i AI-drivna beslutsprocesser.

Vad inspirerade dig och Dr. Grant Passmore att grundandet Imandra, och hur påverkade era bakgrunder visionen för företaget?

Efter college gick jag in i kvantitativ handel och hamnade i London. Grant gjorde sin doktorsexamen i Edinburgh och flyttade sedan till Cambridge för att arbeta med tillämpningar av automatisk logisk resonemang för analys av autopilotsäkerhet (komplexa algoritmer som involverar icke-linjär beräkning). I mitt arbete hanterade jag också komplexa algoritmer med mycket icke-linjär beräkning och vi insåg att det fanns en djup koppling mellan de två områdena. Sättet som finansbranschen skapade sådana algoritmer var verkligen problematiskt (som framhölls av många nyhetsartiklar om “algo-glitch”), så vi satte oss för att ändra på det genom att ge ingenjörer i finansbranschen automatiserade logiska verktyg för att införa rigorösa vetenskapliga metoder i programvarudesign och utveckling. Men vad vi slutade skapa var branschagnostiskt.

Kan du förklara vad neurosymbolisk AI är och hur den skiljer sig från traditionella AI-ansatser?

AI-området har (ganska grovt!) två områden: statistisk (som inkluderar LLM) och symbolisk (även kallad automatisk resonemang). Statistisk AI är otroligt bra på att identifiera mönster och göra översättningar med hjälp av informationen den lärde sig från de data den tränades på. Men den är dålig på logiskt resonemang. Den symboliska AI är nästan det exakta motsatsen – den tvingar dig att vara mycket exakt (matematiskt) med vad du försöker göra, men den kan använda logik för att resonera på ett sätt som är (1) logiskt konsekvent och (2) inte kräver data för träning. Teknikerna som kombinerar dessa två områden i AI kallas “neurosymboliska”. Ett berömt tillämpningsområde för denna ansats är AlphaFold-projektet från DeepMind som nyligen vann Nobelpriset.

Vad tror du särskiljer Imandra i att leda den neurosymboliska AI-revolutionen?

Det finns många otroliga symboliska resonatorer där ute (de flesta inom akademin) som riktar sig till specifika nischer (t.ex. proteinveckning), men Imandra ger utvecklare möjlighet att analysera algoritmer med en aldrig tidigare skådad automatisering som har mycket större tillämpningar och större målgrupper än dessa verktyg.

Hur eliminerar Imandras automatiserade resonemang vanliga AI-utmaningar, såsom hallucinationer, och förbättrar förtroendet för AI-system?

Med vår ansats används LLM för att översätta mänskliga förfrågningar till formell logik som sedan analyseras av resonemotorn med fullständig logisk revisionslogg. Medan översättningsfel kan uppstå när man använder LLM, tillhandahålls användaren en logisk förklaring till hur indata översattes och de logiska revisionerna kan verifieras av tredjepartsöppen källkod. Vårt slutgiltiga mål är att ge handlingsbar transparens, där AI-system kan förklara sitt resonemang på ett sätt som är oberoende logiskt verifierbart.

Imandra används av Goldman Sachs (GS ) och DARPA, bland andra. Kan du dela en verklig exempel på hur er teknik löste ett komplext problem?

Ett utmärkt exempel på den verkliga världens påverkan av Imandra är vår UBS Future of Finance-tävling där vi vann första pris (detaljerna med Imandra-kod finns på vår webbplats). Medan vi skapade en fallstudie för UBS som kodade en regulatorisk dokument som de lämnade in till SEC, identifierade Imandra en grundläggande och subtil fel i algoritmbeskrivningen. Felet härstammade från subtila logiska villkor som måste uppfyllas för att rangordna order i en orderbok – något som skulle vara omöjligt för människor att upptäcka “för hand”. Banken tilldelade oss första pris (av över 620 företag globalt).

Hur har din erfarenhet på Deutsche Bank format Imandras tillämpningar i finansiella system, och vad är den mest betydande användningen du sett hittills?

På Deutsche Bank hanterade vi mycket komplex kod som fattade automatiserade handelsbeslut baserat på olika maskinlärningsinmatningar, riskindikatorer etc. Som alla banker var vi också tvungna att följa många regler. Vad Grant och jag insåg var att detta, på en matematisk nivå, var mycket likt den forskning han gjorde för autopilotsäkerhet.

Förutom finans, vilka branscher ser du som har den största potentialen att dra nytta av neurosymbolisk AI?

Vi har sett AlphaFold få Nobelpriset, så låt oss definitivt räkna med det… I slutändan kommer de flesta tillämpningarna av AI att dra stor nytta av symboliska metoder, men specifikt arbetar vi med följande agenter som vi snart kommer att släppa: källkodsanalys (översättning av källkod till matematiska modeller), skapande av rigorösa modeller från engelska specifikationer, resonemang om SysML-modeller (språk som används för att beskriva system i säkerhetskritiska branscher) och automatisering av affärsprocesser.

Imandras regionuppdelning är en ny funktion. Kan du förklara hur den fungerar och dess betydelse för att lösa komplexa problem?

En fråga som varje ingenjör tänker på när de skriver programvara är “Vilka är de extrema fallen?”. När deras jobb är kvalitetssäkring och de behöver skriva testfall eller när de skriver kod och tänker på om de har implementerat kraven korrekt. Imandra tillför vetenskaplig rigor för att besvara denna fråga – den behandlar koden som en matematisk modell och analyserar symboliskt alla dess extrema fall (samtidigt som den producerar ett bevis om fullständig täckning). Denna funktion bygger på en matematisk teknik som kallas “Cylindrical Algebraic Decomposition”, som vi har “lyft” till algoritmer i stort. Den har sparat otaliga timmar för våra kunder inom finans och avslöjat kritiska fel. Nu tar vi denna funktion till ingenjörer överallt.

Hur integrerar Imandra med stora språkmodeller, och vilka nya funktioner låser detta upp för generativ AI?

LLM och Imandra fungerar tillsammans för att formalisera mänsklig inmatning (antingen det är källkod, engelska prosa etc.), resonera om den och sedan returnera utmatningen på ett sätt som är lätt att förstå. Vi använder agenter (t.ex. Langgraph) för att orkestrera detta arbete och leverera upplevelsen som en agent som våra kunder kan använda direkt eller integrera i sina applikationer eller agenter. Denna symbiotiska arbetsflöde hanterar många av de utmaningar som finns med att använda LLM-baserade AI-verktyg och utökar deras tillämpning bortom tidigare sedda träningsdata.

Vad är din långsiktiga vision för Imandra, och hur ser du att det kommer att förändra AI-tillämpningar över branscher?

Vi tror att neurosymboliska tekniker kommer att vara grunden som banar väg för att vi ska kunna förverkliga löftet om AI. Symboliska tekniker är den saknade ingrediensen för de flesta industriella tillämpningarna av AI och vi är glada över att vara i framkanten av detta nästa kapitel i AI.

Tack för den underbara intervjun, läsare som vill lära sig mer bör besöka Imandra.