Denis Ignatovich, Mitgründer und Co-CEO von Imandra – Interview-Serie

Denis Ignatovich, Mitgründer und Co-CEO von Imandra, hat über ein Jahrzehnt Erfahrung in Handel, Risikomanagement, quantitativem Modellieren und komplexer Handelssystementwicklung. Bevor er Imandra gründete, leitete er den zentralen Risikohandelsbereich bei Deutsche Bank (DB ) London, wo er die entscheidende Rolle von KI im Finanzsektor erkannte. Seine Erkenntnisse während dieser Zeit halfen bei der Gestaltung von Imandras Finanzproduktportfolio. Denis’ Beiträge zu computergestützter 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 von symbolischer Logik mit maschinellem Lernen verbessert es die Sicherheit, die Einhaltung von Vorschriften und die Effizienz und hilft Institutionen dabei, Risiken zu reduzieren und die Transparenz bei KI-gesteuerter Entscheidungsfindung 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 von automatisierter logischer Argumentation 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 der Finanzsektor solche Algorithmen erstellte, war wirklich problematisch (wie von vielen Nachrichtenartikeln über “Algo-Glitches” hervorgehoben), also haben wir uns entschieden, dies zu ändern, indem wir Ingenieure im Finanzsektor mit automatisierten logischen Werkzeugen ausstatten, um strenge wissenschaftliche Methoden bei der Software-Entwicklung und -Entwicklung einzusetzen. Allerdings haben wir letztendlich etwas Branchen-übergreifendes entwickelt.

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: statistische (die LLMs umfasst) und symbolische (auch als automatisierte Argumentation bekannt). Statistische KI ist unglaublich gut darin, Muster zu erkennen und Übersetzungen mithilfe der Informationen durchzuführen, die sie aus den Daten gelernt hat, auf denen sie trainiert wurde. Aber sie ist schlecht darin, logische Argumentationen zu führen. Die symbolische KI ist fast das Gegenteil – sie zwingt Sie, 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 Bereiche der KI kombinieren, werden als “Neurosymbolik” bezeichnet. Eine berühmte Anwendung dieses Ansatzes ist das AlphaFold-Projekt von DeepMind, das kürzlich den Nobelpreis gewonnen hat.

Was unterscheidet Imandra von anderen Anbietern im Bereich der Neurosymbolik-KI?

Es gibt viele unglaubliche symbolische Argumentationswerkzeuge da draußen (die meisten in der akademischen Welt), die sich auf bestimmte Nischen konzentrieren (z. B. Proteinfaltung), aber Imandra ermöglicht es Entwicklern, Algorithmen mit unvergleichlicher Automatisierung zu analysieren, was viel größere Anwendungen und Zielgruppen als diese Werkzeuge hat.

Wie eliminiert Imandras automatisierte Argumentation 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 von der Argumentations-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 Drittanbietern mit Open-Source-Software überprüft werden. Unser ultimatives Ziel ist es, handlungsfähige Transparenz zu schaffen, 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 (GS ) und DARPA unter anderen verwendet. Können Sie ein reales Beispiel dafür nennen, wie Ihre Technologie ein komplexes Problem gelöst hat?

Ein großartiges Beispiel für die reale Wirkung von Imandra ist unser Sieg beim UBS-Future-of-Finance-Wettbewerb (die Details mit Imandra-Code finden Sie auf unserer Website). Als wir für UBS einen Fallstudienbericht erstellten, der ein regulatorisches Dokument enthielt, das sie bei der SEC eingereicht hatten, entdeckte Imandra einen fundamentalen und subtilen Fehler in der Algorithmenbeschreibung. Der Fehler resultierte aus subtilen logischen Bedingungen, die erfüllt werden mussten, um Bestellungen in einem Orderbuch zu priorisieren – etwas, das für Menschen unmöglich zu erkennen wäre. Die Bank hat uns den 1. Platz zuerkannt (von über 620 Unternehmen weltweit).

Wie hat Ihre Erfahrung bei Deutsche Bank die Anwendungen von Imandra im Finanzsystem geprägt, und was ist der bedeutendste Einsatz, den Sie bisher gesehen haben?

Bei Deutsche Bank hatten wir es mit sehr komplexen 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.

Welche Branchen sehen Sie außerhalb der Finanzwirtschaft als am meisten geeignet, um von der Neurosymbolik-KI zu profitieren?

Wir haben gesehen, wie AlphaFold den Nobelpreis gewonnen hat, also zählen wir das definitiv… Letztendlich werden die meisten Anwendungen von KI 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, Argumentation ü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 für die Lösung komplexer Probleme ist?

Eine Frage, die jeder Ingenieur sich stellt, wenn er Software schreibt, ist: “Was sind die Randfälle?”. Wenn seine Aufgabe die Qualitätssicherung ist und er Unit-Tests schreiben muss oder er Code schreibt 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 “Zylindrische Algebraische Dekomposition”, die wir auf Algorithmen im Allgemeinen “gehoben” haben. Sie hat unseren Kunden im Finanzsektor unzählige Stunden gespart und kritische Fehler aufgedeckt. Jetzt bringen wir diese Funktion Ingenieuren überall hin.

Wie integriert Imandra sich mit großen Sprachmodellen und welche neuen Fähigkeiten schafft dies für generative KI?

LLMs und Imandra arbeiten zusammen, um menschliche Eingaben (sei es Quellcode, englischer Text usw.) zu formalisieren, zu argumentieren und dann die Ausgabe in einer verständlichen Weise zurückzugeben. Wir verwenden agentenbasierte Frameworks (z. B. Langgraph), um diese Arbeit zu orchestrieren und die Erfahrung als Agent zu liefern, den unsere Kunden direkt verwenden 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 die bisher gesehenen Trainingsdaten hinaus.

Was ist Ihre langfristige Vision für Imandra und wie sehen Sie es als Transformator von KI-Anwendungen in verschiedenen Branchen?

Wir denken, dass Neurosymbolik-Techniken die Grundlage bilden, die den Weg für die Erfüllung des Versprechens von KI ebnet. Symbolische Techniken sind das fehlende Ingrediens 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.