Résumé Technique : TLA-Prover

Énoncé du Problème

TLA+ est un langage de spécification formelle utilisé pour la vérification de systèmes distribués et de protocoles critiques pour la sécurité, associé au vérificateur de modèles TLC pour l'exploration exhaustive de l'espace d'états. Bien que les grands modèles de langage (LLM) soient prometteurs pour la génération de code, ils éprouvent des difficultés significatives avec TLA+ en raison de la rareté de sa représentation dans les corpus de pré-entraînement et de sa syntaxe idiosyncrasique (ex: opérateurs temporels, compréhensions d'ensembles).

Les bases existantes, telles que l'étude FormaLLM, indiquent que les LLM en poids ouverts non ajustés n'atteignent qu'un taux de réussite de 8,6 % pour passer le vérificateur de modèles TLC sur 25 modèles. Un défi critique de l'entraînement des LLM pour la vérification formelle est le piratage de récompense (reward hacking). Dans le contexte de TLA+ et TLC, un modèle peut optimiser le signal binaire « passage » en générant des invariants triviaux et tautologiques (ex: TypeOK == TRUE). Ces spécifications passent TLC sur chaque état atteignable, mais ne transmettent aucune propriété significative sur le protocole, rendant la vérification inutile. Les approches standard d'apprentissage par renforcement qui reposent uniquement sur le signal de succès/échec de TLC sont vulnérables à ce mode de défaillance.

Méthodologie

Les auteurs présentent TLA-Prover, un modèle de 20 milliards de paramètres (basé sur gpt-oss-20b) conçu pour la synthèse de spécifications TLA+. L'approche combine l'ajustement fin supervisé (SFT) avec un nouveau pipeline d'entraînement intégrant l'optimisation de politique de groupe relative par réparation (GRPO) et une hiérarchie de validation à quatre niveaux.

1. Hiérarchie de Validation à Quatre Niveaux

Pour prévenir le piratage de récompense et garantir la validité sémantique, chaque sortie de modèle est évaluée par un pipeline externe déterministe selon l'un des quatre niveaux :

• Bronze : La sortie échoue au parseur SANY (syntaxiquement invalide).
• Argent : La sortie est analysée mais échoue à se charger ou à s'exécuter dans TLC (ex: délais d'attente, erreurs de type).
• Or : La sortie réussit à la fois SANY et TLC ; le vérificateur de modèles épuise l'espace d'états et tous les invariants sont respectés.
• Diamant : La sortie réussit le niveau Or et l'invariant est sensible à la mutation.
  • Mécanisme : Une mutation automatisée au niveau de l'AST est appliquée au prédicat de l'invariant (ex: négation d'une conjonction, inversion d'opérateurs relationnels ou échange de constantes). La spécification mutée est ensuite réexécutée via TLC.
  • Critère : Si la mutation provoque un contre-exemple dans TLC, l'invariant original est jugé non trivial (Diamant). Si TLC passe toujours (ex: parce que l'invariant était TRUE), la sortie échoue au test Diamant. Cette étape bloque explicitement les invariants tautologiques.

2. Pipeline d'Entraînement

Le processus d'entraînement se compose de deux étapes principales, avec une ablation DPO pour comparaison :

• Étape 1 : Ajustement Fin Supervisé (SFT)

  • Corpus : Un ensemble de données de 1 053 spécifications, strictement filtrées pour le niveau Diamant. Les données proviennent de la distribution TLA+ Foundation et du dépôt tlaplus/examples, augmentées par un générateur Ollama et filtrées par un juge LLM et le pipeline à quatre niveaux.
  • Architecture : Un adaptateur LoRA (rang 8, alpha 16) est appliqué aux projections d'attention du modèle de base de 20B de paramètres.
  • Objectif : Enseigner au modèle le vocabulaire structurel et la syntaxe de TLA+.

