Le génie logiciel Cleanroom exige que vous prouviez la correction de votre code avant de le compiler. Cela semble noble jusqu’à ce que vous passiez trois heures à écrire des invariants de boucle pour une fonction qui trie dix entiers.

Le goulot d’étranglement n’est pas la preuve elle-même. C’est le code répétitif. Générer des conditions de vérification, annoter des boucles avec des invariants et formater des assertions pour Dafny, Why3 ou Z3 est fastidieux, source d’erreurs et profondément peu amusant. Les LLM sont étonnamment bons à cette tâche. Ils ne sont pas bons dans la preuve réelle. Comprendre la différence est ce qui rend l’automatisation utile au lieu de dangereuse.

Pourquoi les obligations de preuve manuelles tuent la vélocité de développement

En Cleanroom, vous écrivez du code à partir de spécifications de structure en boîte, puis vous générez des conditions de vérification (VCs) pour prouver que votre implémentation correspond à la spécification. Chaque boucle a besoin d’un invariant. Chaque fonction a besoin d’une précondition et d’une postcondition. Chaque raffinement de données a besoin d’une fonction d’abstraction.

Pour une équipe qui essaie de livrer un logiciel, c’est un impôt. Un ingénieur senior peut passer 40 % de son temps sur des annotations et un échafaudage de conditions de vérification, et 60 % sur le raisonnement logique réel. L’échafaudage ne nécessite pas de discernement profond. Il nécessite de la patience et de la familiarité avec la syntaxe de votre démonstrateur.

C’est exactement le genre de tâche de reconnaissance de motifs à laquelle les LLM excellent. Ils ont vu des milliers d’invariants de boucle, de méthodes Dafny et de fichiers SMT-LIB. Ils peuvent générer des annotations syntaxiquement valides qui sont assez plausibles pour servir de point de départ.

Ce que signifie réellement « Automatiser les preuves formelles avec les LLM »

Soyons précis. Un LLM ne prouve pas que votre code est correct. Un solveur de preuves comme Z3, CVC5 ou le vérificateur Dafny prouve que votre code est correct. Le LLM automatise le travail humain qui se situe entre votre pseudocode et le solveur.

Le flux de travail ressemble à ceci :

  1. Vous écrivez l’implémentation et la spécification.
  2. Le LLM génère des annotations candidates : invariants, préconditions, postconditions, variables fantômes.
  3. Vous fournissez le code annoté au vérificateur.
  4. Le vérificateur accepte soit la preuve, la rejette avec un contre-exemple, ou dépasse le délai imparti.
  5. Si la preuve échoue, vous inspectez l’échec et demandez au LLM d’affiner l’annotation.

Le LLM est un stagiaire très rapide et très confiant qui connaît la syntaxe de chaque outil de vérification sur Internet. Il va volontiers halluciner un invariant qui semble parfait et échoue immédiatement. Ce n’est pas grave. Le solveur attrape l’hallucination. La valeur réside dans le fait d’éviter le problème de la page blanche.

Comment les LLM génèrent des annotations que les solveurs peuvent vérifier

L’astuce réside dans l’invite. Vous ne demandez pas au LLM de « prouver que cette fonction est correcte ». Vous lui demandez de produire un artefact spécifique dans un format spécifique.

Par exemple, si vous avez une fonction de type Python qui calcule la somme d’un tableau, vous interrogez le LLM comme ceci :

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

Le LLM renvoie du code Dafny avec un invariant de boucle comme forall k :: 0 <= k < i ==> arr[k] is accounted for in result. Il se peut qu’il n’obtienne pas la syntaxe exacte du premier coup. Mais il obtient la structure correcte, et cela vous fait gagner dix minutes de frappe.

Pour plus de contrôle, vous pouvez interroger directement pour du SMT-LIB. Cela est utile lorsque vous construisez des pipelines de vérification personnalisés plutôt que d’utiliser un langage de haut niveau comme Dafny.

Un exemple concret : automatiser un invariant de boucle avec Python et Z3

Voici un exemple complet et exécutable. Nous utilisons Python pour demander à un LLM (API d’OpenAI) de générer un invariant de boucle pour une simple fonction de somme de tableau, puis nous le vérifions avec Z3.

Tout d’abord, installez les dépendances :

pip install z3-solver openai

Puis exécutez le script :

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

Ce script ne vérifiera pas la fonction en une seule fois. C’est le but. Le LLM vous donne un invariant candidat. Z3 vous dit s’il est vérifié. Vous itérez.

En pratique, les équipes qui construisent des pipelines de vérification assistés par LLM encapsulent cette boucle dans un script qui renvoie les VCs échoués au LLM, analyse la nouvelle annotation, exécute le vérificateur et fournit tout message d’erreur en retour comme invite de raffinement.

