📊 statistics

Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

Ce papier démontre que les prouveurs de théorèmes hiérarchiques réalisent une réduction exponentielle de la complexité d'échantillonnage par rapport aux prouveurs plats en apprenant des structures de preuve réutilisables à partir de traces d'enseignants, évitant ainsi la répétition redondante de sous-preuves difficiles inhérente aux représentations aplatis.

Auteurs originaux : Sho Sonoda, Shunta Akiyama, Yuya Uezato

Publié 2026-05-11

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Sho Sonoda, Shunta Akiyama, Yuya Uezato

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous enseigniez à un étudiant comment résoudre un puzzle très complexe, comme un immense puzzle en pièces ou un problème mathématique difficile. L'objectif est de permettre à l'étudiant de trouver la solution aussi rapidement et efficacement que possible, en utilisant une quantité limitée de temps et d'efforts.

Ce document pose une question simple : Est-il préférable d'enseigner à l'étudiant de résoudre le puzzle entier à partir de zéro à chaque fois, ou de lui apprendre à reconnaître et réutiliser de plus petits morceaux du puzzle déjà résolus ?

Les auteurs soutiennent qu'enseigner à l'étudiant de réutiliser des morceaux (une approche hiérarchique) est exponentiellement plus efficace que de le forcer à résoudre à nouveau chaque petite étape à partir de zéro (une approche plate), même si les « morceaux » eux-mêmes sont difficiles à déterminer.

Voici la décomposition utilisant des analogies du quotidien :

1. Les deux façons d'apprendre

L'étudiant « Plate » (Le travailleur acharné)
Imaginez un étudiant à qui l'on donne une recette pour un immense banquet. Chaque fois que la recette indique « préparez la sauce », l'étudiant doit repartir de zéro : émincer les oignons, peler l'ail, laisser mijoter les tomates et tout mixer. Même si la recette demande la sauce dix fois, cet étudiant prépare dix batches de sauce séparés, éminçant les oignons dix fois.

Dans le document : Il s'agit d'un « prouveur plat ». Il voit la preuve entière comme une longue ligne droite d'étapes. Si un argument logique spécifique (comme un lemme) est nécessaire cinq fois, l'étudiant doit apprendre et exécuter ces cinq étapes cinq fois séparément.

L'étudiant « Hiérarchique » (L'organisateur intelligent)
Imaginez maintenant un étudiant plus intelligent. Lorsqu'il voit « préparez la sauce », il réalise : « Je l'ai déjà fait ! » Il note : « Recette de sauce : émincer, peler, mijoter ». La prochaine fois que la recette demande de la sauce, il dit simplement « Utilisez la recette de sauce », et il n'a pas besoin d'émincer les oignons à nouveau. Il construit une bibliothèque de « blocs » réutilisables (lemmes).

Dans le document : Il s'agit d'un « prouveur hiérarchique ». Il décompose le problème en une carte (un DAG, ou graphe orienté acyclique) où les parties partagées sont résolues une fois puis référencées de nombreuses fois.

2. La découverte centrale : l'écart « exponentiel »

La principale découverte du document concerne la complexité d'échantillonnage. En termes simples, cela signifie : « Combien d'exemples l'étudiant doit-il étudier pour devenir compétent dans la tâche ? »

Les auteurs prouvent que si un problème nécessite de réutiliser une sous-étape difficile de nombreuses fois, l'étudiant « Plate » doit voir cette étape difficile répétée exponentiellement plus souvent dans ses données d'entraînement que l'étudiant « Hiérarchique ».

L'analogie de la bibliothèque :

Étudiant Plate : Pour apprendre à écrire un livre qui cite un poème célèbre 1 000 fois, cet étudiant doit lire le livre entier 1 000 fois, mémorisant les 10 lignes du poème à chaque fois. Il a besoin d'une bibliothèque massive de livres pour apprendre cela.
Étudiant Hiérarchique : Cet étudiant lit le livre une fois. Il mémorise les 10 lignes du poème une seule fois et les place dans une « Boîte de citation ». Lorsqu'il doit le citer à nouveau, il pointe simplement vers la boîte. Il a besoin d'une toute petite bibliothèque pour apprendre la même chose.

