Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design

Cet article présente une découverte mathématique en théorie des designs combinatoires, obtenue par une collaboration neurosymbolique entre un agent IA, des outils de calcul formel et un humain, aboutissant à une nouvelle borne inférieure stricte pour le déséquilibre des carrés latents dans le cas $n \equiv 1 \pmod{3}$.

L'essentiel

Voici une explication simple et imagée de cette recherche, comme si on racontait une histoire autour d'un café.

🧠 L'Histoire : Une équipe de trois pour résoudre l'énigme des carrés magiques

Imaginez que les mathématiciens cherchent à résoudre un casse-tête très difficile : les carrés latins.
Pour faire simple, un carré latin est comme une grille de Sudoku, mais sans les sous-grilles. Vous devez remplir une case $n \times n$ avec des chiffres de 0 à $n-1$, de sorte qu'aucun chiffre ne se répète dans une ligne ou une colonne.

Le but du jeu ? Trouver la configuration la plus "équilibrée" possible. Mais il y a un problème : pour certaines tailles de grille (quand le nombre $n$ donne un reste de 1 quand on le divise par 3), il est impossible d'avoir un équilibre parfait. C'est comme essayer de couper une pizza en parts parfaitement égales avec un nombre de parts qui ne va pas.

La question était : "Quel est le meilleur équilibre possible dans ce cas impossible ?"

Pour répondre, les chercheurs ont monté une équipe spéciale composée de trois membres très différents, qui travaillent ensemble comme un trio de super-héros :

1. L'IA (Le Détective Curieux) : Un cerveau artificiel très rapide, capable de lire des milliers de grilles et de repérer des motifs invisibles pour l'œil humain.
2. L'Outil Symbolique (Le Vérificateur Rigoureux) : Des logiciels de calcul ultra-précis (comme des calculatrices géantes) qui ne font jamais d'erreur de logique et peuvent vérifier chaque détail mathématique.
3. L'Humain (Le Capitaine de l'Équipe) : Le chercheur qui a le bon sens, l'intuition et qui décide de changer de direction si l'équipe tourne en rond.

---

🚦 Le Voyage en 4 Étapes

1. Le Mur (L'impasse)

Au début, l'équipe a essayé de trouver une formule magique (une construction algébrique) pour créer ces grilles parfaites.

• Ce qui s'est passé : L'IA a calculé des milliers de possibilités. Le vérificateur a tout analysé.
• Le résultat : Rien. C'était comme chercher une aiguille dans une botte de foin, sauf que la botte de foin n'avait pas d'aiguille. C'était une impasse.
• Le rôle de l'IA : Elle a dit : "Je ne trouve rien, c'est du bruit blanc."

2. Le Changement de Cap (Le coup de génie humain)

C'est ici que l'humain intervient. Au lieu de continuer à chercher l'impossible (l'équilibre parfait), il a dit : "Attendez, si on ne peut pas avoir zéro déséquilibre, quel est le plus petit déséquilibre possible ?"

• L'analogie : C'est comme si vous cherchiez à construire un pont parfaitement droit sur une rivière, mais que la géographie l'interdit. Au lieu d'abandonner, l'humain a dit : "Ok, quel est le pont le plus droit qu'on puisse construire ?"
• Pourquoi c'est crucial : L'IA seule n'aurait probablement jamais eu cette idée de changer la question. Elle aurait continué à chercher le "zéro" jusqu'à épuisement.

3. La Découverte (Le motif caché)

Avec la nouvelle question, l'IA s'est remise au travail. Elle a regardé des milliers de grilles générées par ordinateur et a remarqué quelque chose d'étrange :

• L'observation : Dans toutes les meilleures grilles, un certain nombre (la "distance" entre les lignes) était toujours pair (un nombre divisible par 2).
• L'analogie : Imaginez que vous comptez les pas de milliers de personnes. L'IA a remarqué que, pour les meilleurs marcheurs, ils faisaient toujours des pas de 2 mètres, jamais de 1 mètre. C'était une règle cachée que personne n'avait vue avant.
• Le résultat : L'IA a utilisé cette règle pour prouver mathématiquement qu'on ne pouvait pas faire mieux qu'une certaine limite. Elle a trouvé la réponse : $4n(n-1)/9$.

4. La Vérification (Le test de réalité)

L'IA a proposé sa preuve, mais elle était un peu trop confiante et avait fait deux petites erreurs (elle pensait que sa règle s'appliquait à tout, alors que non).

