INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic

Cet article présente INDUCTION, un nouveau benchmark évaluant la capacité des modèles à synthétiser des concepts logiques du premier ordre à partir de structures finies, en mettant en évidence des gradients de difficulté marqués et l'importance de la concision des formules pour la généralisation.

L'essentiel

🧩 Le Grand Jeu du Détective Logique : INDUCTION

Imaginez que vous êtes un détective privé. Votre mission ? Découvrir la règle secrète qui explique pourquoi certaines personnes sont invitées à une fête (les "positifs") et d'autres ne le sont pas (les "négatifs").

Mais il y a un piège : vous ne pouvez pas juste deviner. Vous devez écrire la règle sous la forme d'une phrase mathématique parfaite (ce qu'on appelle une "formule logique") qui fonctionne dans tous les cas que vous avez observés.

C'est exactement ce que fait le benchmark INDUCTION. C'est un nouveau test pour voir si les intelligences artificielles (les "modèles") sont de véritables détectives logiques ou si elles sont juste de bons parleurs qui trichent.

🌍 Le Terrain de Jeu : Des Mondes Finis

Pour tester ces détectives, les chercheurs ont créé des "mondes" (des petites situations) remplis d'objets et de relations :

• Les objets : Des gens, des animaux, des points.
• Les relations : Qui connaît qui ? Qui est à côté de qui ? (Par exemple : "A est ami avec B").
• La règle cible : Une liste de ceux qui sont "invités".

Le défi ? Trouver une seule phrase logique qui explique cette liste d'invités dans tous les mondes différents, même si les détails changent.

🎮 Les Trois Niveaux de Difficulté

Le test propose trois façons de jouer, comme dans un jeu vidéo :

1. Le Niveau "Tout Vu" (FullObs) :

   • L'analogie : Vous avez une carte complète du monde. Vous voyez tout : qui est ami avec qui, qui porte un chapeau, etc.
   • Le but : Trouver la règle qui correspond parfaitement à la liste des invités. C'est le niveau de base.

2. Le Niveau "Contraste" (CI - Comme le jeu Zendo) :

   • L'analogie : On vous montre deux types de boîtes. Les boîtes OUI contiennent des objets qui respectent la règle secrète. Les boîtes NON contiennent des objets qui ne la respectent pas.
   • Le but : Trouver la règle qui fonctionne pour toutes les boîtes OUI, mais qui échoue (fait une erreur) pour toutes les boîtes NON. C'est comme trouver la différence subtile entre un vrai diamant et une fausse pierre.

