Des chercheurs proposent NeuroNL2LTL, une architecture neurosymbolique qui traduit le langage naturel en Linear Temporal Logic (LTL), le formalisme des systèmes critiques. Le problème : les approches purement neuronales produisent du texte fluide mais sans garanties de correction, tandis que les méthodes templates sont rigides et peu expressives.
La solution hybride fonctionne en trois temps. D'abord, un modèle neural traduit la phrase en représentation intermédiaire. Ensuite, un convertisseur structure-preserving mappe cette représentation vers du LTL valide par construction. Enfin, un système de vérification détecte les spécifications invalides ou triviales, puis les répare automatiquement via un mécanisme d'édition minimale.
Zéro triche, zéro correction manuelle..
L'enjeu est immédiat : la vérification formelle reste largement inaccessible faute d'expertise pour rédiger des specs LTL. Aujourd'hui, seuls des spécialistes peuvent traduire des exigences métier en logique temporelle. Ce goulot ralentit l'adoption dans l'aéronautique, l'automobile, les systèmes critiques.
Si ça marche à l'échelle, c'est un vrai déverrouillage : vérifier formellement des propriétés de sécurité devient accessible sans expertise logique. Les équipes produit dictent leurs garanties en français, le système produit des specs fiables. Zéro triche, zéro correction manuelle.