💻 computer science

COMPOSE: Composing Future Theorems from Citations and Formal Structure

L'article présente COMPOSE, un cadre à double graphe qui génère des théorèmes mathématiques futurs plausibles en exploitant conjointement les contextes de citations scientifiques et les dépendances formelles des théorèmes, démontrant des performances supérieures grâce à un jeu de données et un benchmark nouvellement construits.

Auteurs originaux : David Busbib, Michael Werman

Publié 2026-05-29

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : David Busbib, Michael Werman

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 essayiez de prédire la prochaine grande percée dans un domaine spécifique des mathématiques. Vous voulez deviner ce qu'un futur article dira, mais vous ne voulez pas simplement inventer des mots mathématiques au hasard. Vous voulez que votre hypothèse soit plausible—c'est-à-dire qu'elle s'inscrive dans la conversation actuelle et qu'elle suive les règles strictes de la logique que les mathématiques exigent.

Cet article présente un nouveau système appelé COMPOSE (Composing Future Theorems from Citations and Formal Structure, soit Composer des théorèmes futurs à partir de citations et de la structure formelle), conçu pour faire exactement cela.

Voici comment cela fonctionne, décomposé en concepts simples :

Le Problème : Deux Cartes Différentes

Pour prédire l'avenir des mathématiques, vous avez généralement besoin de deux choses, mais les outils existants n'en examinent qu'une seule :

La Carte "Sociale" (Citations) : C'est comme observer qui parle à qui lors d'une fête. Si l'article A cite l'article B, ils ont une conversation. Cela vous indique quels sujets sont populaires et où la recherche est en train de se diriger.
La Carte "Logique" (Structure Formelle) : C'est comme le règlement d'un jeu. En mathématiques, vous ne pouvez pas dire n'importe quoi ; vous devez le prouver en utilisant des étapes antérieures. Cette carte montre les dépendances strictes : « Vous ne pouvez prouver le Théorème X que si vous connaissez déjà le Lemme Y. »

Le Problème :

Si vous ne regardez que la Carte Sociale, vous pourriez deviner un sujet qui est populaire mais logiquement impossible (comme essayer de construire une maison sans fondation).
Si vous ne regardez que la Carte Logique, vous pourriez trouver une preuve logiquement parfaite, mais elle pourrait porter sur un sujet dont plus personne ne s'intéresse, ou elle pourrait manquer la « vue d'ensemble » de la direction prise par le domaine.

La Solution : COMPOSE

Les auteurs ont construit un système qui agit comme un traducteur bilingue qui est aussi un détective. Il examine les deux cartes simultanément.

