Constraint Learning for Non-confluent Proof Search

Cet article présente une méthode d'apprentissage de contraintes appliquée au calcul des connexions en logique du premier ordre, permettant de réduire considérablement le retour en arrière dans la recherche de preuves tout en préservant la complétude.

L'essentiel

🕵️‍♂️ Le Dilemme du Détective : Comment éviter de tourner en rond ?

Imaginez que vous êtes un détective privé (un ordinateur) chargé de résoudre une énigme complexe : prouver qu'une affirmation est vraie ou fausse en utilisant un ensemble de règles logiques.

Pour ce faire, vous utilisez une méthode appelée "Tableau de Connexion". C'est comme si vous dessiniez un arbre de décisions géant. Vous partez d'un point, vous faites des choix (par exemple : "Si A est vrai, alors je vais par là"), et vous continuez à creuser jusqu'à trouver une contradiction ou une preuve.

🚧 Le Problème : Le "Mur" et le Retour en Arrière (Backtracking)

Le problème avec cette méthode, c'est qu'elle n'est pas toujours fluide. Parfois, vous faites un choix, vous avancez de 100 mètres, et soudain... BOUM ! Vous vous rendez compte que c'est une impasse. Vous ne pouvez plus avancer.

Dans ce cas, vous devez faire un retour en arrière (ce qu'on appelle le backtracking). Vous effacez vos pas, vous revenez au dernier carrefour, et vous essayez un autre chemin.

Le souci, c'est que dans les systèmes logiques complexes, vous pouvez vous retrouver à faire des milliers de retours en arrière inutiles. C'est comme si vous cherchiez une clé dans une maison, que vous ouvriez chaque tiroir, que vous vous rendiez compte qu'il n'y a rien, puis que vous fermiez le tiroir, reveniez à la porte, et recommenciez exactement la même chose, encore et encore, sans jamais apprendre de vos erreurs. C'est épuisant et inefficace.

💡 La Solution Apprise : Le "Carnet de Notes" (Constraint Learning)

C'est ici que les auteurs de ce papier, Michael Rawson et ses collègues, apportent une idée géniale : l'apprentissage par contraintes.

Au lieu de simplement rebrousser chemin quand vous tombez sur un mur, vous prenez un carnet de notes (une base de données de contraintes). Vous analysez pourquoi vous êtes bloqué.

• L'analogie du détective :
  Imaginez que vous avez essayé d'ouvrir une porte avec une clé A, mais elle ne rentre pas parce que la serrure est cassée.

  • Sans apprentissage : Vous retournez au carrefour, essayez la clé B, puis C, puis D... et à chaque fois, vous vous souvenez que la porte est fermée, mais vous ne savez pas pourquoi. Vous continuez à essayer des clés au hasard.
  • Avec apprentissage : Quand vous tombez sur le mur, vous écrivez dans votre carnet : "Attention ! Si j'utilise la clé A et que je suis dans le couloir de gauche, cette porte est bloquée pour toujours."

  La prochaine fois que vous arrivez à ce carrefour, vous regardez votre carnet. Vous voyez l'avertissement. Vous savez immédiatement : "Ah non, pas cette combinaison !" et vous évitez de perdre du temps à essayer.

🧩 Comment ça marche techniquement (sans les maths) ?

1. Le Blocage : L'ordinateur construit son arbre de preuves. Il arrive à un point où aucune règle ne s'applique. C'est un "tableau bloqué".
2. L'Analyse : Au lieu de juste dire "Échec", le système regarde en arrière. Il se demande : "Quels sont les choix précis que j'ai faits pour arriver ici ?" (Par exemple : "J'ai choisi la règle X, et j'ai lié la variable Y au terme Z").
3. L'Enseignement : Il crée une règle d'interdiction (une contrainte). Par exemple : "Ne jamais faire le choix X si la variable Y est liée à Z".
4. Le Saut en Arrière (Backjumping) : Au lieu de revenir d'un seul pas en arrière, le système peut sauter plusieurs pas en arrière d'un coup, car il sait que tous les chemins intermédiaires sont condamnés par sa nouvelle règle.

🏆 Les Résultats : Moins de pas, plus de vitesse

Les auteurs ont créé un prototype appelé hopCoP pour tester cette idée. Ils l'ont comparé à un autre système célèbre, meanCoP, qui utilise des astuces pour limiter les retours en arrière, mais qui est parfois incomplet (il rate des preuves).

• Le verdict : hopCoP, grâce à son "carnet de notes", a prouvé beaucoup plus d'énigmes en 10 secondes que les autres systèmes.
• Le secret : Il fait beaucoup moins de "pas inutiles". Il explore moins de chemins, mais il explore les bons. C'est comme un randonneur qui a une carte des zones dangereuses : il ne marche pas au hasard, il contourne les marais dès le début.

🚀 En résumé

Ce papier nous dit que pour résoudre des problèmes logiques complexes, se souvenir de ses échecs est aussi important que de réussir. En apprenant des raisons pour lesquelles un chemin est bloqué, l'ordinateur devient plus intelligent, évite de tourner en rond, et trouve la solution beaucoup plus vite.

C'est un peu comme passer d'un détective qui cherche au hasard avec un marteau, à un détective qui utilise un manuel de déduction pour éviter les pièges qu'il a déjà rencontrés ! 🕵️‍♀️📝✨

Résumé technique

Voici un résumé technique détaillé de l'article « Constraint Learning for Non-Confluent Proof Search » (Apprentissage de contraintes pour la recherche de preuves non confluentes) par Michael Rawson, Clemens Eisenhofer et Laura Kovács.

1. Problématique

La recherche de preuves dans les calculs de tableaux non confluentes, tels que le calcul de tableaux de connexion (connection tableau calculus), souffre d'un problème majeur : un retour en arrière (backtracking) excessif.

• Nature du problème : Dans ces calculs, le choix d'une extension de tableau peut bloquer la fermeture d'autres branches plus tard, obligeant le système à revenir en arrière pour essayer une autre voie. Contrairement aux calculs confluents (comme la superposition), le non-confluent exige de considérer des alternatives, ce qui peut mener à une explosion combinatoire.
• Limites des approches actuelles : Les méthodes existantes pour réduire ce retour en arrière, comme l'utilisation de coupes (cuts) dans le système leanCoP, améliorent les performances mais sacrifient la complétude (le système peut échouer à trouver une preuve même si elle existe). Les approches qui conservent la complétude souffrent souvent d'un retour en arrière pathologique, où le système tente de fermer les mêmes objectifs en boucle sans changer la cause racine de l'échec.

2. Méthodologie

Les auteurs proposent d'adapter une technique issue de la satisfaction de contraintes (CSP) et de la logique propositionnelle (SAT), connue sous le nom d'apprentissage de contraintes (Constraint Learning), au contexte de la logique du premier ordre via les tableaux de connexion.

A. Concept Central : Apprentissage de Contraintes

L'idée est d'analyser les points morts (dead ends) rencontrés lors de la recherche. Lorsqu'un tableau est « bloqué » (aucune inférence n'est possible), le système :