3. Le Niveau "Partiel" (EC - L'Enquête Incomplète) :

   • L'analogie : Vous avez une carte, mais certaines zones sont cachées par du brouillard. Vous ne savez pas si telle personne est amie avec telle autre.
   • Le but : Trouver une règle qui fonctionne s'il existe au moins une façon de remplir les zones cachées pour que tout s'explique. C'est comme dire : "Je ne sais pas tout, mais ma théorie est valide si on suppose que le brouillard cache ceci ou cela."

🚨 Le Problème : La "Gonflette" (Bloat)

C'est ici que le test devient brillant.

Jusqu'à présent, on jugeait les IA uniquement sur le fait qu'elles trouvaient une réponse correcte. Mais imaginez un élève qui, pour résoudre un problème de mathématiques simple, écrit un roman de 50 pages avec des centaines de cas particuliers pour arriver au bon résultat. Techniquement, c'est juste, mais c'est bête.

Dans INDUCTION, les chercheurs ont remarqué que les IA les plus puissantes (comme GPT-5 ou Grok) trouvaient souvent des réponses correctes, mais énormément trop longues et compliquées.

• La solution "élégante" : "L'invité est quelqu'un qui a un ami qui porte un chapeau." (Court, beau, vrai).
• La solution "gonflée" (Bloat) : "L'invité est quelqu'un qui a un ami qui porte un chapeau, SAUF si cet ami est rouge, SAUF si le soleil brille, SAUF si..." (Une liste interminable de cas particuliers).

Les IA utilisaient ces listes interminables pour "tricher" en mémorisant les exemples plutôt qu'en comprenant la règle générale.

💡 La Grande Découverte : La Simplicité est la Clé de la Vérité

Le résultat le plus important de l'article est une révélation : Les solutions courtes et simples généralisent beaucoup mieux.

• Quand une IA trouve une solution courte (proche de la "règle d'or"), elle continue de bien fonctionner sur de nouveaux mondes qu'elle n'a jamais vus.
• Quand une IA trouve une solution "gonflée" (trop longue), elle échoue lamentablement sur les nouveaux mondes. Elle a juste appris par cœur les exemples d'entraînement sans rien comprendre.

C'est comme si un étudiant apprenait par cœur les réponses d'un examen de l'année dernière (solution gonflée) plutôt que de comprendre les concepts (solution simple). Le jour de l'examen avec de nouvelles questions, l'étudiant qui a compris gagne.

🏆 Qui a gagné ?

Le test a comparé plusieurs IA (GPT-4, GPT-5, Claude, Gemini, etc.).

• GPT-5.4 s'est distingué non pas parce qu'il trouvait plus de réponses, mais parce qu'il trouvait des réponses plus courtes et plus élégantes. Il a appris à éviter la "gonflette".
• D'autres modèles, comme Grok, trouvaient parfois des réponses correctes mais étaient souvent incapables de les formuler ou produisaient des réponses trop complexes.

🎯 En Résumé

L'article INDUCTION nous dit quelque chose de fondamental sur l'intelligence artificielle :

Ce n'est pas parce qu'une machine a la bonne réponse qu'elle a compris la leçon.

Pour vraiment être intelligente, une machine doit être capable de trouver la règle la plus simple qui explique le monde, et non pas une liste interminable d'exceptions. C'est la différence entre un robot qui mémorise et un véritable scientifique qui découvre.

Ce benchmark est donc un outil pour forcer les IA à devenir plus "humaines" dans leur raisonnement : chercher la beauté et la simplicité de la vérité, plutôt que la complexité brute.

Résumé technique

1. Problématique et Contexte

Les modèles de langage (LLM) et de raisonnement actuels sont capables de générer des formules logiques syntaxiquement valides. Cependant, il manque des évaluations rigoureuses de leur capacité à produire des explications correctes et compactes sous une sémantique entièrement spécifiée et vérifiable mécaniquement.

L'article se concentre sur la synthèse de concepts sur structures finies :

• Entrée : Plusieurs petits mondes relationnels finis (structures) étiquetés extensionnellement avec un prédicat cible unaire $T(x)$.
• Objectif : Le modèle doit produire une unique formule de logique du premier ordre (FOL) $\phi(x)$ qui récupère (explique) $T$ de manière uniforme à travers tous les mondes.
• Contrainte clé : La correction est vérifiable par un solveur (SMT/Z3) via le model checking sur des domaines finis, éliminant l'ambiguïté du langage naturel.

Le défi principal réside dans la généralisation logique (quantificateurs, structure relationnelle) plutôt que dans l'ajustement de données (fitting), tout en évitant le « gonflement » (bloat) des formules, où les modèles résolvent les problèmes par des cas particuliers complexes plutôt que par une abstraction conceptuelle.

2. Méthodologie : La Suite de Benchmarks INDUCTION

Les auteurs introduisent INDUCTION, une suite de benchmarks conçue pour évaluer la généralisation inductive sous trois régimes complémentaires, partageant un langage commun et une pipeline d'évaluation :

A. Les Trois Tâches

1. FULLOBS (Observation Complète) : Tous les faits des prédicats sont observés. Le modèle doit trouver une formule $\phi$ qui correspond exactement à l'extension de $T$ dans chaque monde d'entraînement. C'est la tâche la plus directe de synthèse de concepts.
2. CI (Induction Contrastive / Style Zendo) : Les mondes sont divisés en deux groupes : YES (la règle s'applique) et NO (la règle ne s'applique pas).
   • La solution doit correspondre parfaitement à $T$ sur tous les mondes YES.
   • Elle doit échouer à correspondre à $T$ sur chaque monde NO (au moins un élément mal classé).
   • Mécanisme de piège : Les mondes NO sont générés pour correspondre à des hypothèses « raccourcis » tentantes qui survivent aux mondes YES, forçant le modèle à rejeter ces raccourcis.
3. EC (Observation Partielle & Complétion Existentielle) : Certains atomes de base (faits) sont inconnus.
   • Une formule est valide si, pour chaque monde, il existe une complétion des atomes inconnus telle que $\phi$ corresponde à $T$.
   • Cela teste la capacité du modèle à raisonner sur ce qui pourrait être vrai dans un monde partiellement observé.

B. Génération de Données et Contrôle de Difficulté

• Formules Or (Gold) : Un pool de ~200 formules templates structurées (famille, profondeur de quantificateurs, motifs « lift-hard » où une relation apparaît sous un quantificateur universel).
• Génération de Mondes : Les mondes sont générés pour éliminer les hypothèses distracteurs (raccourcis, mutants proches) tout en conservant la formule or.
• Filtres de Rejet : Élimination des instances triviales (solutions atomiques, sous-formules) pour garantir que le raisonnement sur les quantificateurs est nécessaire.

C. Métriques d'Évaluation

Au-delà de la simple exactitude (validité), l'article introduit des métriques de parsimonie :

• Acc@(+$\Delta$) : Taux de succès où la taille de la formule (AST) est proche de la formule or (ex: AST $\le$ AST(Or) + 25).
• Taux de Gonflement (Bloat Rate) : Fréquence des solutions valides mais excessivement longues.
• Généralisation sur Mondes Retenus (Held-out) : Évaluation de la capacité de la formule à généraliser sur de nouveaux mondes générés à partir de la même règle or.

3. Résultats Clés

Les expériences ont été menées sur une variété de modèles (GPT-4o, GPT-5.2/5.4, Grok4, Claude Opus, Gemini, etc.).

A. Difficulté et Généralisation

• Gradients de difficulté nets : La performance chute drastiquement lorsque la profondeur des quantificateurs passe de 1 à 2, ou lorsque le nombre de mondes augmente.
• Le paradoxe du Gonflement (Bloat) : Certains modèles (notamment GPT-5.2) atteignent une haute validité en générant des formules énormes basées sur le découpage de cas (case-splitting).
  • Résultat crucial : Les formules « gonflées » (bloat) généralisent beaucoup moins bien sur les mondes retenus que les formules compactes.
  • Exemple : Pour GPT-5.4, la généralisation chute de 92,4 % (solutions proches de l'or) à 20,9 % (solutions gonflées). Cela confirme que le gonflement est un signe de surapprentissage (overfitting) aux mondes d'entraînement plutôt que d'apprentissage du concept.

B. Comparaison des Modèles

• GPT-5.4 se distingue par une meilleure parsimonie : il obtient des scores budgétés (Acc@+25) supérieurs à GPT-5.2 tout en réduisant le taux de gonflement, indiquant une meilleure capacité d'abstraction.
• Grok4 montre une forte performance sur FULLOBS mais souffre d'un taux de couverture (coverage) plus faible (échecs de génération).
• GPT-5.4 domine la tâche EC (complétion existentielle) avec une validité de 93,5 %, surpassant nettement les autres modèles.
• Échec des modèles plus anciens : GPT-4o obtient 0 % de précision sur FULLOBS, suggérant que ces tâches nécessitent des capacités de raisonnement relationnel non élicitées par le prompting standard.

C. Analyse des Échecs

• CI : Les échecs proviennent souvent de l'incapacité à utiliser la preuve négative (mondes NO) pour rejeter des hypothèses de raccourcis.
• EC : Les modèles ont du mal à raisonner sur les complétions existentielles, produisant souvent des formules qui ne sont valides que pour une complétion spécifique, ou qui échouent structurellement.

4. Contributions Principales

1. Formalisation Unifiée : Définition d'un cadre de synthèse de concepts sur structures finies en FOL avec trois tâches (FULLOBS, CI, EC) aux sémantiques vérifiables par solveur.
2. Génération Contrôlée : Méthodes de génération de données incluant des « pièges » pour la tâche contrastive et des diagnostics d'espace des versions pour contrôler la difficulté.
3. Métriques de Parsimonie : Introduction de métriques qui pénalisent le gonflement des formules, démontrant que la simplicité est un proxy robuste pour la généralisation et l'abstraction conceptuelle.
4. Benchmark Stable (v1) : Publication de résultats sur une suite de benchmarks reproductible, reliant les modes d'échec aux propriétés structurelles des instances (ex: motifs « lift-hard »).

5. Signification et Conclusion

L'article démontre que la validité logique seule est insuffisante pour évaluer la compréhension logique des modèles. Un modèle peut « tricher » en mémorisant des configurations spécifiques via des formules énormes, ce qui conduit à un échec de généralisation.

Leçons clés :

• La capacité à former des hypothèses concises et stables sous de nouvelles preuves est le véritable marqueur d'une induction réussie, similaire à la pratique scientifique et mathématique humaine.
• Les benchmarks logiques doivent intégrer des contraintes de complexité syntaxique (AST) pour éviter de récompenser le surapprentissage.
• INDUCTION fournit une méthodologie pour construire des benchmarks logiques où la difficulté est contrôlable et les erreurs sont analysables au niveau de la structure des quantificateurs.

En résumé, INDUCTION propose un nouveau standard pour évaluer non seulement si un modèle peut « résoudre » un problème logique, mais s'il peut découvrir la règle sous-jacente de manière élégante et généralisable.