Le document montre que si le « poème » (la sous-preuve difficile) est ardu, l'étudiant Plate pourrait avoir besoin de millions d'exemples pour l'apprendre, tandis que l'étudiant Hiérarchique n'aurait besoin que de dizaines. La différence n'est pas minime ; c'est un écart exponentiel.

3. Pourquoi cela se produit-il ?

Les auteurs modélisent cela en utilisant un concept appelé MDP (Processus de Décision Markovien), qui n'est qu'une manière sophistiquée de décrire un jeu avec des règles, des états et des mouvements.

Le Professeur : Un résolveur parfait qui montre à l'étudiant des preuves réussies.
Les Données : L'étudiant apprend en observant ces preuves réussies.
Le Problème : Si la preuve du professeur utilise un raccourci astucieux (un lemme) cinq fois, la vue « Plate » des données ressemble à cinq chemins longs et difficiles séparés. L'étudiant doit apprendre cinq chemins séparés.
La Solution : La vue « Hiérarchique » voit que ces cinq chemins ne sont en fait qu'un seul chemin répété. L'étudiant n'a besoin d'apprendre que ce seul chemin.

Le document fournit des formules mathématiques (bornes) pour prouver que le nombre d'exemples d'entraînement nécessaires pour l'étudiant Hiérarchique reste faible, tandis que le nombre nécessaire pour l'étudiant Plate explose à mesure que le problème devient plus profond.

4. Ce que cela signifie pour les prouveurs de théorèmes en IA

Le document se concentre sur les Prouveurs de Théorèmes Agents — des systèmes d'IA qui tentent de prouver des théorèmes mathématiques. Ces systèmes tentent souvent de décomposer les grands problèmes en plus petits « sous-objectifs » ou « lemmes ».

Le point de vue du sceptique : « Pourquoi prendre la peine de le décomposer ? Prouver le petit lemme est difficile. Pourquoi perdre du temps là-dessus ? »
La réponse du document : « Parce que si vous ne le décomposez pas et ne réutilisez pas la solution, vous devrez résoudre ce même problème difficile encore et encore. Le 'gaspillage' de résoudre le lemme une fois est en réalité une économie massive par rapport à le résoudre mille fois. »

Résumé

Pensez-y comme à la construction d'une maison :

Approche Plate : Vous construisez la maison en posant chaque brique individuellement, même si vous devez construire le même motif de mur 100 fois. Vous avez besoin d'une montagne de briques et de beaucoup de temps.
Approche Hiérarchique : Vous construisez un « module de mur » une fois. Ensuite, vous empilez simplement ce module préfabriqué 100 fois. Vous avez besoin de beaucoup moins de matières premières et de moins de temps.

Le document prouve mathématiquement que pour les problèmes complexes, l'approche « module » (hiérarchique) nécessite exponentiellement moins d'exemples d'entraînement pour apprendre que l'approche « brique par brique » (plate). Cela explique pourquoi les prouveurs de théorèmes en IA modernes qui utilisent des « lemmes » et des « sous-objectifs » sont statistiquement plus efficaces que ceux qui tentent de résoudre tout en une seule longue ligne plate.

Titre : Séparation exponentielle de la complexité d'échantillonnage entre les prouveurs de théorèmes agissants plats et hiérarchiques

Auteurs : Sho Sonoda, Shunta Akiyama, Yuya Uezato
Affiliations : CyberAgent, RIKEN AIP
Date : 7 mai 2026

1. Énoncé du problème

Les récents prouveurs de théorèmes agissants emploient souvent des stratégies de décomposition — telles que la génération de lemmes intermédiaires, d'ébauches de preuve ou de décompositions de sous-objectifs — avant d'engager une recherche au niveau des tactiques. Bien que la théorie classique des preuves suggère que les lemmes puissent raccourcir les dérivations, le coût statistique de l'apprentissage consistant à découvrir et à prouver ces étapes intermédiaires reste une question ouverte. Plus précisément, si la preuve d'un lemme est elle-même difficile, pourquoi un prouveur appris devrait-il y consacrer des efforts ?

