L’écart entre le code correct et un programme vérifié

Les LLMs peuvent écrire du Rust qui compile et même passe cargo test. Ce qu’ils ne peuvent pas faire de manière fiable, c’est écrire une preuve formelle que le code est correct pour toutes les entrées possibles.

Le problème n’est pas la syntaxe Rust. La vérification formelle exige d’énoncer ce que vous voulez prouver, de trouver l’invariant qui fait passer la preuve, et d’exprimer les deux dans un langage que le vérificateur accepte. Les LLMs sont entraînés sur du code source, pas sur l’acte de prouver. Ils voient des théorèmes, mais ils voient rarement les vingt tentatives infructueuses qui ont précédé la preuve réussie.

Si vous collez une recherche binaire récursive dans GPT-4 et lui demandez de “prouver que c’est correct”, vous obtiendrez quelque chose qui ressemble à une preuve. Il mentionnera des invariants de boucle et des préconditions. Il utilisera probablement aussi de la syntaxe Dafny, référencera des lemmes qui n’existent pas, et affirmera des invariants trop faibles pour établir la postcondition. Ça a l’air correct jusqu’à ce que vous essayiez de le vérifier.

À quoi ressemble réellement la vérification formelle de Rust

Rust dispose de plusieurs outils de vérification. Kani est un model checker qui explore exhaustivement tous les états possibles d’une fonction jusqu’à une certaine limite. Prusti et Creusot sont des vérificateurs déductifs qui traduisent Rust en logique et demandent à un SMT solver de prouver des propriétés. Chacun nécessite des annotations dans une syntaxe spécifique.

Voici une fonction simple et à quoi ressemble une vraie preuve déductive en Creusot :

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot vérifie que la précondition a.len() > 0 garantit la postcondition result == a[0]. C’est trivial car la logique est simple. Rendons les choses plus difficiles :

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

Les invariants sont la partie difficile. Un humain les écrit en réfléchissant à ce qui reste vrai à chaque itération. Un LLM pourrait deviner s == i * (i - 1) / 2 parce que ce motif apparaît dans les données d’entraînement, ou il pourrait omettre l’invariant entièrement et laisser le solver échouer.

Ce qui se passe quand vous demandez une preuve à un LLM

J’ai testé cela avec plusieurs modèles. Le prompt était : “Écrivez une fonction Rust vérifiée qui calcule la factorielle de n en utilisant Creusot, avec des préconditions, postconditions et invariants de boucle complets.”

Les réponses se sont réparties en trois catégories.

Premièrement, certains modèles ont produit des annotations plausibles qui utilisaient une mauvaise syntaxe. Ils ont écrit #[precondition(...)] au lieu de #[requires(...)], ou ont mélangé la syntaxe Prusti avec celle de Creusot. Le code ne passait même pas le parsing.

Deuxièmement, certains modèles ont produit des annotations syntaxiquement correctes avec des invariants trop faibles. La fonction factorielle a besoin d’un invariant comme res == fact(i). Les modèles écrivaient souvent res >= i, qui est vrai mais inutile pour prouver la postcondition. Creusot signalerait qu’il ne peut pas établir l’objectif, et le LLM n’avait aucun mécanisme pour corriger cela.

Troisièmement, quelques réponses avaient l’invariant correct mais hallucinaient un lemme auxiliaire. Ils référencaient une fonction math::fact qui n’existe pas dans la bibliothèque standard de Creusot. La preuve ne fonctionne que si vous construisez vous-même cette définition logique.

Aucun des modèles n’a produit une preuve qui a passé du premier coup.

Où les LLMs aident réellement dans le workflow de vérification

Cela ne signifie pas que les LLMs sont inutiles pour la vérification formelle. Cela signifie qu’il faut les utiliser pour les bonnes tâches.

Ils sont bons pour générer le boilerplate. Étant donnée une signature de fonction, un LLM peut généralement produire les clauses #[requires] et #[ensures] qui capturent les contrats évidents. Pour une fonction fn divide(a: i32, b: i32) -> i32, il suggérera correctement #[requires(b != 0)] et #[ensures(result * b == a)]. Ce ne sont pas des idées profondes, mais elles économisent des frappes.

Ils sont passables pour expliquer les erreurs du vérificateur. Si Creusot signale “cannot prove loop invariant”, coller l’erreur dans un LLM donne souvent une explication utile de ce que l’invariant est censé faire. Il ne suggérera pas l’invariant exact dont vous avez besoin, mais il réduira l’espace de recherche.

Ils sont utiles pour traduire entre langages de vérification. Si vous avez une preuve Dafny et que vous voulez la porter vers Prusti, un LLM peut gérer une grande partie du mapping syntaxique. La logique sous-jacente est la même. C’est exactement le type de tâche de reconnaissance de motifs à laquelle les LLMs excellent.

La limitation fondamentale : prouver, c’est chercher, pas compléter

