Imaginez un correcteur qui ne comprend rien à ce qu'il lit, mais qui vérifie que chaque phrase découle bien des précédentes selon des règles écrites à l'avance. Il ne peut pas juger si le raisonnement est intéressant, ni s'il répond à la bonne question. Il peut garantir qu'il n'y a pas de trou. C'est exactement ce qu'est un assistant de preuve, et c'est beaucoup plus utile qu'il n'y paraît.
Nous rapportions ce matin une preuve mathématique obtenue avec des modèles et vérifiée formellement. Voici comment ça marche.
Le principe
Une démonstration écrite en langage naturel comporte toujours des raccourcis : « on voit facilement que », « le cas suivant est analogue », « par un argument standard ». Ces raccourcis sont utiles entre spécialistes, et c'est là que se cachent la plupart des erreurs.
La vérification formelle supprime ces raccourcis. On réécrit la démonstration dans un langage où chaque étape doit être justifiée explicitement, en s'appuyant sur des règles logiques et sur des résultats déjà établis.
Un programme parcourt ensuite l'ensemble et vérifie mécaniquement que chaque déduction est valide. S'il accepte, la preuve est correcte au sens strict. S'il refuse, il indique où ça coince.
Pourquoi faire confiance au vérificateur
La question naturelle est : pourquoi croire ce programme plutôt que la preuve ?
La réponse tient à une propriété d'architecture. Ces systèmes sont conçus autour d'un noyau minimal : quelques centaines de lignes de code qui implémentent les règles logiques de base. Tout le reste du système, qui est énorme, doit passer par ce noyau pour valider quoi que ce soit.
Donc pour faire confiance à l'ensemble, il suffit de faire confiance à ce petit noyau. Il est relativement simple, il a été audité par de nombreuses personnes, et il n'a pas changé depuis des années.
C'est le déplacement que nous décrivions dans notre article sur la confiance : on ne comprend pas l'objet, on comprend le dispositif qui l'a contrôlé.
L'énoncé n'est pas vérifié. Le système garantit que la démonstration prouve ce qui est écrit. Si l'énoncé formalisé ne correspond pas à la question qu'on voulait poser, la preuve est parfaitement valide et sans objet. C'est l'erreur la plus courante, et elle demande une relecture humaine de l'énoncé seul — ce qui est court.
L'intérêt n'est pas jugé. Un vérificateur accepte une démonstration triviale aussi volontiers qu'un résultat majeur.
Le coût reste élevé. Formaliser une preuve prend beaucoup plus de temps que l'écrire. C'est ce qui a longtemps limité cette pratique, et c'est précisément ce que les modèles changent.
Pourquoi ça devient central maintenant
Deux mouvements convergent.
Les modèles produisent du volume. Ils peuvent proposer des dizaines de pistes, tenter des constructions, produire des démonstrations. Le goulot d'étranglement se déplace de la production vers la vérification.
Les modèles rendent la formalisation moins coûteuse. Traduire une preuve en langage formel est un travail fastidieux, répétitif, où l'erreur se voit immédiatement puisque le vérificateur refuse. C'est exactement le profil de tâche que nous décrivions comme automatisable dans notre article sur ce qui mérite de l'être.
La combinaison est vertueuse : le modèle propose et formalise, le vérificateur garantit. Le défaut principal du modèle — produire du plausible avec assurance — est neutralisé par un dispositif qui ne se laisse pas convaincre.
Au-delà des mathématiques
Cette approche s'applique déjà ailleurs, et c'est peu connu.
Des composants critiques de logiciels de transport, d'aéronautique ou de cryptographie sont vérifiés formellement : on démontre que le programme fait exactement ce que sa spécification décrit, plutôt que de le tester sur des cas.
C'est une piste intéressante pour le code produit par des modèles. Nous relevions à propos du code scientifique modernisé que le danger vient des programmes qui tournent parfaitement en produisant un résultat faux. Un dispositif de vérification supprimerait cette classe d'erreurs — pour les propriétés qu'on a pensé à spécifier.
Ce qu'il faut retenir
La vérification formelle n'est pas une technologie d'IA, et elle est en train de devenir son complément le plus utile.
Elle propose une réponse concrète à la question que nous posons sans arrêt : comment utiliser un système qui a raison souvent et tort parfois, sans pouvoir distinguer les deux cas ? La réponse n'est pas de mieux faire confiance, c'est de ne pas avoir à le faire.
Ce principe dépasse largement les mathématiques. Partout où l'on peut définir mécaniquement ce qu'est un résultat correct, on peut laisser un modèle produire beaucoup et faire trier par un vérificateur. Là où l'on ne peut pas le définir — le jugement, le goût, la pertinence — il faudra continuer à lire.