Denis Ignatovich, Co-Founder und Co-CEO von Imanda – Interview-Serie

Denis Ignatovich, Co-Founder und Co-CEO von Imandra, verfügt über mehr als ein Jahrzehnt Erfahrung in den Bereichen Handel, Risikomanagement, quantitatives Modellieren und komplexes Handelssystemdesign. Bevor er Imandra gründete, leitete er den zentralen Risikohandelsdesk bei Deutsche Bank London, wo er die kritische Rolle erkannte, die künstliche Intelligenz (KI) im Finanzsektor spielen kann. Seine Erkenntnisse während dieser Zeit halfen dabei, Imandras Suite von Finanzprodukten zu gestalten. Denis’ Beiträge zur computergestützten Logik für Finanzhandelsplattformen umfassen mehrere Patente. Er hält einen MSc in Finanzen von der London School of Economics und Abschlüsse in Informatik und Finanzen von der UT Austin.

Imandra ist ein KI-gestützter Reasoning-Engine, der Neurosymbolik-KI verwendet, um die Verifizierung und Optimierung komplexer Algorithmen, insbesondere im Finanzhandel und in Softwaresystemen, zu automatisieren. Durch die Kombination symbolischer Reasoning-Methoden mit Machine Learning verbessert es die Sicherheit, die Einhaltung von Vorschriften und die Effizienz und hilft Institutionen dabei, Risiken zu reduzieren und die Transparenz bei KI-gestützten Entscheidungsprozessen zu verbessern.

Was hat Sie und Dr. Grant Passmore dazu inspiriert, Imandra zu gründen, und wie haben Ihre Hintergründe die Vision für das Unternehmen beeinflusst?

Nach dem College ging ich in den quantitativen Handel und landete in London. Grant hat seinen PhD in Edinburgh gemacht und dann in Cambridge gearbeitet, um Anwendungen der automatischen logischen Reasoning für die Analyse der Sicherheit von Autopilot-Systemen (komplexe Algorithmen, die nichtlineare Berechnungen beinhalten) zu entwickeln. In meiner Arbeit habe ich auch mit komplexen Algorithmen mit vielen nichtlinearen Berechnungen zu tun gehabt, und wir haben festgestellt, dass es eine tiefe Verbindung zwischen diesen beiden Bereichen gibt. Die Art und Weise, wie die Finanzbranche diese Algorithmen erstellte, war wirklich problematisch (wie in vielen Nachrichtenartikeln über “Algo-Glitches” hervorgehoben), also haben wir uns entschieden, dies zu ändern, indem wir Ingenieure im Finanzsektor mit automatischen logischen Werkzeugen ausstatten, um strenge wissenschaftliche Methoden für die Softwaredesign- und -entwicklung zu verwenden. Allerdings haben wir letztendlich etwas Branchen-agnostisches geschaffen.

Können Sie erklären, was Neurosymbolik-KI ist und wie sie sich von herkömmlichen KI-Ansätzen unterscheidet?

Das Feld der KI hat (sehr grob!) zwei Bereiche: statistisch (das umfasst LLMs) und symbolisch (auch automatisierte Reasoning genannt). Statistische KI ist unglaublich gut darin, Muster zu erkennen und Übersetzungen mithilfe der Informationen durchzuführen, die sie aus den Trainingsdaten gelernt hat. Aber sie ist schlecht darin, logische Reasoning durchzuführen. Die symbolische KI ist fast das genaue Gegenteil – sie zwingt Sie dazu, sehr präzise (mathematisch) zu sein, was Sie tun möchten, aber sie kann Logik verwenden, um auf eine Weise zu argumentieren, die (1) logisch konsistent und (2) keine Trainingsdaten erfordert. Die Techniken, die diese beiden KI-Bereiche kombinieren, werden als “Neurosymbolik” bezeichnet. Ein berühmtes Anwendungsbeispiel für diesen Ansatz ist das AlphaFold-Projekt von DeepMind, das kürzlich den Nobelpreis gewonnen hat.

Was unterscheidet Imandra Ihrer Meinung nach von anderen Anbietern und führt die Neurosymbolik-KI-Revolution an?

Es gibt viele unglaubliche symbolische Reasoner (meist in der Akademie), die sich auf bestimmte Nischen (z. B. Proteinfaltung) konzentrieren, aber Imandra ermöglicht es Entwicklern, Algorithmen mit unvergleichlicher Automatisierung zu analysieren, was viel größere Anwendungen und Zielgruppen als diese Tools hat.

Wie eliminiert Imandras automatisierte Reasoning gemeinsame KI-Herausforderungen wie Halluzinationen und verbessert das Vertrauen in KI-Systeme?

Mit unserem Ansatz werden LLMs verwendet, um menschliche Anfragen in formale Logik zu übersetzen, die dann vom Reasoning-Engine mit vollständiger logischer Prüfung analysiert wird. Zwar können Übersetzungsfehler auftreten, wenn LLMs verwendet werden, aber der Benutzer erhält eine logische Erklärung, wie die Eingaben übersetzt wurden, und die logischen Prüfungen können von Open-Source-Software von Drittanbietern verifiziert werden. Unser ultimatives Ziel ist es, handlungsfähige Transparenz zu bieten, bei der KI-Systeme ihre Argumentation auf eine Weise erklären können, die unabhängig logisch überprüfbar ist.

