Résumé Technique : Découverte par IA de Relaxations Convexes via des Agents Duaux

1. Énoncé du Problème

L'article traite du défi consistant à améliorer les bornes inférieures certifiées pour les inégalités à constante aiguë en analyse fonctionnelle, en se concentrant spécifiquement sur les problèmes d'optimisation non convexes où l'objectif est de trouver l'infimum d'un score sur un espace de dimension infinie de fonctions admissibles.

Les auteurs ciblent deux constantes spécifiques étudiées par Georgiev et al. (2025) :

1. La première inégalité d'autocorrélation (C6.2) : Une constante issue de la combinatoire additive liée aux ensembles de Sidon, définie par l'inégalité :
   $$\max_{-1/2 \le t \le 1/2} \int_{\mathbb{R}} f(t-x)f(x) \, dx \ge C_{6.2} \left( \int_{-1/4}^{1/4} f(x) \, dx \right)^2$$
   pour toutes fonctions non négatives $f: \mathbb{R} \to \mathbb{R}$.
2. La constante de recouvrement minimum d'Erdős (C6.5) : Une constante régissant l'asymptotique du problème de recouvrement minimum, définie par :
   $$\sup_{x \in [-2, 2]} \int_{-1}^{1} f(t)g(x+t) \, dt \ge C_{6.5}$$
   pour des fonctions non négatives $f, g: [-1, 1] \to [0, 1]$ telles que $f+g=1$ et $\int f = 1$.

Alors que des travaux récents pilotés par l'IA ont réussi à améliorer les bornes supérieures en cherchant des constructions extrémales (des fonctions spécifiques qui violent une borne), l'amélioration des bornes inférieures est une tâche distincte. Une borne inférieure doit être vraie pour chaque fonction admissible, ce qui nécessite de prouver qu'aucune fonction ne peut abaisser le score en dessous d'une certaine valeur. Cela est généralement accompli en résolvant une relaxation convexe du problème non convexe d'origine. Plus la relaxation est serrée (c'est-à-dire plus de contraintes valides sont ajoutées), plus la borne inférieure est forte.

2. Méthodologie : La Boucle des Agents Duaux

Les auteurs instaurent un paradigme d'autorécherche utilisant un cadre avec intervention humaine piloté par deux agents spécialisés basés sur des modèles de langage de grande taille (LLM). Le système est conçu pour découvrir et vérifier de manière itérative des contraintes valides qui resserrent une relaxation convexe.

Les Agents

1. L'Agent de Codage (Coding Agent) :

   • Rôle : Propose de nouvelles contraintes ou renforce les contraintes existantes pour le programme convexe.
   • Sortie : Génère un programme d'optimisation convexe modifié et une « preuve rigoureuse » (un argument mathématique) justifiant pourquoi la nouvelle contrainte est respectée pour toutes les fonctions admissibles.
   • Action : Implémente la contrainte en code (en utilisant CVXPY) et résout le programme pour produire une borne inférieure candidate.

2. L'Agent de Théorie (Theory Agent) :

   • Rôle : Agit comme vérificateur et chercheur de contre-exemples.
   • Action : Lit la contrainte proposée et sa preuve. Il analyse de manière critique la logique pour s'assurer que la contrainte est une conséquence nécessaire des conditions d'admissibilité (par exemple, $f \ge 0$). Crucialement, il recherche activement des contre-exemples — des fonctions admissibles spécifiques dont les coefficients violent la contrainte proposée.
   • Décision : Si la preuve est solide et qu'aucun contre-exemple n'est trouvé, la contrainte est acceptée. Si une faille ou un contre-exemple est détecté, la proposition est rejetée et l'Agent de Codage est dirigé vers une autre approche.

Le Pipeline de Vérification

Pour garantir que le résultat final est une borne certifiée (mathématiquement prouvée et non simplement estimée numériquement), le système utilise un processus de double certification rigoureux :

