Résumé Technique : Iteris : Boucles de Recherche Agentes pour les Mathématiques Computationnelles

1. Énoncé du Problème

Le papier traite du défi consistant à appliquer l'IA aux problèmes ouverts en mathématiques computationnelles. Contrairement aux problèmes de compétition ou aux tâches d'optimisation à objectif unique, la recherche dans ce domaine nécessite une interaction complexe entre expérimentation numérique, construction adversaire et développement de preuves formelles. Les systèmes d'IA actuels peinent souvent à coordonner ces différents modes de recherche ou à maintenir des trajectoires de recherche à long terme où les faits doivent être séparés, vérifiés et réorganisés.

Les auteurs appliquent leur système proposé, Iteris, à deux problèmes ouverts spécifiques issus de la collection Simons Workshop [3] :

1. Problème 2.4 : Une comparaison asymptotique entre le Gradient Conjugué (CG) et la Descente de Coordonnées Aléatoire (RCD) sur des systèmes linéaires à spectres de loi de puissance. L'objectif est de déterminer un diagramme de phase pour le ratio de coût normalisé entre les deux méthodes.
2. Problème 4.3 : Une question concernant la capacité de la factorisation QR avec pivot de colonne (QRCP) à sélectionner de manière fiable des sous-matrices bien conditionnées à partir d'une matrice ayant des lignes orthonormées, spécifiquement sous des conditions de faible cohérence.

2. Méthodologie : Le Système Iteris

Iteris est un système de recherche agentique organisé selon une boucle exploration–planification–exécution. Il coordonne des modes de recherche distincts via un système de mémoire basé sur des fichiers qui sert à la fois de stockage d'état à long terme et de messagerie structurée entre les agents.

2.1 Le Protocole Agentique

Chaque itération du système suit trois phases distinctes :

1. Exploration (Explore) : Un Agent d'Exploration effectue un « sondage léger au niveau du dépôt ». Il lit les fichiers du projet, inspecte les itérations récentes et rédige un raisonnement de brouillon sur des voies plausibles. Crucialement, il ne rédige pas le plan officiel mais produit un avis recommandant les formes de tâches, les vérifications de minima locaux et les évaluations de risques pour éviter que le système ne s'engage trop fermement dans une branche stagnante.
2. Planification (Plan) : Un Agent de Planification lit l'état global du projet (énoncé du problème, feuille de route, mémoire, statut de la route) et l'avis d'exploration. Il décide du pool de tâches pour l'itération suivante, produisant un fichier TASK_POOL.json structuré qui définit les catégories de tâches, les objectifs, les entrées et les exigences de vérification.
3. Exécution (Execute) : Des Agents d'Exécution spécialisés reçoivent des tâches assignées et effectuent des actions de recherche spécifiques, réécrivant des fichiers de résultats structurés dans la mémoire du projet.

2.2 Les Agents d'Exécution

Le système emploie quatre catégories d'agents d'exécution, chacune dotée de compétences spécifiques définies par des spécifications de capacités basées sur Markdown :

• Agent de Fondation (Foundation Agent) : Audite les sources, fige les définitions, rédige des cartes de conjectures et maintient la discipline des affirmations.
• Agent d'Expérimentation (Experiment Agent) : Exécute des travaux numériques (harnais de test, diagnostics, recherches de contre-exemples). L'évidence est traitée comme une orientation, non comme une preuve.
• Agent de Preuve (Proof Agent) : Construit et vérifie des artefacts de preuve pour des énoncés stables, des cas particuliers ou des lemmes.
• Agent de Revue (Review Agent) : Évalue l'évidence, les lacunes de preuve et la valeur de la route, recommandant de approfondir, de recadrer ou d'abandonner une branche de recherche.

2.3 Séparation des Préoccupations

Une caractéristique clé de la conception est la séparation de l'Agent d'Exploration de l'Agent de Planification. Tandis que l'Agent de Planification maintient la cohérence globale, l'Agent d'Exploration mène des sondages agressifs pour détecter l'« inertie locale » (par exemple, un travail de suivi incrémental) et suggère des directions alternatives avant qu'une tâche ne soit officiellement engagée. Cela permet au système de chercher au-delà de son chemin actuel tout en gardant une planification globalement cohérente.

3. Contributions Clés et Résultats

3.1 Résultat I : Diagramme de Phase CG vs RCD

Iteris a été appliqué à la comparaison de CG et RCD sur des spectres de loi de puissance ($A_n = U_n \text{diag}(1^{-p}, \dots, n^{-p})U_n^*$).