1. Identifie la cause du blocage (un sous-ensemble des décisions précédentes qui a rendu l'inférence impossible).
2. Génère une clause de contrainte (un ensemble d'atomes) qui interdit de reproduire cette configuration spécifique.
3. Ajoute cette contrainte à une base de données pour guider la recherche future et éviter de rejouer les mêmes échecs.

B. Langage de Contraintes

Les auteurs définissent un langage pour expriquer ces contraintes :

• Version initiale (Simplifiée) : Basée sur les règles d'inférence (démarrage, réduction, extension). Une contrainte est un ensemble d'atomes représentant les étapes nécessaires pour atteindre un état bloqué.
• Version raffinée (Section 5) : Pour améliorer l'efficacité et la généralité, le langage est décomposé en atomes plus fins :
  • Placement de littéraux à des positions spécifiques ($L@p$).
  • Liaison de variables à des termes ($x \mapsto t$).
  • Atomes de non-connexion : Pour éviter de trop spécialiser les contraintes, ils introduisent des atomes indiquant qu'aucune connexion n'est possible entre deux positions ($p \not\sim q$), indépendamment de la substitution.
  • Disséquations : Support pour les inégalités ($s \neq t$) afin de gérer des raffinements classiques comme la régularité.

C. Algorithme de Recherche (Algorithm 1)

L'algorithme maintient une piste (trail) d'atomes vrais pour le tableau courant.

1. Il sélectionne une branche ouverte et tente des inférences.
2. Si une inférence échoue (soit par impossibilité calculatoire, soit par violation d'une contrainte apprise), il calcule la raison de l'échec.
3. Si toutes les inférences sur une branche échouent, une nouvelle contrainte est apprise.
4. Le système effectue un backjumping (retour en arrière sautant plusieurs niveaux) jusqu'à ce qu'une contrainte violée soit rétablie, permettant de changer de décision.
5. L'algorithme garantit la complétude à une profondeur donnée : s'il apprend la contrainte vide (ou épuise l'espace de recherche), il conclut qu'aucune preuve n'existe à cette profondeur.

3. Contributions Clés

• Preuve de Complétude : Contrairement aux méthodes de coupes (cuts), cette approche préserve la complétude du calcul de tableaux de connexion tout en réduisant le retour en arrière.
• Cadre Théorique pour le Non-Confluent : Ils formalisent comment l'apprentissage de contraintes peut être appliqué à des calculs non confluent, en définissant précisément ce qu'est une « raison » d'échec d'inférence.
• Langage de Contraintes Adapté : Développement d'un langage capable d'expliquer non seulement pourquoi un tableau est bloqué, mais aussi pourquoi une inférence spécifique est impossible, en tenant compte des substitutions globales.
• Implémentation (hopCoP) : Création d'un prototype (hopCoP) basé sur meanCoP (un système de référence) intégrant cet apprentissage de contraintes.

4. Résultats Expérimentaux

Les auteurs ont comparé hopCoP (avec apprentissage de contraintes) contre meanCoP (avec coupes mais incomplet) et !meanCoP (avec coupes agressives).

• Réduction du Backtracking : Sur le problème PUZ005-1, hopCoP a effectué considérablement moins d'étapes d'extension pour explorer les niveaux de profondeur élevés que meanCoP. Par exemple, à la profondeur 7, meanCoP a tenté plus de 6 millions d'étapes, contre environ 48 000 pour hopCoP.
• Performance Globale : Sur plusieurs ensembles de benchmarks (TPTP, MPTP, Miz40), hopCoP a résolu plus de problèmes dans un délai de 10 secondes que les deux variantes de meanCoP.
  • Sur l'ensemble M2k : hopCoP (1050) > !meanCoP (878) > meanCoP (795).
  • Sur l'ensemble Miz40 : hopCoP (13 040) > !meanCoP (9 748) > meanCoP (7 592).
• Conclusion : La réduction du retour en arrière compense largement la surcharge computationnelle liée à la gestion des contraintes et à la détection de conflits.

5. Signification et Perspectives

• Impact Théorique : Ce travail démontre que les techniques avancées de résolution de problèmes SAT/SMT (comme l'apprentissage de clauses et le backjumping) peuvent être transposées avec succès à la logique du premier ordre non confluente, comblant le fossé entre l'efficacité pratique et la complétude théorique.
• Applications : La méthode est particulièrement pertinente pour les prouveurs interactifs de théorèmes (où il y a beaucoup d'axiomes non pertinents) et pour l'intégration de l'apprentissage automatique dans la preuve de théorèmes.
• Limites et Futur :
  • L'utilisation de la mémoire pour stocker les contraintes est le principal compromis (trade-off), bien que jugée acceptable.
  • Les auteurs suggèrent que l'élimination des positions explicites dans le langage de contraintes (pour gérer l'équivalence structurelle) serait une amélioration future majeure.
  • Une synergie potentielle est identifiée entre l'apprentissage de contraintes (pour réduire l'espace de recherche) et l'apprentissage automatique (pour guider les heuristiques).

En résumé, cet article propose une avancée significative pour les prouveurs de théorèmes basés sur les tableaux, transformant un processus de recherche souvent inefficace en une méthode robuste, complète et performante grâce à l'apprentissage dynamique de contraintes.