• Le rôle du Vérificateur (Symbolique) : Il a dit : "Attends, ta preuve ne marche que pour un type de grille spécifique, pas pour toutes !"
• Le rôle de l'Humain : Il a aidé à corriger le tir.
• Le verdict final : Une fois corrigée, la preuve a été vérifiée par un logiciel de mathématiques pur (Lean 4) qui a confirmé : "C'est vrai, c'est incontestable."

---

💡 Ce qu'on a appris de cette expérience

Cette étude nous apprend trois choses importantes sur l'avenir de l'IA :

1. L'IA est excellente pour trouver des motifs : Elle peut voir des régularités dans des montagnes de données que l'humain ne verrait jamais (comme le fait que les nombres soient toujours pairs).
2. L'IA est mauvaise pour inventer des stratégies : Elle est très bonne pour répondre à une question, mais elle est nulle pour se dire "Tiens, je devrais poser une autre question". Elle a besoin d'un humain pour la rediriger quand elle est dans une impasse.
3. L'IA est un excellent critique, mais un mauvais inventeur : Quand on demande à plusieurs IA de discuter entre elles, elles sont très douées pour trouver les erreurs des autres ("Tu as fait une erreur ici !"), mais elles sont souvent confiantes et fausses quand elles essaient de proposer de nouvelles idées mathématiques complexes.

🏆 Le Résultat Final

Grâce à cette collaboration, l'équipe a découvert une nouvelle classe de solutions mathématiques (qu'ils appellent des "permutations quasi-parfaites") et a prouvé qu'on ne peut pas faire mieux que cette limite précise. C'est une vraie découverte mathématique, validée par des machines et dirigée par un humain.

En résumé : L'IA a fourni les yeux pour voir le motif, l'ordinateur a fourni les mains pour vérifier les calculs, et l'humain a fourni le cerveau pour changer de direction quand le chemin était bloqué. Ensemble, ils ont résolu un problème qui restait ouvert depuis longtemps.

Résumé technique

Voici un résumé technique détaillé de l'article « Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design », rédigé en français.

1. Problématique et Contexte

L'article s'intéresse à la découverte mathématique autonome via une approche neuro-symbolique, où un agent IA (basé sur un Grand Modèle de Langage ou LLM) collabore avec des outils de calcul symbolique et une direction stratégique humaine.

Le problème central étudié est la théorie des carrés latins en combinatoire. Plus précisément, les auteurs se concentrent sur le problème de l'imbalance (déséquilibre spatial) d'un carré latin $n \times n$.

• Un carré latin est dit « équilibré spatialement » (SBLS) si son imbalance $I(L)$ est nulle.
• Il est connu que $I(L) = 0$ est impossible lorsque $n \equiv 1 \pmod 3$, car la distance idéale entre les lignes n'est pas un entier.
• Le défi ouvert : Déterminer la borne inférieure stricte (tight lower bound) de l'imbalance minimale pour le cas difficile où $n \equiv 1 \pmod 3$. Les travaux précédents n'avaient pas réussi à établir cette borne ni à construire des objets l'atteignant.

2. Méthodologie : Collaboration Neurosymbolique Agentic

Les auteurs proposent un cadre de collaboration en trois composantes, orchestré par un agent IA (utilisant le modèle Claude Opus 4.5) disposant d'un accès terminal, d'un système de fichiers et d'outils externes.

Architecture du système (Figure 1)

1. L'Agent (Neural) : Traduit les objectifs en code, exécute des outils, synthétise des résultats en conjectures et ébauches de preuves. Il est responsable de la reconnaissance de motifs et de la génération d'hypothèses.
2. Composante Symbolique :
   • SageMath : Pour l'analyse algébrique et l'interpolation polynomiale.
   • Solveur Rust : Pour l'énumération exhaustive de structures combinatoires.
   • Recuit Simulé (Python/JIT) : Pour l'optimisation stochastique et la recherche de solutions approchées.
