Alors que les entreprises peinent à transformer les programmes pilotes d’IA en éléments fonctionnels de leur activité, la fiabilité occupe une place centrale. Une nouvelle startup espère résoudre ce problème en s’appuyant sur les outils de formalisation mathématique, combinant l’un des systèmes les plus fiables de l’informatique avec l’un des plus chaotiques.
Mercredi, Pramaana Labs a annoncé un financement de démarrage de 27 millions de dollars dirigé par Khosla Ventures, avec la participation d’Accel, Boldcap, Nexus Venture Partners, Premji Invest et Unbound.
Pramaana se concentrera sur des secteurs verticaux très sensibles comme le droit, la découverte de médicaments et la préparation des déclarations de revenus, où les erreurs peuvent être coûteuses et où la fiabilité est primordiale. Le déploiement de l’IA dans ces systèmes nécessitera des protections plus fortes contre les hallucinations et les erreurs que celles dont nous disposons actuellement. Mais selon Ranjan Rajagopalan, co-fondateur et PDG de Pramaana, ils sont également particulièrement adaptés à la formalisation.
« C’est comme les mathématiques dans le sens où vous devez respecter de nombreuses règles », a déclaré Rajagopalan à TechCrunch, décrivant les règles du code des impôts. « Une fois que vous en avez une version codifiée, le raisonnement qui s’y rattache commence à devenir déterministe. »
Le système de Pramaana fonctionne toujours sur un LLM conventionnel, ce qui lui donne la flexibilité nécessaire pour répondre à des questions en langage naturel et résoudre des problèmes complexes que les ordinateurs conventionnels ne peuvent pas gérer. Mais il y a une couche déterministe au-dessus de ce LLM qui garantit que le travail du LLM est vérifié.
Cette combinaison d’un moteur LLM avec une vérification déterministe est une configuration populaire ; L’approche unique de Pramaana consiste à utiliser les outils de vérification formelle, en s’appuyant sur le langage de programmation open source LEAN utilisé pour vérifier les preuves mathématiques. Il existe un véritable précédent pour une grande partie de ce travail ; Rajagopalan cite le projet français CATALA, qui formalise une grande partie du système fiscal et social du pays dans un code exécutable.
Pour chaque cas d’utilisation, Pramaana construira son propre système de vérification formelle de style LEAN, supervisé par des experts du domaine. Pour le droit fiscal, la société travaille avec l’ancien commissaire de l’IRS Danny Werfel, tandis que des professeurs de l’IIT Delhi, de l’IIT Madras et de l’UC Berkeley supervisent le système de cybersécurité et de découverte de médicaments.
« Les problèmes les plus difficiles du monde ne sont pas insolubles. Ils ne sont pas formalisés », déclare Rajagopalan. « Tous les domaines dans lesquels le fait de se tromper peut coûter à quelqu’un sa santé, son argent ou sa liberté ont des règles. »
Il ne reste plus qu’à codifier ces règles.
Lorsque vous achetez via des liens dans nos articles, nous pouvons gagner une petite commission. Cela n’affecte pas notre indépendance éditoriale.
