ImandraX : une avancée dans le raisonnement neurosymbolique et la vérification logique automatisée

Imandra Inc., l’entreprise d’IA qui révolutionne le raisonnement logique automatisé, a annoncé la sortie d’ImandraX, son dernier progrès dans le raisonnement neurosymbolique d’IA. Cette sortie marquante introduit des capacités de pointe dans l’automatisation des preuves, la génération de contre-exemples et les procédures de décision, établissant une nouvelle norme industrielle pour l’analyse logique pilotée par l’IA.

Alors que les systèmes d’IA alimentent de plus en plus d’applications critiques dans des secteurs tels que la finance, la défense, les soins de santé et les systèmes autonomes, la demande de raisonnement fiable, explicite et rigoureux sur le plan mathématique a jamais été plus élevée. ImandraX pousse les limites de l’IA en intégrant un raisonnement automatisé puissant avec des agents d’IA, des cadres de vérification et des modèles de prise de décision du monde réel.

Imandra Inc. : pionnier du raisonnement logique piloté par l’IA

Imandra Inc. est une entreprise d’IA mondiale qui met au point des plates-formes de raisonnement en tant que service pour le raisonnement logique automatisé dans les secteurs financiers, de la défense et des systèmes critiques. Ses solutions d’IA avancées comprennent Imandra Markets et Imandra Connectivity, qui fournissent des outils de vérification formelle, d’automatisation de la conception et de conformité pour les applications critiques. Fondés sur des progrès importants dans le raisonnement automatisé, Imandra permet aux entreprises d’appliquer avec confiance des connaissances d’IA pilotées par la logique, précises et auditable.
Imandra se consacre à apporter de la rigueur et une gouvernance aux algorithmes les plus critiques du monde. L’entreprise a construit un système de raisonnement automatisé à l’échelle du cloud, permettant aux organisations d’harnacher la logique mathématique pour le raisonnement d’IA. Avec un fort accent sur le développement d’une IA fiable et explicable, la technologie d’Imandra est utilisée par des chercheurs, des entreprises et des agences gouvernementales du monde entier.

Élever la barre du raisonnement d’IA

Denis Ignatovich, co-fondateur et co-PDG d’Imandra Inc., a déclaré : « ImandraX est une étape de transformation pour rendre le raisonnement symbolique avancé une partie intégrante des flux de travail d’IA. En équipant les agents d’IA de puissantes capacités de raisonnement logique automatisé et de vérification formelle, nous repoussons les limites de ce que les systèmes intelligents peuvent accomplir. »
Dr Grant Passmore, co-fondateur d’Imandra Inc., a ajouté : « ImandraX est le résultat de années de recherche et de déploiement dans le monde réel dans certains des secteurs les plus exigeants, notamment la finance, la défense et l’IA. Nos clients et partenaires s’appuient sur le raisonnement automatisé d’Imandra pour garantir la sécurité et la fiabilité des systèmes critiques, des échanges financiers aux agents autonomes. Avec ImandraX, nous ne rendons pas seulement le raisonnement rigoureux accessible, mais nous le rendons indispensable pour la prochaine génération de prise de décision d’IA. »

Innovations clés dans ImandraX

ImandraX introduit plusieurs capacités révolutionnaires, notamment :

• Avancées dans l’automatisation des preuves – Améliore le raisonnement logique en introduisant de nouvelles techniques pour les fonctions récursives discrètes et continues sur les types de données. Cette innovation permet la première modélisation formelle et la vérification de la nouvelle norme IEEE P3109 pour les formats de point flottant binaire de petite taille (<16 bits), essentiels pour la quantification et la distillation des réseaux de neurones.
• Vérification de la sécurité des réseaux de neurones – Équipe la première vérificatrice de preuves formellement vérifiée pour la vérification des propriétés de sécurité des réseaux de neurones, en utilisant la vérification de modèle borné d’ordre supérieur et l’induction pour garantir que les modèles d’IA fonctionnent de manière sûre et conforme à l’intention.
• Décomposition de l’espace d’états – Fournit plus de 4 fois d’accélération pour les tâches de décomposition de région, améliorant considérablement l’efficacité pour les utilisateurs de la finance dans les tests de connectivité FIX et d’autres applications critiques.
• Améliorations de l’expérience du développeur – Un nouveau plugin VS Code introduit permet le développement de preuves parallèles, permettant des travaux concurrents à s’exécuter dans le cloud de raisonnement d’Imandra et rationalisant le flux de travail de vérification formelle.
• Intégration transparente d’IA – ImandraX s’intègre sans effort à la nouvelle API Python d’Imandra, permettant une adoption fluide dans les cadres d’agents d’IA, ouvrant la voie à la prochaine vague de raisonnement neurosymbolique d’IA.