3. Direction Humaine : Fournit la stratégie, valide les pivots de recherche et décide des orientations.
4. Mémoire Persistante : Un système à deux niveaux (fichier d'instructions de projet et base de connaissances thématique) permet de maintenir la continuité entre plusieurs sessions de travail sans mettre à jour les poids du modèle.
5. Révision Multi-Modèle : Des LLMs de pointe sont consultés en parallèle pour critiquer les preuves et détecter les erreurs.

Déroulement du processus de découverte (5 phases)

1. Impasse Algébrique : Tentative initiale de trouver des constructions algébriques pour des permutations parfaites (imbalance nulle). L'analyse des données (interpolation, analyse d'orbites) révèle une absence de structure algébrique pour $n \ge 6$.
2. Pivot de Recherche (Humain) : L'humain redéfinit le problème : au lieu de chercher un objet à imbalance nulle (impossible), on cherche à caractériser l'imbalance positive minimale.
3. Découverte de la Contrainte de Parité (IA) : L'agent analyse les données numériques des meilleures permutations trouvées par recuit simulé. Il remarque que la fonction de corrélation de décalage $f_\sigma(\delta)$ est toujours paire. Cette observation, invisible par analyse symbolique pure, conduit à une nouvelle borne inférieure.
4. Formalisation et Révision : L'agent rédige une preuve. Une révision multi-modèle détecte deux erreurs : une généralisation abusive (la preuve utilisait des propriétés de carrés circulants non valables pour tous les carrés latins) et une erreur de notation ($\sigma$ vs $\sigma^{-1}$).
5. Extension Computationnelle : L'agent introduit le concept de « permutations quasi-parfaites » (near-perfect permutations) et utilise le recuit simulé pour prouver l'existence de ces objets jusqu'à $n=52$, atteignant exactement la borne théorique.

3. Résultats Principaux

Les contributions mathématiques et techniques sont les suivantes :

A. Résultat Mathématique

• Théorème de la borne inférieure : Pour tout $n \equiv 1 \pmod 3$, l'imbalance d'un carré latin $L$ satisfait :
  $$I(L) \ge \frac{4n(n-1)}{9}$$
• Preuve formelle : Le résultat a été vérifié formellement dans l'assistant de preuves Lean 4.
• Construction optimale : Introduction d'une nouvelle classe d'objets, les permutations quasi-parfaites (near-perfect permutations), définies par des fonctions de corrélation de décalage prenant uniquement les valeurs $\{a, a+2\}$. Ces permutations atteignent exactement la borne inférieure.
• Validation empirique : L'existence de ces permutations a été confirmée par calcul pour tous les $n \equiv 1 \pmod 3$ jusqu'à $n=52$.

B. Contributions Méthodologiques

1. Cadre de collaboration agentic : Démonstration qu'un agent LLM peut orchestrer des outils symboliques complexes pour résoudre un problème mathématique ouvert.
2. Asymétrie de la délibération multi-modèle : L'étude révèle que les LLMs de pointe sont fiables pour la critique (détection d'erreurs, comme le piège des structures circulantes) mais peu fiables pour les affirmations constructives (ex: prédictions incorrectes sur la complexité asymptotique de certaines applications).
3. Analyse des rôles cognitifs :
   • IA : Découverte de structures cachées (parité), génération d'hypothèses.
   • Symbolique : Vérification rigoureuse, énumération exhaustive, recherche stochastique.
   • Humain : Pivots stratégiques (changement de question), contrôle qualité.

4. Signification et Implications

• Preuve de concept pour la découverte mathématique : L'article démontre que les systèmes neurosymboliques peuvent produire de véritables découvertes en mathématiques pures, et non seulement optimiser des problèmes existants.
• Rôle crucial de l'humain : L'analyse contrefactuelle montre que sans l'intervention humaine pour changer la question de recherche (de la recherche d'un objet impossible à l'optimisation), l'agent serait resté bloqué dans une impasse. L'IA actuelle manque encore de capacités métacognitives pour abandonner une direction infructueuse.
• Limites et perspectives :
  • Les outils symboliques butent sur des murs combinatoires (ex: énumération impossible au-delà de $n=18$ sans heuristiques).
  • L'asymétrie critique/construction des LLMs suggère que les futurs systèmes doivent être conçus pour maximiser la critique et minimiser la génération directe de conjectures non vérifiées.
  • L'intégration de la vérification formelle dans la boucle de raisonnement de l'agent est essentielle pour éviter les erreurs de généralisation.

En conclusion, cette étude illustre comment la combinaison de l'intuition de reconnaissance de motifs des LLMs, de la rigueur des outils symboliques et de la direction stratégique humaine peut résoudre des problèmes mathématiques ouverts complexes, ici en établissant une borne optimale pour l'imbalance des carrés latins.