Face à l’essor des systèmes d’intelligence artificielle capables de générer du code pour des applications critiques — comme les logiciels de contrôle des centrales nucléaires ou les systèmes autonomes de conduite — une question fondamentale se pose : comment garantir que ce code est absolument fiable ? Les modèles d’IA actuels, bien qu’extrêmement performants, souffrent d’un défaut structurel : ils dépendent fortement de tests humains pour valider leur sortie. Or, cette approche présente deux limites majeures. Premièrement, le nombre de cas de test nécessaires croît de manière exponentielle avec la complexité du code — même pour des problèmes de niveau LeetCode, il faut souvent une dizaine de tests pour couvrir une partie significative du comportement. Deuxièmement, les tests ne peuvent pas explorer toutes les branches logiques possibles, laissant subsister des failles profondes et difficiles à détecter. Face à ce défi, l’équipe Veri-Code du Laboratoire d’intelligence artificielle de Shanghai, dirigée par le jeune chercheur Fu Jie, propose une nouvelle voie : une validation formelle du code par des outils mathématiques, sans dépendre des connaissances humaines préalables. Leur approche repose sur des langages formels comme Dafny, capables de produire des preuves mathématiques de correction. Ces preuves, une fois validées, garantissent que le code se comporte exactement comme prévu — avec une certitude équivalente à celle d’un théorème mathématique. Comme l’a souligné le lauréat du prix Turing Yoshua Bengio : « Même avec une intelligence super-évoluée, les théorèmes restent vrais. » Le problème actuel réside dans la dépendance aux humains : les méthodes existantes exigent des centaines d’heures de travail humain pour annoter des chaînes de raisonnement (chain-of-thought, CoT) et fournir des signaux de récompense fiables. Pour un simple programme, cela peut prendre 220 heures à deux experts ; pour vérifier le noyau SeL4, cela représente 20 années-personne. Cette approche est non seulement coûteuse, mais aussi intrinsèquement limitée : elle force l’IA à imiter des raisonnements humains imparfaits, ce qui freine son potentiel d’évolution à long terme. C’est ici que l’approche de Fu Jie et de son équipe, baptisée Re:Form, entre en jeu. Inspirés par l’idée du « multivers mathématique » de Max Tegmark — selon laquelle tout système mathématiquement cohérent existe dans une réalité possible —, ils explorent l’idée que les logiciels, en tant que systèmes formels, peuvent être modélisés et validés rigoureusement à l’aide de logiques mathématiques. L’environnement formel fournit une rétroaction objective, absolue, indépendante des biais humains. C’est là que réside la clé : utiliser ces environnements comme cadre d’apprentissage automatique, en particulier via l’apprentissage par renforcement (RL). La stratégie consiste à entraîner un modèle d’IA pour qu’il génère directement du code Dafny accompagné d’une spécification formelle, puis à valider cette spécification à l’aide d’un vérificateur mathématique. L’innovation majeure ? Éliminer complètement les annotations humaines de type CoT et les jugements subjectifs. Au lieu de cela, l’IA reçoit une récompense basée sur la vérification formelle (pass/fail), et surtout, sur une nouvelle métrique : le taux de supériorité de la spécification (SSR). Ce dernier mesure si la spécification générée est plus précise, plus générale ou plus stricte que celle du « ground truth » — par exemple, en imposant moins de contraintes sur les entrées ou en décrivant plus précisément les sorties. Pour construire les données d’entraînement, l’équipe a développé un pipeline de traduction : ils ont converti des programmes Python existants en code Dafny vérifiable, puis ont utilisé ces données pour entraîner un modèle pré-entraîné (Qwen2.5-coder) via une fine-tuning supervisée, avant de passer à l’apprentissage par renforcement. Le résultat est impressionnant : les modèles Re:Form (de 0,5 à 14 milliards de paramètres) surpassent GPT-4o et Claude 4 sur plusieurs benchmarks, notamment DafnyComp, un test conçu pour évaluer la capacité à combiner des modules validés. Cette avancée ouvre la voie à une nouvelle génération d’IA « sûre par conception ». L’objectif ultime ? Développer un outil plug-in, similaire à CodeRabbit, capable d’analyser automatiquement le code généré par une IA et de confirmer qu’il correspond exactement aux besoins. Cela permettrait d’assurer la sécurité dans des domaines critiques comme la santé, la finance, les véhicules autonomes ou les systèmes d’exploitation. Enfin, Fu Jie souligne que l’IA n’a pas besoin de copier le raisonnement humain pour être efficace. L’avenir réside dans des modèles capables d’apprendre à raisonner de manière formelle, sans dépendre des connaissances humaines préalables. Comme l’a dit Rich Sutton dans son essai « The Bitter Lesson » : les progrès durables viennent non pas de l’ingénierie de connaissances humaines, mais de l’extension des capacités de recherche et d’apprentissage. Re:Form incarne cette vision : une IA qui ne copie pas l’humain, mais qui le dépasse — en s’appuyant sur la rigueur mathématique.