Écrire une preuve n’est pas comme écrire un serveur web. Quand vous écrivez un serveur web, il y a de nombreuses réponses correctes. Quand vous écrivez une preuve, il y a exactement une réponse, ou une petite famille de réponses, et tout le reste est faux.

Les LLMs sont des prédicteurs de token suivant. Ils génèrent la continuation la plus probable étant donné le contexte. Une étape de preuve n’est pas la continuation la plus probable. C’est l’étape qui ferme l’obligation de preuve, qui peut être la vingtième option la plus probable ou la deux-millième.

Imaginez prouver qu’une fonction de tri renvoie une permutation de son entrée. L’idée clé est généralement de définir un multiset ou de compter les occurrences. Un LLM pourrait suggérer de comparer les longueurs, ce qui est nécessaire mais pas suffisant. Il faut un humain pour reconnaître que l’égalité des longueurs n’implique pas la permutation, et pour introduire l’invariant de comptage.

Le model checking avec Kani évite une partie de cela car il ne requiert pas d’invariants. Les LLMs peuvent générer des harnesses kani::proof plus fiablement car ils ressemblent à des unit tests. Mais Kani ne fonctionne que pour une vérification bornée. Si vous avez besoin d’une preuve non bornée, vous avez toujours besoin de l’humain.

Un workflow pratique qui utilise les deux

Si vous voulez vérifier du Rust aujourd’hui, voici un workflow qui fonctionne réellement.

Commencez par écrire le code normalement. Exécutez cargo test. Puis ajoutez des contrats. Utilisez un LLM pour générer les clauses #[requires] et #[ensures] à partir de la signature de la fonction. Revoyez-les attentivement. Le modèle aura les faciles correctement et les difficiles subtilement faux.

Exécutez le vérificateur. Il échouera sur au moins une boucle. Prenez le message d’erreur et demandez au LLM d’expliquer quel invariant manque. Utilisez son explication comme point de départ, pas comme réponse. Écrivez l’invariant vous-même.

Itérez. Le vérificateur vous dira si votre invariant est assez fort. Le LLM ne le fera pas. Traitez le modèle comme un pair programmeur qui connaît la syntaxe mais n’a jamais terminé une preuve.

La réponse honnête à la question

Les LLMs peuvent-ils écrire des preuves formelles pour Rust ? Non. Pas encore. Pas sans un humain qui comprend la logique.

Ils peuvent écrire l’échafaudage, expliquer les erreurs et traduire entre outils. Mais trouver l’invariant, le lemme ou l’hypothèse d’induction qui fait passer la preuve reste une compétence humaine.

Si vous cherchez un outil qui vous permet d’éviter d’apprendre la separation logic ou les Hoare triples, un LLM ne l’est pas. Si vous cherchez un outil qui rend la courbe d’apprentissage moins raide en gérant la syntaxe et le boilerplate pendant que vous vous concentrez sur la logique, un LLM vaut le coup d’essayer.

Commencez avec Kani si vous voulez des vérifications bornées sans invariants. Passez à Creusot ou Prusti quand vous avez besoin de preuves non bornées. Utilisez le LLM pour avoir la syntaxe correcte, mais attendez-vous à écrire la preuve vous-même.

Questions fréquemment posées

Qu’est-ce que la vérification formelle en Rust ?

La vérification formelle utilise la logique mathématique pour prouver qu’un programme satisfait une spécification pour toutes les entrées possibles. En Rust, des outils comme Kani, Prusti et Creusot ajoutent des annotations aux fonctions qui décrivent les préconditions, postconditions et invariants. Un vérificateur vérifie ensuite si ces propriétés sont satisfaites.

ChatGPT peut-il écrire des preuves pour Kani ?

ChatGPT peut écrire des harnesses de preuve Kani, qui ressemblent à des unit tests avec des attributs #[kani::proof]. Ces harnesses sont plus faciles à générer que des preuves déductives car ils ne nécessitent pas d’invariants de boucle. Cependant, les harnesses complexes avec des assumptions et assertions nécessitent encore une révision humaine.

Quelle est la différence entre Kani et Creusot ?

Kani est un bounded model checker. Il explore tous les chemins d’exécution possibles jusqu’à une limite et vérifie les panics ou échecs d’assertion. Creusot est un vérificateur déductif. Il traduit Rust en formules logiques et utilise un SMT solver pour prouver des propriétés pour toutes les entrées, y compris les boucles non bornées, mais requiert des invariants fournis par l’utilisateur.

Pourquoi les LLMs peinent-ils avec les invariants de boucle ?

Les invariants de boucle nécessitent de raisonner sur ce qui reste vrai à travers les itérations, ce qui est une forme de raisonnement inductif. Les LLMs sont entraînés à prédire des continuations de texte probables, pas à chercher l’énoncé logique exact qui ferme une obligation de preuve. L’invariant correct n’est souvent pas le token suivant le plus probable.