Denis Ignatovich, cofondateur et co-PDG d'Imanda – Série d'entretiens

Denis IgnatovitchDenis, cofondateur et co-PDG d'Imandra, possède plus d'une décennie d'expérience dans le trading, la gestion des risques, la modélisation quantitative et la conception de systèmes de trading complexes. Avant de fonder Imandra, il a dirigé le bureau central de négociation des risques de la Deutsche Bank de Londres, où il a reconnu le rôle essentiel que l'IA peut jouer dans le secteur financier. Ses connaissances au cours de cette période ont contribué à façonner la gamme de produits financiers d'Imandra. Les contributions de Denis à la logique informatique pour les plateformes de trading financier comprennent plusieurs brevets. Il est titulaire d'une maîtrise en finance de la London School of Economics et de diplômes en informatique et en finance de l'UT Austin.

Imandra est un moteur de raisonnement basé sur l'IA qui utilise l'IA neurosymbolique pour automatiser la vérification et l'optimisation d'algorithmes complexes, notamment dans les systèmes de trading financier et les logiciels. En combinant le raisonnement symbolique à l'apprentissage automatique, il améliore la sécurité, la conformité et l'efficacité, aidant ainsi les institutions à réduire les risques et à améliorer la transparence dans la prise de décision basée sur l'IA.

Qu'est-ce qui vous a poussé, vous et le Dr Grant Passmore, à cofonder Imandra, et comment vos antécédents ont-ils influencé la vision de l'entreprise ?