• Faisabilité Duale : Le système construit le dual du programme convexe.
• Arithmétique d'Intervalle : Il trouve un point dual-faisable $\lambda$ et vérifie sa faisabilité ainsi que la valeur de l'objectif dual en utilisant une arithmétique d'intervalle rigoureuse. Cela prend en compte les erreurs d'arrondi de la virgule flottante et les données irrationnelles du problème (par exemple, les moments trigonométriques).
• Certification : Par dualité faible, un point dual valide $\lambda$ avec une valeur d'objectif $\beta$ prouve que l'optimum primal (et donc la vraie constante) est au moins égal à $\beta$. La borne rapportée est la borne inférieure d'un emboîtement vérifié.

Rôle de l'Humain

Un chercheur humain effectue une revue finale et une compactification. La boucle des agents accumule souvent des contraintes redondantes. L'humain examine le programme final, supprime les contraintes inutiles pour créer une formulation minimale et lisible, et vérifie les arguments mathématiques avant la certification finale.

3. Contributions Clés

• Changement de Paradigme : L'article démontre une application novatrice des agents IA à la découverte de relaxations convexes plutôt qu'à la simple recherche d'exemples extrémaux. Il traite le côté « borne inférieure » des inégalités, ce qui nécessite de prouver une quantification universelle (validité pour toutes les fonctions) plutôt qu'une quantification existentielle (trouver une fonction).
• Cadre de Double Agent : Il introduit une boucle spécifique où un agent de codage propose des contraintes et un agent de théorie vérifie la validité et traque les contre-exemples, automatisant ainsi l'affinement itératif des relaxations mathématiques.
• Certification Rigoureuse : L'intégration de l'arithmétique d'intervalle et des vérifications de faisabilité duale garantit que les bornes améliorées sont mathématiquement certifiées, indépendamment de la précision en virgule flottante du solveur numérique.

4. Résultats

Le cadre a été appliqué aux deux constantes mentionnées ci-dessus, améliorant les bornes inférieures certifiées :

• C6.2 (Première inégalité d'autocorrélation) :

  • Ancienne meilleure borne inférieure : 1.28 (Cloninger & Steinerberger, 2017).
  • Nouvelle borne inférieure certifiée : 1.2937.
  • Note : Aucun programme convexe n'existait auparavant pour ce problème ; les agents l'ont construit de toutes pièces.

• C6.5 (Constante de recouvrement minimum d'Erdős) :

  • Ancienne meilleure borne inférieure : 0.379005 (White, 2022).
  • Nouvelle borne inférieure certifiée : 0.37912.
  • Note : Les agents sont partis du programme convexe existant de White et ont découvert deux nouvelles contraintes valides basées sur le théorème de Bochner (imposant que les séquences de moments de $f$ et de son complément $g=1-f$ soient réalisables par des mesures non négatives).

L'article note que les bornes supérieures pour ces problèmes ont été améliorées par des méthodes de recherche (par exemple, Together AI, 2026), mais que les bornes inférieures étaient restées stagnantes depuis 2022. Ce travail fait progresser avec succès les bornes inférieures.

5. Signification et Revendications

Les auteurs affirment qu'il s'agit de la première utilisation d'une boucle d'agents de type autorécherche pour améliorer les bornes inférieures certifiées sur ces inégalités spécifiques. La signification réside dans :

1. Complémentarité : Cela complète la recherche actuelle sur l'IA qui se concentre sur la recherche d'exemples extrémaux (bornes supérieures) en s'attaquant au problème plus difficile de prouver les bornes inférieures via la relaxation.
2. Autonomie de Découverte : Les agents ont identifié avec succès des propriétés mathématiques (telles que les conditions de Bochner pour $f$ et $1-f$) que les formulations conçues par des humains avaient négligées ou n'avaient pas imposées explicitement.
3. Généralité : Bien que démontrée sur les inégalités d'autocorrélation, les auteurs affirment que le cadre n'est pas spécifique à ces problèmes. Il s'applique à tout problème d'optimisation non convexe dont une borne inférieure peut être exprimée par une relaxation convexe resserrée par des contraintes valides et certifiée par dualité (par exemple, en optimisation, en combinatoire et en contrôle).

L'article conclut avec modestie, reconnaissant que la validité des contraintes repose actuellement sur la revue humaine des arguments mathématiques plutôt que sur des assistants de preuve formelle (comme Lean), bien qu'il suggère qu'une intégration future avec des outils de vérification formelle pourrait rendre la boucle entièrement autonome.