L'article aborde le problème d'apprentissage statistique de savoir si l'apprentissage d'une structure de preuve réutilisable (hiérarchique) augmente la probabilité de trouver une preuve vérifiée dans un budget de recherche fixe par rapport à l'apprentissage à partir de traces de preuve entièrement intégrées (plat). Les auteurs se concentrent sur la distribution de données induite par un prouveur « enseignant », composée d'états initiaux de théorèmes et de traces de preuve réussies et vérifiées, plutôt que sur la complexité de preuve dans le pire des cas pour toutes les formules.

2. Méthodologie

Les auteurs modélisent la preuve de théorèmes comme un processus de décision markovien (MDP) déterministe à horizon fini où les états sont des états de preuve et les actions sont des tactiques, des règles d'inférence ou des mouvements de décomposition de haut niveau. Ils analysent l'apprentissage par imitation hors ligne à partir de traces d'enseignants réussies dans trois configurations distinctes :

Configuration 1 (Plat) : L'enseignant génère des traces de preuve de bas niveau entièrement intégrées. L'élève imite ces traces sans prédiction de graphe ni mémorisation. Les sous-preuves répétées apparaissent comme des occurrences distinctes et copiées dans les données d'entraînement et de test.
Configuration 2 (Hiérarchique) : L'enseignant construit un graphe acyclique dirigé (DAG) de preuve de haut niveau où les nœuds représentent des blocs de preuve réutilisables. L'élève apprend un prédicteur de graphe et des politiques pour des actions de graphe de haut niveau (sélection, expansion, réutilisation de blocs) et une résolution locale de bas niveau. Les données d'entraînement consistent en des traces intégrées, obligeant l'élève à inférer la structure latente du DAG de preuve.
Configuration 3 (Comparaison) : Un élève plat et un élève hiérarchique sont tous deux entraînés sur les mêmes données sources générées par l'enseignant hiérarchique (traces intégrées). L'élève plat rejette la structure de graphe latente, tandis que l'élève hiérarchique l'infère. Cette configuration isole l'effet de la représentation sur la complexité d'échantillonnage.

L'analyse repose sur trois quantités clés :

