💻 computer science

Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

Cet article présente une dérivation entièrement automatique d'un algorithme d'unification à trois arguments utilisant la synthèse de programmes déductive, généralisant et automatisant une preuve manuelle de Manna et Waldinger pour générer un programme correct qui calcule les unificateurs idempotents les plus généraux par rapport à une substitution d'environnement accumulée.

Auteurs originaux : Richard Waldinger

Publié 2026-07-27✓ Author reviewed ⓘ

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Richard Waldinger

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 par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le guide du détective pour faire correspondre les choses

Imaginez que vous êtes un détective essayant de résoudre un mystère où deux descriptions différentes d'une scène de crime doivent en réalité correspondre au même événement. Un témoin dit : « Le suspect portait un chapeau rouge et un manteau bleu », tandis qu'un autre dit : « Le suspect portait un chapeau rouge et un manteau bleu ». Facile, n'est-ce pas ? Mais que se passe-t-il si le second témoin dit : « Le suspect portait un chapeau rouge et un manteau bleu, mais le chapeau était en fait un déguisement pour un manteau bleu » ? Vous devez maintenant déterminer si ces deux récits peuvent correspondre en remplaçant les « variables » (comme les couleurs ou les objets spécifiques) par les bonnes valeurs. Dans le monde de l'informatique, ce casse-tête s'appelle l'unification. C'est le moteur qui alimente tout, de l'intelligence artificielle qui joue aux échecs aux logiciels qui vérifient si votre code est correctement écrit.

Pendant des décennies, les informaticiens ont tenté d'apprendre aux machines à résoudre ce casse-tête automatiquement. L'objectif n'est pas seulement d'obtenir que l'ordinateur dise « oui, ils correspondent », mais de faire en sorte que l'ordinateur invente la recette étape par étape (l'algorithme) pour les faire correspondre. C'est un domaine appelé la synthèse de programmes déductive. Considérez cela comme demander à un robot super intelligent de prouver un théorème mathématique, mais au lieu de simplement écrire « Q.E.D. » à la fin, le robot doit vous remettre un logiciel fonctionnel qui résout le problème. Le piège ? Le robot doit être absolument certain que le logiciel est correct car la preuve est la garantie. Si la preuve tient, le programme fonctionne. Si la preuve échoue, le programme est bon pour la poubelle.

La grande découverte du papier : Enseigner à un robot à construire son propre solveur de casse-têtes

Ce papier, écrit par Richard Waldinger, est l'histoire d'un robot nommé Snark à qui l'on a demandé de construire un algorithme d'unification à partir de zéro, en utilisant uniquement les règles de la logique. L'auteur ne s'est pas contenté de donner la réponse à Snark ; il lui a donné un ensemble de règles logiques (une « théorie axiomatique ») et un objectif : « Trouver une substitution qui rend ces deux expressions identiques. »

La principale conclusion du papier est que Snark a réussi à dériver automatiquement un algorithme d'unification fonctionnel. Il n'a pas simplement copié un ancien algorithme ; il a découvert une nouvelle version qui est en fait plus efficace et plus facile à comprendre que certaines tentatives manuelles précédentes. Le robot a fait cela en traitant la création du programme comme un immense puzzle logique. Il est parti d'un objectif vague et, par un processus de décomposition du problème en cas plus petits (comme « Et si le premier élément est une constante ? » ou « Et si c'est une variable ? »), il a construit un arbre de décision complexe de type « si-alors-sinon ». Cet arbre est le programme final.

Le papier exclut explicitement l'idée qu'il s'agissait d'un simple tour en une seule étape. L'auteur admet que le processus a nécessité beaucoup d'« aide humaine » sous la forme de la mise en place des bonnes règles logiques et du choix des bons « rapports bien fondés » (une façon sophistiquée de dire « des règles qui garantissent que le robot ne restera pas bloqué dans une boucle infinie »). Le papier argumente également contre l'idée que l'unification soit une question simple et directe. Comme le note une citation dans le papier, « lorsqu'une présentation approfondie est tentée, on réalise alors que la question est assez subtile et traîtresse. » Le papier ne prétend pas que cela résout tous les problèmes de synthèse de programmes ou que c'est un remède miracle pour tout le génie logiciel. Au contraire, il présente cela comme une étude de cas réussie prouvant que la dérivation entièrement automatique d'algorithmes complexes est possible, même si cela reste un objectif de recherche pour de nombreux autres types de programmes.