L'Entrée : Vous donnez au système un « Article Ancre » (un article mathématique actuel).
Le Double Graphe :
- Il construit un Graphe Scientifique : Il examine l'Article Ancre et les articles qu'il cite, créant ainsi un réseau d'idées et de conversations.
- Il construit un Graphe Formel : Il prend les théorèmes mathématiques contenus dans ces articles et trouve leurs versions « officielles » dans une immense bibliothèque numérique appelée Mathlib (qui est comme une encyclopédie vérifiée de preuves mathématiques). Il trace ensuite les dépendances logiques entre ces versions officielles.
La Fusion : Le système utilise un « réseau de neurones » spécial (un type d'IA) pour fusionner ces deux cartes. Il apprend comment la conversation (les citations) se connecte aux règles (la logique formelle).
La Sortie : Le système génère une nouvelle affirmation mathématique plausible (un « théorème futur ») qui s'insère dans la conversation actuelle et respecte les règles logiques.

L'Analogie : Prédire le prochain coup aux échecs

Imaginez que vous essayez de prédire le prochain coup dans une partie d'échecs complexe.

Les anciennes méthodes ressemblaient à l'examen d'une liste d'ouvertures d'échecs populaires (la « Carte Sociale »). Elles pouvaient deviner que vous pourriez jouer un « Gambit du Roi », mais elles ne savaient pas si ce coup était légal ou s'il vous ferait échec et mat immédiatement.
COMPOSE est comme un grand maître qui examine à la fois l'histoire de la partie (qui a joué quoi avant) et les règles strictes des échecs (comment les pièces bougent). Il prédit un coup qui n'est pas seulement une stratégie populaire, mais aussi un coup légal et solide qui correspond à l'état actuel du plateau.

Comment ils l'ont testé

Les chercheurs n'ont pas seulement deviné ; ils ont construit un ensemble de tests massif.

Ils ont collecté 108 000 exemples d'articles et de leurs structures logiques formelles correspondantes.
Ils ont créé un « test futur » en utilisant des articles publiés à la fin de 2024 et en 2025 (que le modèle n'avait pas encore vus).
Ils ont demandé au modèle : « À partir de cet ancien article, que dira le prochain article ? »

Les Résultats :

Meilleures hypothèses : COMPOSE était bien meilleur pour deviner le sujet exact du futur article que les autres modèles d'IA.
Plus ancré : Lorsque des juges humains (et d'autres IA) ont examiné la sortie, les hypothèses de COMPOSE ont été mieux notées pour leur profondeur mathématique, leur spécificité et leur exactitude.
L'ingrédient secret : Lorsqu'ils ont désactivé soit la « Carte Sociale », soit la « Carte Logique », le système s'est dégradé. Cela a prouvé que vous avez vraiment besoin des deux pour faire une bonne prédiction.

Une Limitation (Le « Point Aveugle »)

L'article admet une faiblesse : le système repose sur la « Carte Logique » (Mathlib) pour fonctionner. Si un sujet mathématique est très nouveau ou de niche et n'a pas encore été écrit dans la bibliothèque formelle, le système pourrait se confondre et essayer de forcer le nouveau sujet dans une ancienne catégorie sans rapport (comme essayer d'expliquer un nouveau type de musique en utilisant les règles d'un instrument différent).

Résumé

COMPOSE est un outil qui aide à prédire l'avenir des mathématiques en combinant ce dont les mathématiciens parlent avec la façon dont leur logique fonctionne réellement. Il garantit que les prédictions futures ne sont pas simplement un non-sens qui sonne bien, mais qu'elles sont ancrées à la fois dans l'histoire du domaine et dans les règles strictes des mathématiques.

Résumé Technique : COMPOSE – Composition de Théorèmes Futurs à partir de Citations et de Structures Formelles

Définition du Problème

L'article aborde le défi de la génération future de mathématiques ancrée : la tâche de prédire une affirmation mathématique future plausible (une énonciation de type théorème) pour un article « ancre » donné. Les auteurs soutiennent qu'une prédiction valide doit satisfaire deux contraintes simultanées :

Trajectoire Scientifique : Elle doit étendre la direction de recherche indiquée par le graphe de citations scientifiques et l'évolution des idées dans la littérature.
Ancrage Formel : Elle doit respecter les dépendances logiques inhérentes aux mathématiques formelles, garantissant que l'affirmation est déductible de manière valide à partir des définitions, lemmes et théorèmes existants.

Les approches existantes modélisent généralement une seule de ces sources. Les modèles entraînés uniquement sur du texte scientifique peuvent générer des affirmations fluides mais logiquement non ancrées, tandis que les systèmes de preuve de théorèmes raisonnent sur des structures formelles mais manquent du contexte scientifique pour identifier des directions de recherche prometteuses. L'article postule que la combinaison de ces sources complémentaires n'est pas triviale en raison des différences fondamentales dans la façon dont les articles scientifiques et les bibliothèques formelles (comme Mathlib) organisent les connaissances.

Méthodologie : Le Cadre COMPOSE

Les auteurs proposent COMPOSE, un cadre à double graphe qui conditionne un modèle de langage à la fois sur le contexte de citation scientifique et sur la structure formelle des théorèmes. L'approche se compose de trois composants principaux :

1. Construction des Données

Les auteurs ont construit un ensemble de données de 108 000 exemples de graphes scientifiques-formels appariés, dérivés d'articles de mathématiques d'arXiv (2000–2023) et de la bibliothèque Lean Mathlib.

Graphe Scientifique ( $G_s$ ) : Construit à partir d'un article ancre et de son contexte de citation (jusqu'à deux sauts). Il comprend des nœuds abstraits pour les articles et des nœuds de théorèmes extraits du texte. Les arêtes représentent les liens de citation et les dépendances internes aux articles.
Graphe Formel ( $G_f$ ) : Construit en alignant les théorèmes informels extraits sur les théorèmes correspondants dans Mathlib. Cet alignement utilise FrenzyMath (un corpus de descriptions informelles rédigées par des humains pour les théorèmes Mathlib) pour effectuer une recherche informel-vers-informel, évitant ainsi le bruit de l'auto-formalisation directe. Le graphe formel s'étend à partir de la racine du théorème apparié en utilisant des arêtes de dépendance extraites via LeanDojo.
Référence de comparaison (Benchmark) : Un ensemble de test temporellement exclu de 47 000 articles futurs de fin 2024 et 2025, utilisé pour évaluer la capacité du modèle à prédire des résultats réellement publiés.

2. Architecture du Modèle

COMPOSE utilise une architecture à double encodeur suivie d'un décodeur conditionné par le graphe :

Double Encodeur : Deux Réseaux de Neurones à Graphes (GNN) dédiés traitent $G_s$ $G_{s}$ et $G_f$ $G_{f}$ séparément.
- Les nœuds de $G_s$ sont initialisés avec des embeddings E5 (texte scientifique).
- Les nœuds de $G_f$ sont initialisés avec des embeddings DeepSeek-Math (signatures formelles).
- Les deux utilisent un passage de messages dirigé, spécifique au type d'arête, avec des connexions résiduelles à porte.
Module de Fusion : Les représentations des deux graphes sont projetées dans un espace latent partagé et fusionnées via un mécanisme d'attention croisée bidirectionnelle. Cela permet au modèle d'intégrer la direction scientifique avec les contraintes formelles.
Décodeur : Un LLM spécialisé en mathématiques pré-entraîné (DeepSeek-Math-7B ou Mistral-7B) adapté avec LoRA. Des couches d'attention croisée sont insérées dans le décodeur pour conditionner la génération sur les embeddings de graphe fusionnés, permettant au modèle de prêter attention à la structure complète du graphe lors de la génération de tokens.

3. Entraînement en Deux Étapes

Étape 1 (Apprentissage de Représentation) : Les encodeurs de graphes et le module de fusion sont entraînés sans le décodeur en utilisant trois objectifs :
- Prédiction de Lien : Pour s'assurer que les encodeurs capturent la structure du graphe.
- Alignement Contrastif : Pour aligner la représentation de graphe fusionnée avec l'abstract et l'affirmation principale de l'article cible.
- Alignement Croisé : Pour aligner explicitement les nœuds de théorèmes informels avec leurs homologues formels appariés.
Étape 2 (Génération) : Le décodeur est ajouté et affiné en utilisant :
- Perte Autoregressive : Prédiction standard du token suivant.
- Perte de Marge de Graphe : Un terme de régularisation qui pénalise le modèle s'il génère le même texte pour une paire de graphes non appariée, le forçant à s'appuyer sur le contexte spécifique du graphe.

Résultats Clés

Des expériences ont été menées sur la référence de comparaison de 47 000 articles futurs, comparant COMPOSE à des bases de référence solides (incluant GIANTS, FutureGen, GoAI, et diverses variantes uniquement textuelles ou uniquement basées sur des invites).

Performance de Recherche : COMPOSE a obtenu le Gap le plus élevé (0,240), défini comme la différence de similarité cosinus entre le texte généré et le véritable article futur par rapport aux articles non liés. Il surpasse significativement les bases de référence en H@10 (50,8 %) et H@100 (80,8 %), indiquant que ses affirmations générées sont beaucoup plus susceptibles de récupérer le bon article futur dans le pool.
Prédiction d'Affirmation Mathématique Nouvelle (NMCP) : COMPOSE a mené en Précision (0,560) et en Correspondance (0,730), démontrant que ses sorties s'alignent avec les théorèmes futurs aux niveaux formel et informel, et pas seulement thématiquement.
Évaluation par Juge LLM : Un juge LLM (GPT-4.0) a évalué les sorties sur le Contenu, la Profondeur, la Nouveauté, la Précision et la Spécificité. COMPOSE a obtenu le score global le plus élevé (3,36/5), en particulier en Profondeur Technique (3,52) et en Spécificité (3,52), produisant des sorties plus concrètes et mathématiquement riches que les bases de référence qui génèrent souvent des résumés vagues.
Études d'Ablation : La suppression de l'encodeur de graphe scientifique ou formel a provoqué des baisses de performance significatives, confirmant que les deux modalités fournissent des signaux complémentaires. Le graphe formel était crucial pour l'ancrage, tandis que le graphe scientifique était essentiel pour identifier la bonne direction de recherche.

Signification et Affirmations

L'article affirme que la génération future de mathématiques bénéficie de la combinaison du contexte scientifique avec la structure formelle.

Génération Ancrée : Les auteurs démontrent que s'appuyer uniquement sur du texte scientifique conduit à des affirmations thématiquement pertinentes mais logiquement non ancrées, tandis que s'appuyer uniquement sur une structure formelle limite le modèle à des théorèmes connus sans anticiper de nouvelles directions. COMPOSE comble avec succès ce fossé.
Contribution de Données : La construction de l'ensemble de données apparié de 108K et de la référence de comparaison de 47K articles futurs fournit une nouvelle ressource pour évaluer la génération mathématique ancrée, répondant au manque de références temporelles dans ce domaine.
Avance Méthodologique : Le cadre à double graphe avec fusion par attention croisée offre une approche novatrice pour intégrer des sources de connaissances hétérogènes (littérature informelle vs logique formelle) pour des tâches génératives.

Les auteurs notent des limites, spécifiquement que la méthode repose sur un alignement informel-formel approximatif (ce qui peut introduire du bruit dans les domaines où la couverture de Mathlib est faible) et que les affirmations générées ne sont pas vérifiées par un assistant de preuve, s'appuyant plutôt sur la recherche et l'évaluation basée sur LLM comme signaux proxy. Ils suggèrent que des travaux futurs pourraient intégrer une vérification consciente de la preuve pour vérifier directement la correction formelle des affirmations générées.