$L$ (Longueur moyenne) : Le nombre moyen de décisions dans une preuve réussie.
$\eta$ (Perte de recherche intrinsèque) : La masse de probabilité perdue car l'action suivante de l'enseignant ne figure pas dans la liste des $k$ meilleurs candidats de l'élève (prévisibilité locale).
$e$ (Erreur d'imitation) : La divergence de Kullback-Leibler (KL) entre la politique de l'élève et celle de l'enseignant.

Les auteurs supposent une condition de marge de type Tsybakov pour convertir l'erreur d'imitation en probabilité d'omission top- $k$ et supposent la complétude de la recherche si les actions de l'enseignant sont contenues dans la liste des $k$ meilleurs de l'élève.

3. Contributions principales

Formalisation : L'article formule la preuve de théorèmes guidée par un vérificateur comme un MDP à horizon fini et définit la « prouvabilité statistique » comme la probabilité moyenne de trouver une preuve vérifiée dans un budget sur une distribution d'états initiaux.
Garanties de succès : Les auteurs dérivent des bornes de succès à échantillon fini pour les élèves plats (entraînés sur des traces intégrées) et les élèves hiérarchiques (entraînés à prédire des DAG réutilisables). Les bornes séparent explicitement le nombre de décisions, la perte intrinsèque top- $k$ et l'erreur de classement apprise.
Séparation exponentielle : Le résultat théorique principal est une séparation exponentielle de la complexité d'échantillonnage suffisante. Lorsqu'un DAG de preuve réutilisable est aplati en un arbre, des sous-preuves identiques sont dupliquées un nombre exponentiel de fois. L'article démontre que le certificat d'échantillon suffisant pour l'apprenant hiérarchique peut être exponentiellement plus petit que celui de l'apprenant plat, même lorsqu'ils sont entraînés sur la même source de données.
Apprentissage de graphe latent : L'article fournit des taux d'apprentissage pour un élève hiérarchique qui doit inférer des DAG de preuve latents à partir de traces intégrées en utilisant une approche pondérée par l'a posteriori de type EM, tenant compte des erreurs de prédiction de graphe et de la discordance a posteriori.

4. Résultats

Le résultat central est présenté dans le Théorème 6, qui compare les nombres d'échantillons suffisants certifiés ( $\bar{N}$ ) requis pour que les élèves plats et hiérarchiques atteignent un niveau d'échec cible $\delta$ .

Borne plate : $\bar{N}_{flat}(\delta) \propto (L_{flat}/\delta)^{1/(p\gamma)}$
Borne hiérarchique : $\bar{N}_{hier}(\delta) \propto \max(L_{hi}, L_{lo}/\delta)^{1/(p\gamma)}$

Où $L_{flat}$ est la longueur de la trace dépliée et $L_{hier} = L_{hi} + L_{lo}$ est la longueur de la représentation hiérarchique.

L'article démontre que pour une famille de théorèmes indexés par un paramètre de taille/profondeur $D$ , si le processus d'aplatissement fait croître la longueur de la preuve de manière exponentielle ( $L_{flat}/L_{hier} = \exp(\Omega(D))$ ), alors le rapport des échantillons requis croît également de manière exponentielle :
$\bar{N}_{flat}(\delta) / \bar{N}_{hier}(\delta) \geq \exp(\Omega(D))$

Cette séparation découle du fait que l'apprenant plat doit apprendre le même argument local difficile indépendamment pour chaque occurrence, tandis que l'apprenant hiérarchique apprend le bloc partagé une seule fois et le réutilise. L'article utilise un exemple d'élimination des coupures (Annexe G) pour illustrer comment la suppression des lemmes intermédiaires (aplatissement) peut faire exploser la taille de la preuve de manière exponentielle, augmentant ainsi la complexité d'échantillonnage pour les apprenants plats.

5. Signification et affirmations

L'article prétend fournir un mécanisme statistique concret expliquant pourquoi la preuve hiérarchique aide, distinct des arguments de complexité de preuve dans le pire des cas. La signification réside dans l'identification du fait que l'avantage de la décomposition ne réside pas seulement dans le raccourcissement de la dérivation logique, mais dans la réduction du fardeau statistique pesant sur l'apprenant.

Conscience de la distribution de données : Le résultat met en évidence que l'efficacité de l'apprentissage dépend de la structure de la distribution des données. Si les preuves réussies réutilisent des arguments intermédiaires, une représentation hiérarchique capture ce partage, tandis qu'une représentation plate le détruit, conduisant à des tâches d'apprentissage redondantes.
Limites : Les auteurs sont modestes dans leurs affirmations. Ils déclarent qu'il ne s'agit pas d'une borne inférieure dans le pire des cas et que cela n'exclut pas les apprenants plats qui pourraient atteindre une canonicalisation parfaite (reconnaissance parfaite de sous-problèmes identiques sans hiérarchie explicite). La séparation s'applique spécifiquement lorsque l'aplatissement détruit la structure de preuve réutilisable et que la distribution de données contient des preuves où un tel partage est prédominant.
Implication pratique : Les résultats suggèrent que pour la preuve de théorèmes basée sur des vérificateurs, apprendre à prédire des structures de preuve réutilisables (lemmes, sous-objectifs) peut réduire de manière exponentielle la complexité d'échantillonnage requise pour atteindre une probabilité de succès donnée, à condition que le prédicteur de graphe puisse couvrir le certificat de l'enseignant avec une forte probabilité.

L'article conclut que le « détour coûteux » consistant à prouver des lemmes est statistiquement justifié lorsque ces lemmes sont réutilisables, car le coût de les apprendre une seule fois est bien inférieur au coût de les redécouvrir à plusieurs reprises dans un cadre plat.