Introduction

Axiom Quant Inc., une startup spécialisée dans l'IA vérifiable, a annoncé avoir levé 200 millions de dollars dans le cadre d'une série A de financement. Cette levée de fonds porte la valorisation de l'entreprise à 1,6 milliard de dollars et vise à éliminer les risques liés à la génération de code par l'IA.

Contexte Technique

Les outils d'IA existants, tels que Claude Code et CodeRabbit, génèrent du code qui fonctionne souvent bien, mais leur nature probabiliste est une source de préoccupation majeure. Axiom contourne ce problème en formant des systèmes d'IA pour générer des sorties vérifiées formellement dans Lean, un langage de programmation spécialisé conçu pour les preuves mathématiques.

En utilisant Lean, Axiom peut garantir que chaque étape du processus de raisonnement d'un modèle d'IA est « vérifiable par machine » et logiquement garantie. Elle utilise des vérificateurs de preuve déterministes pour comprendre lorsque une sortie est incorrecte, ce qui signifie qu'elle peut fournir une certitude mathématique que toute fonction de code générée par un modèle d'IA renverra toujours la bonne réponse.

Analyse et Implications

Les implications de cette technologie sont considérables, car elle peut éliminer les risques liés à la génération de code par l'IA, tels que les « hallucinations » et les vulnérabilités de sécurité. Axiom voit une opportunité massive pour vérifier de manière probante chaque ligne de code générée par l'IA dans un monde où virtuellement tous les logiciels sont créés avec l'aide de grands modèles de langage.

Les partenaires de Menlo Ventures, Matt Kraning et C.C. Gong, ont souligné que les entreprises qui expédient du code généré par l'IA acceptent des risques inconnus, non seulement que le code pourrait produire des sorties incorrectes, mais qu'il pourrait également créer des surfaces d'attaque imprévues.

Perspective

La prochaine étape pour Axiom consiste à mettre à l'échelle son infrastructure de formation et à élargir son équipe d'experts en mathématiques, dans le but de rendre la vérification formelle rapide et abordable pour chaque entreprise utilisant l'IA. Avec cette technologie, Axiom est en mesure d'éliminer simultanément les deux catégories de risques liés à la génération de code par l'IA.