Imandra wird von Goldman Sachs und DARPA unter anderen genutzt. Können Sie ein reales Beispiel dafür nennen, wie Ihre Technologie ein komplexes Problem gelöst hat?

Ein großartiges öffentliches Beispiel für die reale Wirkung von Imandra ist in unserem UBS Future of Finance-Wettbewerb zu sehen, den wir mit unserem 1. Platz (von über 620 Unternehmen weltweit) gewonnen haben. Während wir einen Fallstudie für UBS erstellten, die ein regulatorisches Dokument kodifizierte, das sie bei der SEC eingereicht hatten, identifizierte Imandra einen fundamentalen und subtilen Fehler in der Algorithmenbeschreibung. Der Fehler resultierte aus subtilen logischen Bedingungen, die erfüllt werden mussten, um Bestellungen in einer Orderbuch zu rangieren – etwas, das für Menschen “von Hand” unmöglich zu erkennen wäre. Die Bank hat uns den 1. Platz zuerkannt.

Wie hat Ihre Erfahrung bei Deutsche Bank die Anwendungen von Imandra in Finanzsystemen geprägt, und was ist der größte Einsatz, den Sie bisher gesehen haben?

Bei Deutsche Bank hatten wir es mit sehr komplexem Code zu tun, der automatisierte Handelsentscheidungen auf der Grundlage verschiedener ML-Eingaben, Risikoinikatoren usw. traf. Als jede Bank auch hatten wir zahlreiche Vorschriften einzuhalten. Was Grant und ich erkannten, war, dass dies auf mathematischer Ebene sehr ähnlich war zu der Forschung, die er für die Sicherheit von Autopilot-Systemen durchführte.

Jenseits der Finanzbranche, welche Branchen sehen Sie als diejenigen, die am meisten von der Neurosymbolik-KI profitieren können?

Wir haben gesehen, wie AlphaFold den Nobelpreis gewonnen hat, also zählen wir das definitiv… Letztendlich werden die meisten Anwendungen von KI erheblich von der Verwendung symbolischer Methoden profitieren, aber insbesondere arbeiten wir an den folgenden Agenten, die wir bald veröffentlichen werden: Code-Analyse (Übersetzung von Quellcode in mathematische Modelle), Erstellung strenger Modelle aus englischen Spezifikationen, Reasoning über SysML-Modelle (Sprache, die zur Beschreibung von Systemen in sicherheitskritischen Branchen verwendet wird) und Geschäftsprozessautomatisierung.

Imandras Region-Zerlegung ist eine neuartige Funktion. Können Sie erklären, wie sie funktioniert und wie wichtig sie bei der Lösung komplexer Probleme ist?

Eine Frage, über die jeder Ingenieur nachdenkt, wenn er Software schreibt, ist “Was sind die Randfälle?”. Wenn seine Aufgabe QA ist und er Unit-Testfälle schreiben oder Code schreiben muss und überlegt, ob er die Anforderungen korrekt implementiert hat. Imandra bringt wissenschaftliche Strenge, um diese Frage zu beantworten – sie behandelt den Code als mathematisches Modell und analysiert alle seine Randfälle symbolisch (während sie einen Beweis über die Vollständigkeit der Abdeckung erzeugt). Diese Funktion basiert auf einer mathematischen Technik namens “Cylindrical Algebraic Decomposition”, die wir auf Algorithmen im Allgemeinen “gehoben” haben. Sie hat unzählige Stunden für unsere Kunden im Finanzsektor gespart und kritische Fehler aufgedeckt. Jetzt bringen wir diese Funktion Ingenieuren überall hin.

Wie integriert Imandra Large Language Models, und welche neuen Fähigkeiten schaltet dies für generative KI frei?

LLMs und Imandra arbeiten zusammen, um menschliche Eingaben zu formalisieren (sei es Quellcode, englischer Text usw.), darüber zu argumentieren und dann die Ausgabe auf eine Weise zurückzugeben, die leicht verständlich ist. Wir verwenden agente Frameworks (z. B. Langgraph), um diese Arbeit zu orchestrieren und das Erlebnis als Agenten anzubieten, den unsere Kunden direkt nutzen oder in ihre Anwendungen oder Agenten integrieren können. Diese symbiotische Arbeitsweise adressiert viele der Herausforderungen bei der Verwendung von LLM-basierten KI-Tools und erweitert ihre Anwendung über das hinaus, was bisher mit Trainingsdaten gesehen wurde.

Was ist Ihre langfristige Vision für Imandra, und wie sehen Sie, dass sie KI-Anwendungen in verschiedenen Branchen verändert?

Wir denken, dass Neurosymbolik-Techniken die Grundlage bilden werden, die den Weg für die Erfüllung des Versprechens von KI ebnet. Symbolische Techniken sind das fehlende Ingredient für die meisten industriellen Anwendungen von KI, und wir sind begeistert, an der Spitze dieses nächsten Kapitels von KI zu sein.

Vielen Dank für das großartige Interview. Leser, die mehr erfahren möchten, sollten Imandra besuchen.