Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

Imaginez que vous essayez d'enseigner à un robot très intelligent et cultivé comment écrire une recette mathématique stricte pour une machine complexe. Cette machine est un « système distribué » (comme les serveurs cloud qui font tourner Amazon ou Microsoft), et la recette est écrite dans un langage spécial appelé TLA+.

Ce langage est comme un puzzle à enjeux élevés. Si vous manquez un seul petit symbole ou si vous vous trompez légèrement dans la logique, la machine pourrait fonctionner dans la recette, mais planter dans la réalité. Le problème est que rédiger ces recettes à la main est difficile et lent. Alors, les chercheurs se sont demandé : pouvons-nous simplement demander à une IA moderne (un grand modèle de langage, ou LLM) d'écrire ces recettes pour nous ?

Ce document est le premier grand rapport d'évaluation sur cette question. Voici ce qu'ils ont trouvé, expliqué simplement :

1. L'écart entre « Grammaire » et « Sens »

Les chercheurs ont demandé à 30 IA différentes d'écrire ces recettes TLA+ basées sur des descriptions en anglais courant.

• La bonne nouvelle (Grammaire) : Environ 26 % du temps, l'IA a écrit une recette qui semblait correcte en surface. Le « correcteur orthographique » (appelé SANY) a dit : « D'accord, les mots et les symboles sont dans le bon ordre. »
• La mauvaise nouvelle (Sens) : Cependant, lorsqu'ils ont réellement exécuté la recette via un « testeur de logique » (appelé TLC) pour voir si elle fonctionnait vraiment, seulement 8,6 % du temps elle a réussi.

L'analogie : Imaginez demander à un étudiant d'écrire un contrat juridique. L'étudiant utilise une orthographe et une grammaire parfaites (26 % de réussite), mais le contrat qu'il a écrit dit en réalité le contraire de ce qui était prévu, ou oublie une clause cruciale, le rendant juridiquement inutile (seulement 8,6 % de réussite). L'IA est douée pour imiter l'apparence du langage, mais elle échoue souvent à comprendre la logique sous-jacente.

2. Plus gros n'est pas toujours mieux

Habituellement, nous supposons qu'une IA plus grande et plus puissante fera un meilleur travail. Mais dans cette étude, ce n'était pas le cas.

• La surprise : Un modèle d'IA plus petit (DeepSeek r1:8b) a fait un bien meilleur travail que son « grand frère » massif (DeepSeek r1:70b).
• Pourquoi ? Le modèle plus petit a été entraîné spécifiquement pour « réfléchir étape par étape » (comme un étudiant en mathématiques montrant son raisonnement), tandis que le modèle plus grand a été entraîné sur tellement de données générales d'Internet qu'il s'est laissé dérouter par les règles strictes de TLA+. C'est comme un chef spécialisé qui sait exactement comment cuisiner un soufflé, par opposition à un généraliste qui sait tout cuisiner mais qui pourrait trop réfléchir à la recette spécifique.

3. Les « experts en code » ont échoué

Les chercheurs ont testé des IA célèbres pour écrire du code informatique (comme Python ou Java). Étonnamment, ces « experts en code » ont moins bien réussi que les IA à usage général.

• La raison : Ces modèles sont tellement habitués à écrire du code avec des points-virgules (;) ou des accolades ({}) qu'ils ont continué à insérer accidentellement ces symboles dans la recette TLA+. Comme TLA+ n'utilise pas ces symboles, la recette se brise immédiatement. C'est comme un menuisier essayant de réparer une montre mais utilisant accidentellement un marteau parce que c'est ce qu'il utilise pour tout le reste.

4. L'astuce du « pas à pas » a le mieux fonctionné

Les chercheurs ont testé quatre manières différentes de demander de l'aide à l'IA. La méthode la plus efficace s'appelle le « Prompting Progressif » (Progressive Prompting).

• Comment cela fonctionne : Au lieu de demander à l'IA d'écrire toute la recette d'un coup, on lui demande de la construire morceau par morceau : « D'abord, écris le titre. Maintenant, écris les variables. Maintenant, écris les règles. »
• Le résultat : C'était la seule méthode qui a produit des recettes entièrement fonctionnelles (le taux de réussite de 8,6 %). C'est comme construire une maison : si vous essayez de construire le toit, les murs et les fondations en un seul bond géant, vous échouerez probablement. Mais si vous construisez chaque pièce une par une, vous avez plus de chances de réussir.

5. Les « hallucinations » de l'IA

Le document a identé cinq façons spécifiques dont l'IA commet les mêmes erreurs, ce que les chercheurs appellent des « hallucinations » :

1. Mauvais symboles : Utiliser des symboles mathématiques sophistiqués (comme ∧) au lieu des symboles en texte brut que TLA+ exige (comme /\).
2. Mélange de langages : Ajouter accidentellement des points-virgules ou des accents graves provenant d'autres langages de programmation.
3. Réflexion à voix haute : L'IA colle parfois son propre « processus de réflexion » (comme ...) directement dans la recette finale, ce qui la casse.
4. Longueur incorrecte : Parfois, l'IA écrit une recette 9 fois trop longue, ou parfois, elle n'écrit presque rien du tout.
5. Structure brisée : Manquer les marqueurs de « fin » de la recette, laissant le document inachevé.

Le mot de la fin

Le document conclut que les IA actuelles ne peuvent pas encore écrire des spécifications TLA+ fiables de manière autonome. Bien qu'elles puissent imiter l'apparence du langage, elles font encore trop d'erreurs logiques pour être dignes de confiance sans qu'un expert humain ne vérifie chaque ligne.

Les chercheurs suggèrent que pour corriger cela, nous devons :

• Utiliser la méthode de prompting « étape par étape ».
• Utiliser des modèles plus petits, axés sur le raisonnement, plutôt que des modèles massifs et généraux.
• Construire des outils qui corrigent automatiquement les erreurs courantes (comme supprimer les mauvais symboles) avant même que l'IA ne tente d'exécuter la recette.

D'ici là, l'écriture de ces recettes de systèmes critiques reste un travail d'experts humains, l'IA agissant comme un assistant utile mais sujet à l'erreur.