Ce n’est pas une vérification entièrement autonome. C’est une vérification avec intervention humaine assistée par un assistant de frappe très rapide.

Où cela échoue : hallucinations contre erreurs réelles

Le LLM va générer des invariants qui sont trop faibles. Il oubliera de mentionner une variable dont le solveur a besoin. Il générera une syntaxe Dafny de 2019 qui ne compile plus. Il vous dira avec assurance que i <= n est suffisant alors que la boucle nécessite en réalité i < n && s == partial_sum(arr, i).

Aucune de ces erreurs n’est catastrophique. Le solveur les rejette. Vous lisez l’erreur, vous interrogez à nouveau.

Le vrai danger est l’inverse. Lorsque le LLM génère un invariant qui est trop fort, le solveur peut prouver que le programme est correct par rapport à une spécification plus stricte que celle que vous aviez l’intention. Vous pensez avoir prouvé que sum_array fonctionne pour tous les tableaux. En réalité, vous avez prouvé qu’elle fonctionne uniquement pour les tableaux où tous les éléments sont positifs, parce que le LLM a ajouté un conjoint supplémentaire qui semblait raisonnable.

Examinez toujours la spécification générée. Le LLM écrit le code répétitif. Vous possédez la logique.

Quand faire confiance à la machine, et quand faire manuellement

Utilisez l’automatisation LLM pour :

  • Échafauder les VCs pour des fonctions simples avec des préconditions et postconditions claires.
  • Traduction de syntaxe entre langages de preuve. Convertir une spécification Dafny en Why3 ou SMT-LIB est mécanique et source d’erreurs. Les LLM sont excellents à cela.
  • Génération de variables fantômes pour les preuves de raffinement de données. Le motif est répétitif.

N’utilisez pas l’automatisation LLM pour :

  • Preuves critiques pour la sécurité où un bogue de spécification subtil est pire que l’absence de preuve.
  • Logique temporelle complexe ou propriétés de vivacité. Les données d’entraînement du LLM sont plus maigres ici, et les hallucinations ont plus de chances de passer entre les mailles du filet.
  • Algorithmes nouveaux qui ne ressemblent à rien dans le corpus d’entraînement. Si vous avez inventé un nouveau protocole de consensus, le LLM n’a aucune idée des invariants dont il a besoin.

Questions fréquemment posées

Qu’est-ce qu’une condition de vérification en génie logiciel Cleanroom ?

Une condition de vérification est une formule logique générée à partir de votre code et de sa spécification. Si la formule est valide, votre code implémente correctement la spécification. En Cleanroom, elles sont généralement générées avant la compilation et levées à l’aide d’un assistant de preuve ou d’un solveur automatisé.

Les LLM peuvent-ils remplacer des assistants de preuve comme Coq ou Isabelle ?

Non. Les LLM génèrent du code et des annotations que les assistants de preuve peuvent vérifier. Ils n’effectuent pas les étapes de preuve réelles. L’assistant de preuve reste l’autorité quant à la validité d’une preuve.

Quel est le meilleur LLM pour générer des annotations de vérification formelle ?

GPT-4o et Claude 3.5 Sonnet fonctionnent tous les deux bien sur la syntaxe Dafny et SMT-LIB. Les modèles plus petits ont souvent du mal avec la syntaxe précise requise par les solveurs de preuves. Réglez la température basse (0,1–0,2) pour réduire les hallucinations créatives.

Comment empêcher un LLM de générer une spécification incorrecte ?

Vous ne le pouvez pas. Vous traitez la sortie du LLM comme un brouillon. Faites toujours passer les annotations générées par votre vérificateur. Lisez toujours les préconditions et postconditions générées pour vous assurer qu’elles correspondent à votre intention. Ne présumez jamais qu’une vérification réussie signifie que la spécification est correcte.

Commencez par les parties ennuyeuses

Si votre équipe pratique le Cleanroom ou tout travail de correction par construction, l’automatisation à plus haute valeur ajoutée n’est pas un grand démonstrateur de théorèmes IA. C’est un script qui génère vos invariants de boucle et formate votre SMT-LIB pour que vous n’ayez pas à le faire.

Choisissez les cinq motifs d’annotation les plus fastidieux de votre codebase. Écrivez un modèle d’invite pour chacun. Faites-les passer par un LLM, vérifiez la sortie, et validez ceux qui passent. C’est tout. Vous venez de récupérer 40 % de votre temps de vérification pour le coût d’un appel API.

Les preuves difficiles vous appartiennent toujours. Mais au moins, vous n’aurez pas à les taper à partir de zéro.