ImandraX : une avancée majeure dans le raisonnement neurosymbolique de l’IA et la vérification logique automatisée

Imandra Inc., l’entreprise d’IA qui révolutionne le raisonnement logique automatisé, a annoncé le lancement d’ImandraX, sa dernière avancée dans le raisonnement neurosymbolique de l’IA. Cette sortie marquante introduit des capacités de pointe en matière d’automatisation de la preuve, de génération de contre-exemples et de procédures de décision, établissant un nouveau standard industriel 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, explicatif et rigoureux sur le plan mathématique n’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 réels.

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

Imandra Inc. est une entreprise d’IA mondiale qui fait figure de pionnier dans les plates-formes de raisonnement logique automatisé pour les industries financières, de défense et de sécurité critique. Ses solutions avancées alimentées par l’IA comprennent Imandra Markets® et Imandra Connectivity®, qui fournissent des outils de vérification formelle rigoureuse, d’automatisation de la conception et de conformité pour les applications critiques. Fondée sur des avancées profondes dans le raisonnement automatisé, Imandra permet aux entreprises d’appliquer avec confiance des connaissances logiques, précises et auditablement pilotées par l’IA.
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 de l’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 dans le raisonnement de l’IA

Denis Ignatovich, co-fondateur et co-PDG d’Imandra Inc., a déclaré : “ImandraX est un pas transformationnel pour faire du raisonnement symbolique avancé une partie intégrante des flux de travail de l’IA. En équipant les agents d’IA de puissants 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 fruit 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 la prise de décision pilotée par l’IA.”

Innovations clés dans ImandraX

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

• Avancées dans l’automatisation de la preuve – 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 petit (<16 bit), essentiel pour la quantification et la distillation des réseaux de neurones.
• Vérification de la sécurité des réseaux de neurones – Équipe le premier vérificateur de preuve formellement vérifié pour la vérification des propriétés de sécurité des réseaux de neurones, en exploitant la vérification de modèle bornée 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 permet le développement de preuves parallèles, permettant aux travaux concurrents de s’exécuter dans le cloud de raisonnement d’Imandra et de rationaliser le flux de travail de vérification formelle.
• <strong<Intégration transparente de l'IA – ImandraX s’intègre sans heurt à la nouvelle API Python d’Imandra, permettant une adoption fluide dans les cadres d’agents d’IA, ouvrant la voie à la prochaine vague d’agents 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 pilotés par l’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 le deep learning, 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é pose un risque majeur dans les secteurs à haute tension 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, garantir 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 s’assurer qu’ils se comportent comme prévu et sont 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 est important pour la finance, la défense et les systèmes autonomes

Des 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, exigeant que les solutions pilotées par l’IA répondent à 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 industries doivent se conformer à des propriétés réglementaires et de sécurité strictes, mais leur complexité a considérablement augmenté par rapport à ce que les humains peuvent pleinement comprendre. L’automatisation de la preuve d’Imandra et la décomposition de l’espace d’états, 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 pilotés par l’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 dans des contraintes strictes, en garantissant que les décisions pilotées par l’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 garantissant 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 approfondies que les méthodes traditionnelles ne peuvent pas fournir. ImandraX intervient en offrant une vérification logique automatisée qui permet un test exhaustif basé sur des scénarios, en réduisant les risques associés à l’imprévisibilité de l’IA.

L’avenir de l’IA neurosymbolique et de la prise de décision pilotée par l’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 principales applications de l’IA aujourd’hui.”