Avant de demander à une IA de réfléchir, essayez d'abord de nettoyer son entrée

Une formule logique et une requête de raisonnement ne sont pas la même chose, mais dans de nombreux pipelines d'IA, elles voyagent ensemble : une base de connaissances exprimée sous forme normale conjonctive (CNF) est compilée en un circuit compact, et ce circuit répond à des questions sur ses modèles. Depuis des décennies, les praticiens débattent de l'opportunité de pré-traiter d'abord la CNF, et si oui, quelles simplifications sont sûres. Une étude publiée par des chercheurs du CRIL, un laboratoire conjoint CNRS et Université d'Artois, apporte une réponse claire : les pré-traitements qui préservent le nombre de modèles et conservent les définitions des variables éliminées débloquent des gains de performance significatifs, tandis que ceux qui ne préservent que la satisfiabilité sont inutiles pour l'échantillonnage et l'énumération.

Le paysage du pré-traitement

L'article, dirigé par Jean Marie Lagniez et Emmanuel Lonca, examine trois familles de techniques de pré-traitement : celles qui préservent l'équivalence logique (vivification, détection de backbone, réduction d'occurrences), celles qui ne préservent que la satisfiabilité (élimination de variables, élimination de clauses bloquées), et celles qui préservent le nombre de modèles en supprimant les variables définies. Pour des tâches comme l'échantillonnage uniforme, l'accès direct (retourner le k-ième modèle sous un ordre lexicographique) et l'énumération de modèles, la distinction a une importance profonde.

Les auteurs prouvent que les techniques préservant la satisfiabilité, comme l'élimination de variables et l'élimination de clauses bloquées, sont fondamentalement incompatibles avec ces requêtes. Dans un contre-exemple simple, la formule a ∨ b se réduit à ⊤ avec les deux méthodes, perdant toutes les informations sur les modèles originaux. « À partir de Φ', il est impossible de retrouver les modèles de Φ », écrivent-ils, confirmant une limitation connue également pour le comptage de modèles.

Plus surprenant est le constat que même les techniques préservant le nombre de modèles, éliminant les variables implicitement ou explicitement définies par d'autres variables, ne peuvent pas être appliquées directement. La formule pré-traitée seule manque de la cartographie nécessaire pour reconstruire les modèles originaux. Cependant, lorsque les définitions des variables éliminées sont stockées dans une fonction d'évaluation compatible, l'approche devient viable pour l'échantillonnage uniforme et l'énumération complète des modèles.

L'accès direct exige un ordre

Les requêtes d'accès direct, où un utilisateur demande le k-ième modèle sous un ordre lexicographique spécifique de variables, ajoutent une contrainte supplémentaire. Les auteurs définissent un « ordre compatible » qui place toutes les variables éliminées après leurs variables de définition. Cela garantit que le k-ième modèle de la formule pré-traitée, lorsqu'il est étendu avec la fonction d'évaluation, correspond exactement au k-ième modèle de l'original. Deux stratégies émergent : soit l'étape de pré-traitement fixe la fin de l'ordre des variables, soit elle restreint l'élimination aux variables dont tous les définisseurs apparaissent plus tôt dans l'ordre donné. La première élimine plus de variables ; la seconde donne à l'utilisateur une liberté totale.

L'énumération partielle des modèles est l'endroit où l'approche atteint une limite dure. Les chercheurs montrent un exemple où l'élimination d'une variable définie par un XOR conduit à un écart exponentiel entre le nombre de modèles partiels dans la formule originale et simplifiée : la fonction de parité n'a pas de représentation compacte, donc le pré-traitement détruit effectivement la structure nécessaire à l'énumération partielle.

Preuves expérimentales à partir de 1 425 benchmarks

L'équipe a mené des expériences approfondies en utilisant le pré-traitement B+E et le compilateur de connaissances d4 sur des benchmarks provenant d'études précédentes d'échantillonnage uniforme. Ils ont testé quatre configurations : aucun pré-traitement, uniquement préservation de l'équivalence (equiv), équivalence plus élimination des variables explicitement définies (#equiv-explicit), et cette dernière avec l'ordre compatible imposé (#equiv-explicit-ordered).

Le diagramme cactus révèle une hiérarchie claire. Le pré-traitement uniquement par équivalence offre des gains marginaux, ne résolvant que huit instances de plus qu'aucun pré-traitement. #equiv-explicit-ordered gère 47 instances de plus que la référence, une amélioration substantielle, tandis que #equiv-explicit en résout 55 de plus, bien qu'il ne puisse pas répondre directement aux requêtes d'accès direct sans contraintes d'ordre. Pour l'échantillonnage uniforme et l'énumération, les auteurs rapportent des réductions significatives des temps d'exécution, les circuits pré-traités surpassant systématiquement leurs homologues bruts.

Le travail souligne un principe pratique pour les ingénieurs en IA : si la tâche en aval implique le comptage de modèles, l'échantillonnage ou l'énumération, investissez dans des pré-traitements qui préservent le nombre de modèles et reportent les définitions des variables. Le surcoût lié au suivi de ces définitions est négligeable par rapport au temps de compilation économisé.