• Théorème 1 : Le système a établi un diagramme de phase à paramètres fixes pour le comportement asymptotique du ratio $\rho_n(\epsilon, p)$ (époques RCD vs étapes CG) lorsque $n \to \infty$.
• Principales Découvertes :
  • Pour $p > 1$ (spectre sommable), RCD converge en $O(1)$ époques tandis que CG prend $O(n)$ étapes, donc $\rho_n \to 0$.
  • Pour $p = 1$, $\rho_n \to 0$ avec une borne logarithmique.
  • Pour $0 < p < 1$, le comportement est régi par un plancher de CG limite $F(p)$, dérivé d'un problème de moment de dimension finie impliquant la mesure de queue $\nu_p$.
  • Si le seuil d'erreur $\epsilon < F(p)$, CG nécessite des degrés croissants pour converger, tandis que RCD reste borné, causant $\rho_n \to 0$.
  • Si $\epsilon > F(p)$, CG converge en $O(1)$ étapes tandis que RCD nécessite une fraction positive d'une époque, causant $\rho_n$ pour être éloigné de zéro.
• Interaction Humain-IA : Le système a identifié la structure de phase et le mécanisme du « plancher de Hankel ». Cependant, un premier jet de preuve reposait sur une hypothèse plus forte non justifiée pour l'analyse du taux dans le régime $p < 1$. Des experts humains ont détecté cette lacune, et l'argument a été réparé par l'interaction pour fournir des bornes de taux conservatrices et vérifiées.

3.2 Résultat II : Contre-exemple QRCP

Iteris a traité la question de savoir si la QRCP garantit des sous-matrices bien conditionnées pour des matrices avec des lignes orthonormées et une cohérence bornée.

• Théorème 2 : Le système a construit une famille de contre-exemples à faible cohérence montrant que la QRCP peut échouer à sélectionner des sous-matrices bien conditionnées, même lorsque les énergies de ligne sont contrôlées uniformément.
• Principales Découvertes : Pour tout $H^* > 1$ (borne de cohérence) et $B > 0$, il existe une matrice $Q$ avec des lignes orthonormées et une cohérence $\mu(Q) < H^*$ telle que le nombre de conditionnement de la sous-matrice sélectionnée dépasse $B k^e$.
• Mécanisme : Le contre-exemple exploite une pression de « substitution arrière triangulaire ». Le système a conçu un bloc central sélectionné qui satisfait les conditions de pivot local mais crée une norme inverse élevée. Des colonnes supplémentaires ont été ajoutées pour restaurer l'orthonormalité globale sans être sélectionnées par la règle de pivotage.
• Interaction Humain-IA : Iteris a identifié l'obstruction et a généré la construction. La trajectoire de preuve était initialement circulaire ; des experts humains ont réorganisé l'argument en une preuve lisible et ont aligné le théorème informel avec une vérification formelle en Lean 4.

4. Signification et Revendications

Le papier affirme que les systèmes d'IA agentiques peuvent participer de manière significative aux flux de travail de recherche pour les problèmes ouverts en mathématiques computationnelles, mais souligne que la validation humaine reste essentielle.

• Au-delà des Benchmarks : Iteris démontre que l'IA peut aller au-delà de la résolution d'exercices isolés pour participer à une véritable recherche, générant des artefacts exploratoires à long terme et des ébauches de preuves.
• Intégration du Flux de Travail : Le système coordonne avec succès l'expérimentation numérique (pour identifier des caractéristiques structurelles comme le plancher de Hankel ou la pression de substitution arrière) avec la construction de preuves formelles.
• Rôle de l'Intervention Humaine : Les auteurs déclarent explicitement qu'Iteris déplace plutôt qu'il ne supprime l'effort humain.
  • Dans le cas de CG, le système a trouvé la structure, mais les humains ont réparé l'analyse du taux.
  • Dans le cas de QRCP, le système a trouvé le contre-exemple, mais les humains ont réorganisé la preuve et vérifié la cohérence sémantique.
• Comparaison avec les LLM directs : Les requêtes directes aux modèles avancés (ex: GPT-Pro) produisent des heuristiques plausibles ou des croquis de haut niveau mais échouent à clore les preuves, confondant souvent les distinctions entre les bornes attendues et de haute probabilité ou traitant des étapes plausibles comme des obligations remplies. Iteris, en revanche, décompose les heuristiques en obligations de preuve auditables et utilise des agents de revue pour bloquer les raccourcis injustifiés.

Le papier conclut que bien que l'IA puisse élargir l'espace de recherche et produire des ébauches d'arguments, le jugement mathématique final, la vérification des hypothèses, la détection des lacunes et l'exposition restent des responsabilités humaines critiques.