Comment le robot a « pensé »

Pour comprendre comment Snark a procédé, imaginez que vous essayez d'apprendre à un enfant à trier un tas de jouets en désordre. Vous ne dites pas simplement « trie-les ». Vous lui donnez un ensemble de règles : « Si c'est un bloc, mets-le dans le bac rouge. Si c'est une voiture, mets-la dans le bac bleu. » Mais que se passe-t-il si le jouet est à la fois un bloc et une voiture ? Vous avez besoin d'une règle pour cela aussi.

Snark a utilisé une méthode appelée tableaux déductifs. Imaginez un tableau blanc avec deux colonces : « Ce que nous savons » (Assertions) et « Ce que nous devons trouver » (Objectifs).

L'Objectif : « Trouver un moyen de faire en sorte que l'Expression A et l'Expression B se ressemblent. »
Le Processus : Snark regarde l'objectif et se demande : « Et si A est une variable ? Et si c'est une constante ? » Il divise le problème en ces différents « cas ».
Le Moment « Eurêka ! » : Quand Snark réalise que pour résoudre un grand problème, il pourrait avoir besoin de résoudre une version plus petite du même problème d'abord, il introduit la récursion. C'est comme dire : « Pour trier ce grand tas, je vais d'abord trier la moitié gauche, puis la moitié droite, et enfin combiner les deux. » Le papier explique que Snark a dû être très prudent ici pour s'assurer qu'il ne trierait pas éternellement. Il a utilisé un « rapport bien fondé » (une garantie mathématique que chaque étape rend le problème strictement plus petit, comme compter de 100 à 0) pour prouver que le processus finirait par s'arrêter.

L'astuce de l'« Environnement »

L'un des mouvements les plus astucieux du papier fut de modifier légèrement le problème pour le rendre plus facile à résoudre pour le robot. Au lieu de simplement demander « Comment faire correspondre A et B ? », on a demandé à Snark : « Comment faire correspondre A et B étant donné que vous avez déjà une liste de correspondances de la part de l'étape précédente ? » Cette liste est appelée un environnement.

Voyez cela comme une partie de « Jacques a dit ». Si Jacques dit « Touche ton nez », vous le faites. Mais si Jacques dit « Touche ton nez » après avoir déjà dit « Porte un chapeau », vous devez vous souvenir du chapeau et toucher votre nez. En gardant une trace de l'« environnement » (le chapeau), le robot a pu construire un algorithme plus efficace. Le papier suggère que cette version à trois arguments (Expression A, Expression B et l'Environnement) est en fait plus facile à synthétiser automatiquement pour un ordinateur que la version plus simple à deux arguments que les humains utilisent habituellement.

Le Résultat Final : Une Nouvelle Recette

Le papier conclut en montant le code réel produit par Snark. Il ressemble à une longue liste d'instructions « si ceci, alors cela ».