Après mes études, je me suis lancé dans le trading quantitatif et j'ai fini à Londres. Grant a fait son doctorat à Édimbourg, puis est parti à Cambridge pour travailler sur les applications du raisonnement logique automatisé pour l'analyse de la sécurité des systèmes de pilotage automatique (algorithmes complexes impliquant des calculs non linéaires). Dans mon travail, j'ai également eu affaire à des algorithmes complexes avec beaucoup de calculs non linéaires et nous avons réalisé qu'il existait un lien profond entre ces deux domaines. La façon dont la finance créait de tels algorithmes était vraiment problématique (comme le soulignent de nombreux articles de presse traitant de « problèmes d'algorithmes »), nous avons donc décidé de changer cela en dotant les ingénieurs de la finance d'outils logiques automatisés pour apporter des techniques scientifiques rigoureuses à la conception et au développement de logiciels. Cependant, ce que nous avons fini par créer est indépendant du secteur.

Pouvez-vous expliquer ce qu’est l’IA neurosymbolique et en quoi elle diffère des approches d’IA traditionnelles ?

Le domaine de l’IA comprend (en gros !) deux domaines : statistique (qui comprend les LLM) et symbolique (c’est-à-dire le raisonnement automatisé). L’IA statistique est incroyable pour identifier des modèles et effectuer des traductions en utilisant les informations qu’elle a apprises à partir des données sur lesquelles elle a été formée. Mais elle est mauvaise en raisonnement logique. L’IA symbolique est presque l’exact opposé – elle vous oblige à être très précis (mathématiquement) dans ce que vous essayez de faire, mais elle peut utiliser la logique pour raisonner d’une manière qui est (1) logiquement cohérente et (2) ne nécessite pas de données pour l’entraînement. Les techniques combinant ces deux domaines de l’IA sont appelées « neurosymboliques ». Une application célèbre de cette approche est le projet AlphaFold de DeepMind, qui a récemment remporté le prix Nobel.

Selon vous, qu’est-ce qui distingue Imandra dans la conduite de la révolution de l’IA neurosymbolique ? 

Il existe de nombreux raisonneurs symboliques incroyables (la plupart dans le milieu universitaire) qui ciblent des niches spécifiques (par exemple, le repliement des protéines), mais Imandra permet aux développeurs d'analyser des algorithmes avec une automatisation sans précédent qui a des applications beaucoup plus importantes et des publics cibles plus larges que ces outils.

Comment le raisonnement automatisé d’Imandra élimine-t-il les défis courants de l’IA, tels que les hallucinations, et améliore-t-il la confiance dans les systèmes d’IA ?

Avec notre approche, les LLM sont utilisés pour traduire les demandes des humains en logique formelle qui est ensuite analysée par le moteur de raisonnement avec une piste d'audit logique complète. Bien que des erreurs de traduction puissent se produire lors de l'utilisation du LLM, l'utilisateur reçoit une explication logique de la manière dont les entrées ont été traduites et les audits logiques peuvent être vérifiés par un logiciel open source tiers. Notre objectif ultime est d'apporter une transparence exploitable, où les systèmes d'IA peuvent expliquer leur raisonnement d'une manière qui soit logiquement vérifiable de manière indépendante.

Imandra est utilisé par Goldman Sachs et DARPA, entre autres. Pouvez-vous nous donner un exemple concret de la manière dont votre technologie a permis de résoudre un problème complexe ?

Un excellent exemple public de l’impact réel d’Imandra dans le monde réel est mis en évidence dans notre Concours UBS « Future of Finance » 1ère place (les détails avec le code Imandra sont sur notre site Web). En créant une étude de cas pour UBS qui encodait un document réglementaire qu'ils soumettaient à la SEC, Imandra a identifié une faille fondamentale et subtile dans la description de l'algorithme. La faille provenait de conditions logiques subtiles qui doivent être remplies pour classer les ordres dans un carnet d'ordres - quelque chose qu'il serait impossible pour les humains de détecter « à la main ». La banque nous a décerné la 1ère place (sur plus de 620 entreprises dans le monde).

Comment votre expérience à la Deutsche Bank a-t-elle façonné les applications d’Imandra dans les systèmes financiers, et quel est le cas d’utilisation le plus impactant que vous ayez vu jusqu’à présent ?

Chez Deutsche Bank, nous avons eu affaire à un code très complexe qui automatisait les décisions de trading en fonction de diverses entrées ML, d'indicateurs de risque, etc. Comme toute banque, nous devions également respecter de nombreuses réglementations. Grant et moi avons réalisé que cela ressemblait beaucoup, sur le plan mathématique, aux recherches qu'il effectuait sur la sécurité du pilotage automatique.

Au-delà de la finance, quels secteurs ont selon vous le plus grand potentiel pour bénéficier de l’IA neurosymbolique ?

Nous avons vu AlphaFold obtenir le prix Nobel, alors comptons certainement celui-là… En fin de compte, la plupart des applications de l'IA bénéficieront grandement de l'utilisation de méthodes symboliques, mais plus précisément, nous travaillons sur les agents suivants que nous publierons bientôt : l'analyse de code (traduction du code source en modèles mathématiques), la création de modèles rigoureux à partir de spécifications en prose anglaise, le raisonnement sur les modèles SysML (langage utilisé pour décrire les systèmes dans les industries critiques pour la sécurité) et l'automatisation des processus métier.

La décomposition de la région d'Imandra est une fonctionnalité nouvelle. Pouvez-vous expliquer son fonctionnement et son importance dans la résolution de problèmes complexes ?

Une question que tout ingénieur se pose lorsqu'il écrit un logiciel est « quels sont les cas limites ? ». Lorsque leur travail consiste à assurer l'assurance qualité et qu'ils doivent écrire des cas de test unitaires ou qu'ils écrivent du code et se demandent s'ils ont correctement implémenté les exigences. Imandra apporte une rigueur scientifique pour répondre à cette question : il traite le code comme un modèle mathématique et analyse symboliquement tous ses cas limites (tout en produisant une preuve de l'exhaustivité de la couverture). Cette fonctionnalité est basée sur une technique mathématique appelée « décomposition algébrique cylindrique », que nous avons « étendue » aux algorithmes en général. Elle a permis à nos clients du secteur financier de gagner d'innombrables heures et de découvrir des erreurs critiques. Nous proposons désormais cette fonctionnalité aux ingénieurs du monde entier.

Comment Imandra s’intègre-t-il aux grands modèles linguistiques et quelles nouvelles capacités cela ouvre-t-il pour l’IA générative ?

Les LLM et Imandra travaillent ensemble pour formaliser les apports humains (qu'il s'agisse de code source, de prose anglaise, etc.), raisonner à leur sujet, puis renvoyer le résultat d'une manière facile à comprendre. Nous utilisons des cadres d'agents (par exemple Langgraph) pour orchestrer ce travail et fournir l'expérience en tant qu'agent que nos clients peuvent utiliser directement ou intégrer dans leurs applications ou agents. Ce flux de travail symbiotique répond à de nombreux défis liés à l'utilisation d'outils d'IA uniquement LLM et étend leur application au-delà des données de formation précédemment vues.

Quelle est votre vision à long terme pour Imandra et comment voyez-vous qu’elle transformera les applications d’IA dans tous les secteurs ?

Nous pensons que les techniques neurosymboliques constitueront la base qui nous permettra de concrétiser les promesses de l’IA. Les techniques symboliques sont l’ingrédient manquant pour la plupart des applications industrielles de l’IA et nous sommes ravis d’être à l’avant-garde de ce prochain chapitre de l’IA.

Merci pour cette excellente interview, les lecteurs qui souhaitent en savoir plus devraient visiter Imandra.