Répondre aux défis logiques les plus difficiles de l’IA

Denis Ignatovich a déclaré : « ImandraX s’appuie sur des années d’applications industrielles à grande échelle du raisonnement automatisé. La version X intègre de nouveaux algorithmes de raisonnement, des fonctionnalités architecturales révolutionnaires et une intégration transparente avec l’IA agente, y compris la bibliothèque Langgraph. »

Les réseaux de neurones et les modèles de prise de décision d’IA doivent faire face à une série de défis, notamment l’explicabilité, la vérifiabilité et la sécurité. De nombreux modèles d’IA actuels, en particulier ceux utilisés dans l’apprentissage profond, fonctionnent comme des “boîtes noires“, rendant difficile la compréhension ou la vérification de leurs processus de prise de décision. Cette opacité présente un risque majeur dans les secteurs à enjeux élevés tels que la finance, les soins de santé et les systèmes autonomes, où les décisions d’IA peuvent avoir des conséquences réelles profondes.

Pour les industries qui s’appuient sur les réseaux de neurones, assurer la robustesse et la sécurité est crucial. Ignatovich explique : « Les réseaux de neurones sont de plus en plus utilisés dans les industries critiques, il est donc très important de garantir qu’ils se comportent comme prévu et soient robustes face aux entrées bruyantes. La capacité d’ImandraX à raisonner sur le calcul numérique et son infrastructure de vérification formelle globale lui permettent de vérifier les propriétés des réseaux de neurones, tout en vérifiant la correction des preuves générées par des prouveurs de théorèmes tiers. »

Pourquoi cela compte pour la finance, la défense et les systèmes autonomes

Les secteurs tels que la finance, la défense et les systèmes autonomes opèrent dans des environnements où la précision, la fiabilité et la conformité sont primordiales. Les normes réglementaires dans ces domaines évoluent constamment, obligeant les solutions d’IA à répondre à des exigences de surveillance strictes. Le non-respect de ces réglementations peut entraîner des conséquences juridiques, des pertes financières et des risques pour la sécurité.

Ignatovich élabore : « Ces secteurs doivent respecter des propriétés réglementaires et de sécurité strictes, mais leur complexité a grandi bien au-delà de ce que les humains peuvent pleinement comprendre. L’automatisation des preuves et la décomposition de l’espace d’états d’Imandra, combinées à l’intégration LLM, permettent aux développeurs et aux ingénieurs d’analyser en profondeur le comportement du système, de garantir la conformité et de tester rigoureusement les systèmes d’IA. »

Dans les marchés financiers, les algorithmes d’IA sont responsables des décisions de trading en temps réel, de la détection de la fraude et de la gestion des risques. Même de petites discordances peuvent avoir des répercussions massives, rendant la vérification formelle et le raisonnement automatisé essentiels pour maintenir l’intégrité du système. De même, dans la défense, les systèmes autonomes doivent fonctionner sous des contraintes strictes, en garantissant que les décisions d’IA s’alignent sur les objectifs de mission et les protocoles de sécurité.

Les systèmes autonomes, y compris les véhicules et les drones sans pilote, dépendent de modèles d’IA qui doivent naviguer dans des environnements imprévisibles tout en assurant la sécurité des passagers et la conformité réglementaire. Garantir que ces systèmes d’IA fonctionnent de manière fiable dans toutes les conditions possibles nécessite des méthodes de test rigoureuses que les méthodes traditionnelles ne peuvent pas fournir. ImandraX intervient en offrant une vérification logique automatisée qui permet un test approfondi basé sur les scénarios, réduisant les risques associés à l’imprévisibilité de l’IA.

Le futur de l’IA neurosymbolique et de la prise de décision d’IA

Ignatovich a souligné : « Nous considérons les approches neurosymboliques comme le prochain grand pas dans l’évolution de l’IA. Les modèles statistiques traditionnels, tels que les LLM, manquent de raisonnement logique fondamental. ImandraX comble ce fossé, offrant une automatisation sans précédent pour l’analyse d’algorithmes complexes – l’une des applications clés de l’IA aujourd’hui. »