LLM2Cert vérifie 81 des 105 certificats de stabilité et de sécurité

Les modèles de langage ont appris à écrire du code et à démontrer des théorèmes. On cherche maintenant à les appliquer à un problème d'ingénierie où l'erreur coûte cher : confirmer qu'un système dynamique reste stable et sûr. Les auteurs du preprint LLM2Cert (arXiv 2610.30524) ont conçu un framework dans lequel un LLM propose des certificats et des vérificateurs formels les contrôlent. Sur le nouveau benchmark DynaCertBench, qui compte 105 tâches, le système en vérifie 81, soit 77,1%. C'est 17,1 points de pourcentage de plus qu'une génération unique sans retour des vérificateurs (environ 60%).

Pourquoi les certificats restent un goulot d'étranglement

Les fonctions de Lyapunov et les certificats de barrière donnent des garanties dans l'espace d'états. Les premières montrent que le système est stable, les seconds prouvent qu'il ne sortira pas vers une zone dangereuse. La difficulté : il faut d'abord trouver ces fonctions, puis les vérifier rigoureusement. Pour les systèmes non linéaires multidimensionnels, le problème reste ouvert.

Les pipelines existants vérifient les candidats de trois façons : solveurs numériques (programmes sum-of-squares), méthodes par intervalles et solveurs SMT. Les trois partagent les mêmes défauts. Ils exigent des relaxations, restent conservateurs ou passent mal à l'échelle quand la dimension et la non-linéarité du modèle augmentent.

Les auteurs pointent aussi un effet de bord. Les jeux de test standard se composent surtout de systèmes polynomiaux de faible dimension, choisis en fonction des capacités des solveurs plutôt que des besoins de l'ingénierie. Les benchmarks reflètent ce que savent faire les outils, pas ce dont la pratique a besoin.

DynaCertBench et routage des obligations

La première partie du travail porte sur le jeu de test. DynaCertBench contient 105 tâches :

• 80 systèmes non redondants, sélectionnés dans la littérature ;
• des extensions de ces systèmes avec des variantes multidimensionnelles et des variantes avec contraintes de commande ;
• de nouveaux systèmes à couplage non linéaire ;
• quatre classes de tâches : stabilité, région d'attraction (region of attraction), invariance avant (forward invariance) et sécurité.

La seconde partie est LLM2Cert proprement dit. Le modèle génère un certificat candidat, puis le framework le décompose en obligations de preuve. Chaque obligation suit l'un de deux chemins : un solveur SMT ou, directement, l'agent Lean Proof-Repair. Lean joue ici le rôle de vérificateur formel strict, et l'agent répare la preuve lorsqu'elle ne converge pas. C'est le retour des vérificateurs qui apporte l'essentiel du gain : sans lui, un modèle qui ne produit qu'un seul candidat résout nettement moins de tâches.

Les chiffres à retenir

• DynaCertBench : 105 tâches, dont 80 issues de la littérature.
• LLM2Cert vérifie 81 tâches sur 105, soit 77,1%.
• Gain par rapport à une proposition one-shot sans retour : 17,1 points de pourcentage.
• Sur les 81 certificats trouvés, 22 sont vérifiés là où l'approche All-SMT, qui envoie tout au solveur SMT, laisse la question ouverte.

Ce dernier chiffre est sans doute le plus parlant. Il représente près d'un quart des certificats du jeu de test, hors de portée d'un SMT seul. Le routage hybride résout une partie des tâches que le SMT ne parvient pas à traiter à lui seul.

L'article est signé Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue et Alessandro Abate. Le code et les données sont publiés dans le dépôt FormalCert-AI/llm2cert.

À qui cela servira en premier

L'effet pratique est attendu là où la commande de systèmes non linéaires exige des garanties formelles : robotique, transport autonome, réseaux électriques, avionique. Aujourd'hui, l'ingénieur doit choisir un certificat à la main ou passer par des programmes SOS, qui butent sur la dimension. Le schéma « le LLM propose, le solveur et Lean vérifient » confie la part créative au modèle et laisse la confiance à la vérification formelle. Même si le modèle se trompe, un certificat erroné ne passera pas la vérification.

Pour les chercheurs, DynaCertBench est utile en soi : il permet de comparer de nouvelles méthodes de synthèse sur des tâches plus proches des systèmes réels que les polynômes de faible dimension habituels. Le code ouvert permet de reproduire les résultats et de brancher un autre modèle. Restent 24 tâches sur 105 que LLM2Cert n'a pas résolues, et elles montrent où se situent les limites de la méthode.