Denis Ignatovich, Co-fondateur et Co-PDG d’Imandra – Série d’entretiens

Denis Ignatovich, Co-fondateur et Co-PDG d’Imandra, compte plus d’une décennie d’expérience dans le domaine du trading, de la gestion des risques, de la modélisation quantitative et de la conception de systèmes de trading complexes. Avant de fonder Imandra, il a dirigé le bureau de trading de risques centrales de Deutsche Bank (DB ) à Londres, où il a reconnu le rôle critique que l’IA peut jouer dans le secteur financier. Ses connaissances acquises à cette époque ont contribué à façonner la gamme de produits financiers d’Imandra. Les contributions de Denis à la logique computationnelle pour les plateformes de trading financier incluent plusieurs brevets. Il détient un master en finance de la London School of Economics et des 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, en particulier dans le trading financier et les systèmes logiciels. En combinant le raisonnement symbolique avec l’apprentissage automatique, il améliore la sécurité, la conformité et l’efficacité, aidant 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 inspiré, vous et le Dr Grant Passmore, à co-fonder Imandra, et comment vos parcours ont-ils influencé la vision de l’entreprise ?

Après mes études, je suis entré dans le trading quantitatif et j’ai fini par travailler à Londres. Grant a fait son doctorat à Édimbourg, puis s’est installé à Cambridge pour travailler sur les applications de la raisonnement logique automatisée pour l’analyse de la sécurité des systèmes de pilotage automatique (algorithmes complexes qui impliquent des calculs non linéaires). Dans mon travail, j’ai également traité d’algorithmes complexes avec de nombreux calculs non linéaires, et nous avons réalisé qu’il y avait une profonde connexion entre ces deux domaines. La façon dont la finance créait ces algorithmes était vraiment problématique (comme le montrent de nombreuses histoires dans les actualités sur les “erreurs d’algo”), nous nous sommes donc lancés pour 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 de l’industrie.

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

Le domaine de l’IA comporte (très grossièrement !) deux domaines : statistique (qui inclut les LLM) et symbolique (également appelé raisonnement automatisé). L’IA statistique est incroyable pour identifier les 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 pour le raisonnement logique. L’IA symbolique est presque l’opposé exact – elle vous oblige à être très précis (mathématiquement) sur 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 la formation. Les techniques qui combinent 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.

Qu’est-ce qui distingue Imandra dans la révolution de l’IA neurosymbolique ?

Il existe de nombreux raisonneurs symboliques incroyables (la plupart dans le monde universitaire) qui ciblent des niches spécifiques (par exemple, le pliage des protéines), mais Imandra permet aux développeurs d’analyser les algorithmes avec une automatisation sans précédent, ce qui a des applications et un public cible beaucoup plus larges que ces outils.

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

Avec notre approche, les LLM sont utilisés pour traduire les demandes humaines en logique formelle, qui est ensuite analysée par le moteur de raisonnement avec une traçabilité logique complète. Même si des erreurs de traduction peuvent survenir lors de l’utilisation du LLM, l’utilisateur est fourni avec une explication logique de la façon dont les entrées ont été traduites et les audits logiques peuvent être vérifiés par des logiciels open source tiers. Notre objectif ultime est d’apporter une transparence opérationnelle, où les systèmes d’IA peuvent expliquer leur raisonnement d’une manière qui est logiquement vérifiable de manière indépendante.

Imandra est utilisé par Goldman Sachs (GS ) et DARPA, entre autres. Pouvez-vous partager un exemple concret de la façon dont votre technologie a résolu un problème complexe ?

Un excellent exemple concret de l’impact réel d’Imandra est mis en évidence dans notre premier prix du concours UBS Future of Finance (les détails avec le code Imandra sont sur notre site Web). Lors de la création d’une étude de cas pour UBS qui codait un document réglementaire qu’ils ont soumis à 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 qui aurait été impossible pour les humains de détecter “à la main”. La banque nous a attribué le premier prix (sur plus de 620 entreprises dans le monde).

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

Chez Deutsche Bank, nous avons traité de nombreux codes très complexes qui prenaient des décisions de trading automatisées basées sur diverses entrées d’apprentissage automatique, d’indicateurs de risque, etc. Comme toute banque, nous devions également respecter de nombreuses réglementations. Ce que Grant et moi avons réalisé, c’est que cela était très similaire, sur le plan mathématique, à la recherche qu’il menait sur la sécurité des systèmes de pilotage automatique.

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

Nous avons vu AlphaFold remporter le prix Nobel, alors comptons-le… 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 allons publier bientôt : analyse de code (traduction du code source en modèles mathématiques), création de modèles rigoureux à partir de spécifications en prose anglaise, raisonnement sur les modèles SysML (langage utilisé pour décrire les systèmes dans les industries critiques) et automatisation des processus métier.

La décomposition de région d’Imandra est une fonctionnalité innovante. Pouvez-vous expliquer comment elle fonctionne et son importance dans la résolution de problèmes complexes ?

Une question que chaque ingénieur se pose lorsqu’il écrit du code est “quels sont les cas de bordure ?”. Lorsque leur travail est de QA et qu’ils doivent écrire des cas de test unitaires ou qu’ils écrivent du code et réfléchissent à savoir s’ils ont correctement mis en œuvre les exigences. Imandra apporte une rigueur scientifique pour répondre à cette question – elle traite le code comme un modèle mathématique et analyse symboliquement tous les cas de bordure (tout en produisant une preuve de la complétude de la couverture). Cette fonctionnalité repose sur une technique mathématique appelée “décomposition algébrique cylindrique”, que nous avons “élevée” aux algorithmes en général. Elle a économisé d’innombrables heures pour nos clients dans le domaine financier et a découvert des erreurs critiques. Nous allons maintenant apporter cette fonctionnalité aux ingénieurs partout dans le monde.

Comment Imandra intègre-t-elle les grands modèles de langage, et quelles nouvelles capacités cela débloque-t-il pour l’IA générative ?

Les LLM et Imandra travaillent ensemble pour formaliser les entrées humaines (que ce soit du code source, de la prose anglaise, etc.), les analyser et puis retourner la sortie d’une manière facile à comprendre. Nous utilisons des cadres d’agents (par exemple, Langgraph) pour orchestrer ce travail et offrir 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 de l’utilisation d’outils d’IA basés uniquement sur les 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 l’entreprise transformer les applications d’IA à travers les industries ?

Nous pensons que les techniques neurosymboliques seront le fondement qui ouvre la voie à la réalisation de la promesse 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.

Je vous remercie pour cette excellente interview, les lecteurs qui souhaitent en savoir plus peuvent visiter Imandra.