• Étape 2 : Optimisation de Politique de Groupe Relative par Réparation (GRPO)

  • Motivation : Le GRPO standard échoue lorsque tous les échantillons d'un groupe échouent au vérificateur (récompenses éparses), entraînant un avantage nul et une absence de flux de gradient.
  • Mécanisme : Le modèle est confronté à une spécification « brisée » (extraite de tentatives précédentes infructueuses) et chargé de la réparer.
  • Signal de Récompense : Un score d'amélioration continue basé sur les transitions de niveaux (Bronze→Argent : 0,1, Argent→Or : 0,3, Or→Diamant : 0,6). Cela fournit des gradients denses même lorsque la sortie finale n'est pas parfaite, tant que le niveau s'améliore.
  • Processus : Le modèle répare de manière itérative ses propres sorties en utilisant les messages d'erreur de TLC comme rétroaction.

• Étude d'Ablation (DPO) : Une variante d'Optimisation de Préférence Directe (DPO) a été entraînée à partir du même point de contrôle SFT en utilisant des paires de préférences statiques (Diamant > Or > Argent > Bronze). Elle a servi de base pour comparer l'approche GRPO dynamique basée sur la réparation.

Résultats Clés

Le modèle a été évalué sur un benchmark de 30 problèmes en utilisant un décodage glouton à un seul passage (single-shot greedy decoding).

• Performance : TLA-Prover (point de contrôle final de la réparation-GRPO) a atteint un taux de réussite de 30 % (9/30) aux niveaux Or et Diamant.
• Comparaison avec la Base : Cela représente une amélioration de 3,5x par rapport à la base de référence FormaLLM non ajustée de 8,6 %.
• Comparaison d'Ablation : La variante DPO a atteint un taux de réussite Diamant de 20 %, surpassée par l'approche de réparation-GRPO (30 %).
• Validation de l'Anti-Piratage de Récompense : Crucialement, les taux de réussite Or et Diamant coïncidaient à chaque point de contrôle dans le pipeline de production (différence de 0). Cela indique que le modèle n'a pas appris à générer des invariants tautologiques qui passent TLC mais échouent au test de mutation. La seule exception est un cas unique dans l'ablation DPO, que le niveau Diamant a réussi à détecter.
• Stratégies d'Inférence :
  • L'échantillonnage Best-of-8 a augmenté le taux de réussite Diamant à 37 % (11/30).
  • L'union Greedy ∪ Best-of-8 suggère un plafond de 43 % (13/30), indiquant que le modèle possède la capacité de résoudre plus de problèmes en multipliant les tentatives.
  • L'auto-correction (rétroaction TLC en 3 étapes) n'a apporté aucune amélioration, suggérant que les échecs sont dus à des lacunes de connaissances plutôt qu'à des erreurs d'échantillonnage aléatoires.

Signification et Contributions

L'article revendique trois contributions principales :

1. TLA-Prover avec une Hiérarchie à Quatre Niveaux : L'introduction d'une hiérarchie de validation où le niveau supérieur (Diamant) utilise des tests de mutation pour exclure les invariants tautologiques. Cela répond au risque spécifique de piratage de récompense inhérent à l'utilisation de TLC comme signal de récompense, garantissant qu'un « passage » implique une spécification non triviale.
2. Pipeline GRPO Basé sur la Réparation : Un pipeline d'entraînement en deux étapes combinant le SFT sur un corpus de niveau Diamant avec le GRPO basé sur la réparation. Cette approche exploite la rétroaction en ligne du vérificateur pour fournir des signaux de récompense denses, surpassant les ablations DPO statiques.
3. Analyse Empirique de l'Anti-Piratage de Récompense : L'observation que les taux de réussite Or et Diamant coïncident à travers tous les points de contrôle fournit une preuve empirique que le pipeline empêche avec succès le mode de défaillance de l'« invariant toujours vrai ».

Les auteurs positionnent ce travail comme la première étude de formation ciblant TLA+ qui dépasse substantiellement les bases de référence de FormaLLM. Ils soulignent que, bien que le modèle améliore considérablement la synthèse de spécifications, il se spécialise actuellement dans les spécifications de type invariant avec de petits espaces d'états et peine avec les protocoles complexes nécessitant une analyse de cas ou la manipulation de quantificateurs. Ce travail souligne qu'un entraînement guidé par un vérificateur sans validation anti-piratage de récompense (comme le niveau Diamant) est insuffisant pour produire des spécifications formelles significatives.