💻 computer science

Case Study: Saturations as Explicit Models in Equational Theories

Cet article présente une méthode pour transformer les ensembles saturés des prouveurs de théorèmes automatiques en systèmes de réécriture explicites, implémente cette construction dans Vampire et E, et l'applique à des théories équationnelles pour générer des contre-modèles infinis vérifiables.

Auteurs originaux : Mikoláš Janota, Michael Rawson, Stephan Schulz

Publié 2026-02-19

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Mikoláš Janota, Michael Rawson, Stephan Schulz

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🧩 Le Problème : La "Boîte Noire" des Mathématiciens

Imaginez que vous demandez à un super-ordinateur (un démonstrateur de théorèmes automatique) de vérifier si une règle mathématique est vraie ou fausse.

Si la règle est vraie, l'ordinateur vous dit : "C'est vrai !" et vous montre le chemin logique (la preuve) pour y arriver. C'est comme un guide touristique qui vous montre chaque étape du trajet.
Si la règle est fausse, l'ordinateur devrait normalement vous dire : "C'est faux !" et vous montrer un contre-exemple (une situation où la règle échoue).

Le problème, c'est que pour les problèmes très complexes, l'ordinateur ne trouve pas toujours un contre-exemple simple et fini. Au lieu de cela, il produit une énorme liste de déductions appelée "saturée". Pour un humain, cette liste ressemble à du charabia incompréhensible. C'est une boîte noire : on sait que la réponse est "faux" quelque part dedans, mais on ne peut pas voir pourquoi ni comment.

💡 L'Idée Géniale : Transformer le Chaos en une Carte

Les auteurs de ce papier (Mikoláš Janota, Michael Rawson et Stephan Schulz) ont eu une idée brillante : et si on pouvait lire cette "liste de déductions" comme une carte routière ?

Dans le domaine des équations (les maths qui manipulent des symboles comme $x + y = y + x$ ), ils ont découvert que cette liste confuse peut en réalité être lue comme un système de réécriture.

L'analogie du jeu de "Dessine-moi un cheval" :
Imaginez que vous avez une règle : "Si tu vois un cheval, dessine un zèbre".

Si vous avez un dessin de cheval, vous le transformez en zèbre.
Si vous avez un zèbre, vous ne faites rien.
Si vous avez un lion, vous ne faites rien.

Le papier explique comment transformer la "liste confuse" de l'ordinateur en une liste de règles claires (comme "Cheval → Zèbre"). Une fois que vous avez cette liste, vous pouvez prendre n'importe quelle phrase mathématique, l'appliquer à ces règles, et voir à quoi elle ressemble à la fin.

🌊 Le Modèle Infini : La Rivière sans Fin

Le plus fascinant, c'est que parfois, la réponse n'est pas un petit dessin fini, mais une rivière infinie.

Dans le projet mentionné (le Equational Theories Project), des mathématiciens voulaient classer des millions de règles. Pour beaucoup d'entre elles, il n'existe pas de "petit contre-exemple" (comme un tableau de 3x3). Le contre-exemple est infini.

Avant : L'ordinateur disait "C'est infini, je ne peux pas vous montrer".
Maintenant (grâce à ce papier) : L'ordinateur génère un système de règles (un "moteur") qui décrit cette infinité. C'est comme si on ne vous donnait pas une photo de l'océan, mais les lois de la physique qui expliquent comment les vagues se forment à l'infini.

🛠️ La Solution : Des Outils de Vérification

Pour que les mathématiciens aient confiance en ces nouvelles "cartes", les auteurs ont modifié deux logiciels célèbres (Vampire et E) pour qu'ils sortent ces règles de réécriture au lieu de la liste confuse.

Ils ont ensuite utilisé d'autres outils (comme des vérificateurs de code) pour s'assurer que :

Les règles ne se contredisent pas (confluence).
Le processus s'arrête toujours (termination).

Résultat : Ils ont pu vérifier 261 contre-exemples infinis qui étaient auparavant inaccessibles. C'est comme si on avait construit un pont solide sur une rivière que personne ne pouvait traverser auparavant.

📝 En Résumé

Ce papier est une boîte à outils pour traduire le langage des robots en langage humain.

Le problème : Les robots de maths savent dire "C'est faux", mais ne savent pas expliquer pourquoi quand la réponse est infinie.
La solution : Ils transforment la réponse du robot en un manuel d'instructions (un système de réécriture) que n'importe qui peut lire.
L'impact : Cela permet aux mathématiciens de comprendre pourquoi une règle échoue, même si la situation est infiniment complexe, et de vérifier que cette explication est correcte.

C'est un peu comme passer d'un message crypté illisible à un guide de voyage détaillé qui vous montre exactement où le chemin s'arrête, même si ce chemin est long à l'infini.

1. Problématique

L'article aborde un défi majeur dans le domaine de la démonstration automatique de théorèmes (ATP) : l'opacité des certificats de réfutation.

Le contexte : Les prouveurs de théorèmes basés sur la saturation (comme Vampire, E, iProver) fonctionnent en déduisant les conséquences d'un ensemble de clauses jusqu'à ce qu'une contradiction soit trouvée (réfutation) ou qu'aucune nouvelle conséquence non redondante ne puisse être déduite (saturation).
Le problème : Lorsqu'une implication ne tient pas (c'est-à-dire qu'elle est fausse), le prouveur atteint un état saturé. Cet ensemble saturé prouve théoriquement l'existence d'un modèle (contre-exemple), mais il est souvent illisible et opaque pour les humains, en particulier pour les mathématiciens qui souhaitent comprendre pourquoi une implication échoue.
La limitation actuelle : Les prouveurs peuvent générer des modèles finis via des constructeurs de modèles finis (FMB), mais de nombreuses structures algébriques nécessitent des modèles infinis pour être contredites. De plus, les modèles finis de grande taille sont souvent inaccessibles en raison de la complexité combinatoire.
L'objectif : Transformer les ensembles saturés, souvent considérés comme de simples certificats techniques, en modèles explicites et vérifiables (sous forme de systèmes de réécriture convergents), même pour des contre-modèles infinis.