Si l'environnement est brisé, renvoyer un signal de « l'échec ».
Si les deux expressions sont déjà identiques, renvoyer la liste actuelle des correspondances.
Si l'un est une variable et l'autre une constante, créer une nouvelle règle pour les échanger.
Si les deux sont des structures complexes (comme une liste d'éléments), les diviser en leurs parties gauche et droite, résoudre la partie gauche d'abord, puis utiliser ce résultat pour résoudre la partie droite.

Le papier souligne que ce programme est prouvablement correct. Parce que le programme a été extrait directement d'une preuve logique, nous savons qu'il fonctionne. Si la preuve dit « cette étape est valide », alors l'étape de code est valide. L'auteur note que bien que la preuve ait pris environ 10 secondes au système Snark pour la trouver, la véritable valeur réside dans la méthode : elle montre que nous pouvons construire des logiciels en prouvant des théorèmes, plutôt qu'en devinant et en testant.

Pourquoi cela importe (Et pourquoi ce n'est pas encore de la magie)

Le papier se termine par un clin d'œil ludique vers l'avenir. Il mentionne que si l'IA moderne (comme les grands modèles de langage) peut écrire du code, elle peut parfois « halluciner » ou inventer des faits. Elle peut écrire un programme qui semble correct mais qui contient un bug caché. La synthèse déductive, en revanche, est comme une preuve mathématique : si les étapes sont justes, le résultat doit être juste.

L'auteur suggère un avenir où nous pourrions combiner ces deux mondes : utiliser une IA intelligente pour aider à configurer les règles logiques et les « suppositions » de la preuve, puis utiliser un prouveur de théorèmes rigoureux pour vérifier le résultat final. Mais pour l'instant, le papier témoigne de la puissance de la logique : une machine a été capable d'examiner un problème complexe et délicat et, étape par étape, d'inventer sa propre solution, prouvant que le chemin vers un logiciel parfait pourrait bien être un chemin de mathématiques pures.

Résumé technique : Automatisation de la dérivation d'algorithmes d'unification

Énoncé du problème
L'algorithme d'unification est un composant fondamental du raisonnement automatisé, de la programmation logique et du contrôle de type. Bien que l'unification soit souvent traitée comme un concept simple, sa mise en œuvre rigoureuse est subtile et sujette à l'erreur ; l'article note que même les algorithmes présents dans des manuels et des systèmes de raisonnement largement utilisés ont été jugés incorrects. Bien que la synthèse de programmes déductive — la construction automatique de programmes à partir de spécifications logiques via la démonstration de théorèmes — soit un objectif de recherche depuis les années 1960, la dérivation entièrement automatique d'un algorithme d'unification complet est restée insaisissable. Les tentatives précédentes, telles que la dérivation manuelle par Manna et Waldinger (1981), nécessitaient une intuition humaine significative pour guider la preuve. Le défi réside dans l'automatisation de la découverte des spécifications nécessaires, des relations bien fondées appropriées pour la terminaison, et de la structure récursive de l'algorithme sans intervention humaine.

Méthodologie
L'article emploie la synthèse de programmes déductive en utilisant le prouveur de théorèmes par résolution du premier ordre Snark. La méthodologie traite la construction de programmes comme une tâche de démonstration de théorèmes :

Théorie du domaine sujet : Une théorie axiomatique formelle des expressions symboliques (modélisée sur les S-expressions de Lisp) et des substitutions est définie. Cette théorie inclut des définitions pour les atomes, les conses, les variables, les constantes et les opérations telles que l'application de substitution, la composition et le remplacement. Crucialement, la théorie définit des relations telles que « l'unificateur le plus général idempotent » (mgi) et la « réduction » pour garantir que l'algorithme résultant est efficace et se termine.
Spécification : L'objectif est de synthétiser un programme unify(θ0, e1, e2) qui trouve une substitution $\Theta$ qui est un unificateur réduisant, idempotent et le plus général (mgi) des expressions $e_1$ et $e_2$ par rapport à une substitution d'environnement $\theta_0$ . La spécification est renforcée pour exiger que l'unificateur soit une extension de l'environnement et une réduction (maintenant ou réduisant les ensembles de variables), ce qui simplifie la preuve de terminaison.
Tableaux déductifs : La preuve est menée à l'aide d'une structure de tableau déductif. Cette structure maintient un ensemble d'assertions (vérités connues) et de buts (conditions à satisfaire). La preuve progresse en appliquant des règles d'inférence :
- Résolution et remplacement d'équivalence : Ces règles effectuent une analyse de cas, introduisant des structures conditionnelles (if-then-else) dans la sortie du programme.
- Induction mathématique : L'induction bien fondée est appliquée pour introduire la récursion. Le système doit découvrir une relation bien fondée qui garantit la terminaation.
Stratégie d'automatisation : Le prouveur Snark recherche une preuve de la spécification. La structure de la preuve correspond directement à la structure du programme extrait. Les auteurs notent que, bien que la dérivation de la relation bien fondée (la « relation u ») ait nécessité une étape de « eureka » manuelle dans ce cas précis, le reste de la dérivation a été automatisé.

Contributions clés

Dérivation entièrement automatique : L'article présente une dérivation entièrement automatique d'un algorithme d'unification pour les expressions symboliques, extraite d'une preuve générée par le prouveur de théorèmes Snark. Cela contraste avec les travaux précédents où l'algorithme était dérivé manuellement ou vérifié de manière semi-automatique.
Structure d'algorithme novatrice : L'algorithme extrait est une version à trois arguments (prenant une substitution d'environnement) qui est plus efficace que la version à deux arguments de Manna et Waldinger (1981). Il incorpore une substitution d'« environnement » qui accumule les remplacements lors des appels récursifs, un motif courant dans les implémentations pratiques mais difficile à synthétiser automatiquement à partir d'une simple spécification à deux arguments.
Découverte de la structure récursive : Le système a découvert automatiquement la nécessité d'appels récursifs imbriqués. Spécifiquement, pour les expressions non atomiques, l'algorithme unifie d'abord les composants gauches, produisant une substitution intermédiaire, qui est ensuite utilisée comme environnement pour unifier les composants droits. Cette structure a émergé naturellement de l'application de l'hypothèse d'induction et des propriétés des relations définies.
Gestion des cas limites : La dérivation gère automatiquement les cas complexes, incluant :
- Le test d'occurrence (occurs check) (détecter quand une expression est une sous-expression propre d'une autre).
- Les conditions d'échec (constantes distinctes, atomes incompatibles).
- Le renommage de variables et la mise à part (standardization apart).
- Les propriétés d'idempotence et de réduction, garantissant que la sortie est un unificateur le plus général valide.

Résultats
Le prouveur de théorèmes Snark a généré avec succès une preuve de la spécification en environ 10 secondes (sur le matériel disponible au moment du travail original, bien que l'article soit daté de 2026). À partir de cette preuve, un programme applicatif (sans effet de bord) correct a été extrait. Le programme résultant :

Unifie correctement deux expressions par rapport à un environnement.
Produit le symbole « bas » $\bot$ si l'unification est impossible.
Produit un unificateur réduisant, idempotent et le plus général.
Contient des éléments novateurs découverts par le prouveur, tels que l'ordre spécifique des vérifications (par exemple, vérifier les substitutions propres avant le test d'occurrence, selon l'ordre des symboles).
Les auteurs notent qu'en modifiant les poids d'ordre des symboles dans Snark, différents algorithmes d'unification valides peuvent être synthétisés, démontant la flexibilité de l'approche.

Signification et affirmations
L'article positionne ce travail comme un cas d'étude significatif de la synthèse de programmes déductive. Sa principale importance ne réside pas dans la nouveauté de l'algorithme d'unification lui-même (qui est un concept connu), mais dans le processus de sa dérivation automatique.

Preuve de concept : Il démontre qu'un prouveur de résolution moderne peut synthétiser un algorithme récursif non trivial avec des arguments de terminaison complexes et une logique conditionnelle à partir d'une spécification déclarative.
Correctitude et explication : Le programme extrait est garanti correct par rapport à la spécification car sa validité est soutenue par la preuve dont il a été extrait. La preuve sert également d'explication au raisonnement de l'algorithme.
Directions futures : Les auteurs suggèrent que cette approche pourrait être étendue pour synthétiser automatiquement des algorithmes d'unification spécifiques à une théorie (par exemple, l'unification associative-commutative), remplaçant potentiellement le raisonnement lourd en axiomes par du code synthétisé efficace au milieu de la preuve.
Limites : L'article reconnaît modestement que la découverte de la relation bien fondée spécifique (la « relation u ») a nécessité une étape manuelle (« Deus ex Machina ») et que la dérivation automatique de telles relations demeure un objectif de recherche. Ils notent également que le corps de connaissances (lemmes et axiomes) requis pour la dérivation était vaste et laborieux à assembler.

L'article conclut en contrastant la synthèse déductive avec les modèles de langage de grande taille (LLM). Bien que les LLM puissent récupérer des algorithmes connus, ils manquent de la justification rigoureuse et de la garantie de correction fournies par les méthodes déductives. Les auteurs proposent une synergie potentielle où les LLM aident à formuler les spécifications ou à sélectionner les paramètres du prouveur de théorèmes, tandis que les prouveurs déductifs assurent la validité logique des programmes résultants.