2. Méthodologie

Les auteurs se concentrent sur le fragment équationnel unitaire, qui ne contient que des équations universellement quantifiées et des diséquations au sol (ground disequations). Cette restriction est puissante car elle couvre de nombreuses structures algébriques et permet d'encoder efficacement la logique du premier ordre (fragment de Horn).

La méthodologie proposée repose sur la construction d'un modèle de Herbrand explicite à partir d'un ensemble saturé :

Interprétation de la saturation : Un ensemble saturé $E$ (issu d'un calcul de complétion ou de superposition) est interprété comme un système de réécriture.
Construction du domaine : Le domaine du modèle est l'univers de Herbrand (l'ensemble de tous les termes ground construits à partir des symboles de la signature).
Fonction de normalisation : Une fonction de normalisation $\llbracket t \rrbracket$ $[[t]]$ est définie pour tout terme $t$ $t$ . Elle consiste à réécrire $t$ $t$ jusqu'à atteindre une forme normale fixe en utilisant les équations de $E$ $E$ orientées selon un ordre de termes bien fondé ( $\prec$ $≺$ ).
- Deux termes $s$ et $t$ sont considérés égaux dans le modèle si et seulement si leurs formes normales sont identiques : $s \approx t \iff \llbracket s \rrbracket = \llbracket t \rrbracket$ .
Validité du modèle :
- La diséquation d'entrée (la négation de la conjecture) est satisfaite car, si elle ne l'était pas, le prouveur aurait dérivé une contradiction (falsum).
- Les équations d'entrée sont satisfaites par construction, car la complétion non défaillante (unfailing completion) garantit que les équations initiales sont préservées et que le système est confluent sur les termes ground.
Implémentation : Les auteurs ont modifié les prouveurs Vampire et E pour extraire et imprimer ces systèmes de réécriture à la fin de la saturation, à condition que les équations soient "pré-ordonnées" (c'est-à-dire que le membre gauche soit strictement plus grand que le membre droit selon l'ordre interne du prouveur).

3. Contributions Clés

Théorique : Une exposition complète et accessible de la manière dont les ensembles saturés dans le fragment équationnel unitaire définissent des modèles explicites (potentiellement infinis) via des systèmes de réécriture convergents.
Pratique : L'implémentation de cette extraction dans deux prouveurs majeurs (Vampire et E).
Vérification : L'intégration d'une chaîne de vérification formelle. Les systèmes de réécriture générés sont soumis à des outils certifiés :
- CSI pour vérifier la confluence (ground confluence).
- TTT2 pour vérifier la terminaison.
- CeTA pour vérifier les certificats produits par CSI et TTT2 (basé sur la bibliothèque Isabelle/IsaFoR).
Application au projet ETP : Application de cette méthode au Equational Theories Project (ETP), un projet collaboratif visant à classifier des millions d'implications entre égalités.

4. Résultats

Les auteurs ont appliqué leur méthode aux problèmes non résolus par les constructeurs de modèles finis dans le cadre de l'ETP :

Données d'entrée : Sur 22 millions d'implications, 304 problèmes ont été réfutés uniquement par saturation (sans modèle fini trouvé par FMB).
Filtrage : Parmi ces 304, 196 sont marqués comme "finitement insatisfiables" par l'outil Infinox, ce qui signifie qu'ils n'ont aucun contre-modèle fini. Les 108 restants pourraient avoir des modèles finis, mais ceux-ci n'ont pas été trouvés.
Extraction : Sur les 304 saturations d'intérêt, 261 étaient déjà "pré-ordonnées" (les équations respectaient l'ordre interne), permettant une extraction directe du système de réécriture.
Vérification : Les 261 systèmes de réécriture extraits ont été tous certifiés comme confluents et terminants par les outils CSI et TTT2.
Exemple concret : L'article détaille la réfutation d'une implication spécifique (entre les équations 118 et 274 de l'ETP) qui admet uniquement des modèles infinis. Le système de réécriture généré (Fig. 1) fournit un contre-exemple explicite et vérifiable.

5. Signification et Impact

Transparence et Confiance : Cette approche transforme les "boîtes noires" des prouveurs de théorèmes en certificats explicites. Les mathématiciens peuvent désormais inspecter, comprendre et vérifier pourquoi une implication échoue, même dans le cas de modèles infinis.
Fiabilité : En déléguant la vérification de la confluence et de la terminaison à des outils certifiés (CeTA/Isabelle), les auteurs garantissent que les contre-modèles générés sont mathématiquement corrects, réduisant ainsi le risque d'erreurs logicielles dans les prouveurs ATP.
Complémentarité : La méthode comble le vide laissé par les constructeurs de modèles finis, permettant de traiter des problèmes algébriques complexes qui nécessitent intrinsèquement des structures infinies.
Perspectives futures : Les auteurs envisagent d'étendre cette approche au-delà du fragment équationnel unitaire (vers la logique de Horn ou la logique du premier ordre complète) et d'explorer la construction de modèles finis explicites à partir de systèmes de réécriture convergents.

En résumé, cet article démontre que la saturation n'est pas seulement une étape intermédiaire vers une preuve, mais peut être directement interprétée comme un modèle mathématique robuste et vérifiable, renforçant ainsi la collaboration entre l'automatisation et la recherche mathématique humaine.