🤖 AI

ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction

L'article présente ALPS, un nouveau benchmark qui mesure rigoureusement la créativité valide dans les grands modèles de langage en leur demandant de générer des preuves ou des constructions mathématiques originales et vérifiables pour des lois équationnelles générées aléatoirement, révélant que les modèles actuels éprouvent des difficultés significatives avec le côté construction et que la plupart des instances restent non résolues même par des prouveurs automatisés avancés.

Auteurs originaux : Eric Xie, Wenqian Ye, Aidong Zhang

Publié 2026-08-18

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Eric Xie, Wenqian Ye, Aidong Zhang

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

Dans le paysage scientifique moderne, l'intelligence artificielle a commencé à sortir de son rôle de processeur de données pour endosser celui de découvreuse. Nous voyons des machines capables de proposer de nouveaux composés chimiques, de suggérer de nouveaux matériaux et même de formuler des conjectures mathématiques que les humains n'ont pas encore envisagées. Ce changement soulève une question profonde : lorsqu'une machine produit une réponse qui ressemble à une percée, comment savoir s'il s'agit d'une véritable créativité ou simplement d'une répétition habile de quelque chose qu'elle a mémorisé lors de son entraînement ? La véritable créativité en science exige deux choses : la solution doit être originale, ce qui signifie qu'elle n'a jamais été vue auparavant, et elle doit être efficace, ce qui signifie qu'elle fonctionne réellement et résout le problème posé. La difficulté réside dans la vérification de ces qualités. Dans de nombreux domaines, juger si une nouvelle idée est valide nécessite que des experts humains examinent le résultat et décident s'il est bon, un processus qui est lent et subjectif. En mathématiques, où les réponses peuvent être vérifiées avec une certitude absolue, le défi est différent : les problèmes sont souvent si complexes qu'un ordinateur ne peut pas simplement parcourir toutes les possibilités pour trouver la réponse, et les problèmes eux-mêmes sont souvent des ensembles fixes que la machine pourrait déjà avoir étudiés.

Pour résoudre ce dilemme, des chercheurs de l'Université de Virginie ont développé une nouvelle façon de tester l'intelligence artificielle, un banc d'essai qu'ils appellent ALPS. Ce système est conçu pour mesurer la « créativité valide » en présentant à la machine un type spécifique de casse-tête mathématique qui ne peut être résolu par la mémoire ou en suivant une routine standard. Les casse-têtes sont basés sur des règles de combinaison d'un ensemble d'éléments. Imaginez une collection d'objets et une règle pour mélanger n'importe quels deux d'entre eux. Les chercheurs génèrent une règle spécifique, ou loi, qui décrit comment ces objets doivent se comporter. La tâche de la machine est de décider de l'une de deux choses : soit la règle est si restrictive qu'elle force tous les objets à être identiques, soit la règle permet une structure complexe et infinie d'objets qui satisfait la condition. Si la machine affirme que la structure existe, elle doit construire une description de celle-ci. Si elle affirme que les objets doivent être identiques, elle doit prouver qu'aucune autre possibilité n'existe. Le génie de cette configuration est que les réponses peuvent être vérifiées par un ordinateur avec une précision parfaite, sans qu'aucun humain ait besoin d'examiner le résultat. De plus, le système peut générer une source infinie de ces casse-têtes, garantissant que la machine soit toujours confrontée à un problème qu'elle n'a jamais rencontré auparavant.

Les chercheurs ont testé ce système en utilisant une variété d'outils de raisonnement automatisés puissants, qui sont des programmes informatiques spécialisés conçus pour résoudre des problèmes logiques. Ils ont soumis ces outils à un ensemble de plus de quatre mille lois générées. Les résultats sont frappants. Même avec une augmentation massive de la puissance de calcul, les outils automatisés n'ont pu résoudre qu'une infime fraction des problèmes. Plus précisément, un portefeuille de huit configurations différentes des meilleurs prouveurs disponibles n'a réussi à résoudre qu'environ deux pour cent des lois. Lorsque les chercheurs ont augmenté le budget informatique par vingt, ils n'ont trouvé qu'une poignée de solutions supplémentaires, et aucune d'entre elles n'était la structure complexe qu'ils recherchaient ; il ne s'agissait que de preuves que les objets devaient être identiques. Cela suggère que la barrière à la résolution de ces problèmes n'est pas un manque de puissance de calcul, mais un manque de méthode pour inventer les structures spécifiques et sur mesure que chaque loi unique requiert. La machine ne sait tout simplement pas comment construire la bonne sorte de structure infinie à partir de rien.

Les chercheurs se sont ensuite tournés vers les grands modèles de langage, le type d'intelligence artificielle qui alimente de nombreux outils conversationnels utilisés aujourd'hui. Ils ont testé les modèles de raisonnement les plus puissants disponibles, en leur donnant les mêmes casse-têtes et les mêmes chances de prouver leurs réponses. Du côté de la tâche où la machine devait prouver que tous les objets étaient identiques, le meilleur modèle a réussi dans environ quatorze pour cent des cas, mais seulement sur les problèmes les plus simples. Du côté où la machine devait construire une nouvelle structure infinie, les résultats étaient encore plus révélateurs : aucun des modèles n'a réussi. Lorsque les modèles tentaient de construire une structure, ils échouaient systématiquement de deux manières : soit ils proposaient une structure trop rigide, faisant s'effondrer tous les objets en un seul point et échouant ainsi à montrer une solution complexe, soit ils proposaient une structure trop lâche, ne respectant pas les règles de la loi qu'ils tentaient de satisfaire. Dans chaque instance, la machine ne parvenait pas à équilibrer le besoin de suivre les règles et le besoin de créer quelque chose de nouveau et de complexe.

L'étude conclut que, bien que ces systèmes d'intelligence artificielle s'améliorent pour suivre des instructions et vérifier leur propre travail, ils luttent encore avec l'acte fondamental de la découverte scientifique : inventer une nouvelle structure qui s'adapte à un ensemble de contraintes. Les chercheurs ont rendu public l'intégralité de leur système, y compris le générateur qui crée les casse-têtes et le juge automatisé qui vérifie les réponses. Cela permet à d'autres scientifiques de continuer à tester et à améliorer ces modèles sans manquer de nouveaux problèmes. Les conclusions suggèrent que la voie à suivre pour l'IA en science ne consiste peut-être pas à donner aux machines plus de données ou plus de temps, mais à leur apprendre à proposer et à affiner leurs propres idées dans une boucle de création et de vérification. Tant que les machines ne pourront pas construire de manière fiable ces solutions sur mesure, leur rôle dans la découverte scientifique restera limité, incapable de franchir le fossé entre le traitement de l'information et la génération d'une connaissance véritablement valide et originale.

Résumé Technique : ALPS – Mesurer la créativité valide dans les grands modèles de langage par construction mathématique

1. Énoncé du problème

Les évaluations actuelles des grands modèles de langage (LLM) dans les domaines scientifiques (par exemple, la démonstration de théorèmes, la conception de molécules) peinent à distinguer la créativité valide de la simple mémorisation ou de l'exécution routinière. Une solution est considérée comme « validement créative » uniquement si elle satisfait deux critères conjoints :

Originalité : La solution n'est pas une répétition de données d'entraînement ou d'une procédure générale connue.
Efficacité : La solution est objectivement correcte et apporte une valeur ajoutée pour la tâche spécifique.

Les benchmarks existants échouent à mesurer cette combinaison de manière fiable car ils manquent au moins l'une des trois propriétés nécessaires :

Vérifiabilité : Les solutions doivent être objectivement vérifiables (non sujettes à un jugement subjectif).
Renouvelabilité : De nouvelles instances de problèmes doivent être générables sans limite pour éviter la contamination par les données d'entraînement.
Constructivité : La tâche doit exiger une solution adaptée à l'instance spécifique, empêchant les solutions par mémoire ou algorithmes standards.

Les corpus statiques (ex. MATH, miniF2F) échouent sur la renouvelabilité ; les puzzles synthétiques (ex. SAT aléatoire) échouent souvent sur la constructivité car ils peuvent être résolus par des procédures connues ; et les tâches de découverte ouverte (ex. conception de molécules) échouent souvent sur la vérifiabilité en raison du jugement humain subjectif.

2. Méthodologie : Le benchmark ALPS

Les auteurs introduisent ALPS (Austin-Law Proof-Synthesis), un benchmark conçu pour remplir simultanément ces trois propriétés dans le domaine de la théorie équationnelle.

Formulation du problème :

Domaine : ALPS opère sur des magmas (ensembles avec une opération binaire unique $\diamond$ ) et des lois équationnelles (identités universellement quantifiées).
Tâche : Chaque instance est une loi $L$ de la forme $x = T[x, y, z, \dots]$ , où $T$ est un terme d'ordre cinq ou plus.
La dichotomie : Pour toute loi de ce type, exactement une de deux conditions est vraie :
1. Triviale : La loi entraîne $x = y$ , faisant s'effondrer tout modèle en un élément unique.
2. Austin : La loi possède un modèle non trivial, qui doit nécessairement être infini (puisque tous les modèles finis non triviaux sont écartés par le processus de certification du benchmark).
Le défi : Le solveur doit soit fournir une preuve déductive que $L \models x=y$ (côté Trivial), soit construire un magma infini satisfaisant $L$ (côté Austin).

Construction du corpus :

Génération : Le corpus est développé via un moteur d'extension. En partant de lois Austin connues, les variables dans le terme $T$ sont remplacées de manière récursive par de nouvelles opérations (ex. $v \to v \diamond w$ ). Cela garantit que des problèmes frais et inédits peuvent être générés indéfiniment.
Filtrage et admissibilité : Les candidats passent par un pipeline de filtrage rigoureux :
1. Filtre de modèle fini : Écarte les lois possédant des modèles finis non triviaux.
2. Proveur d'admissibilité : Utilise des prouveurs automatisés pour certifier qu'aucun modèle fini non trivial n'existe. Cela repose sur une conséquence logique de la finitude : sur un ensemble porteur fini, une application injective est surjective. Le prouveur tente de dériver une contradiction à partir de la loi et de la surjectivité d'un sous-terme, certifiant que tout modèle doit être infini.
3. Déduplication : Les lois équivalentes (s'impliquant mutuellement) sont regroupées en classes d'équivalence pour garantir des comptes de problèmes distincts.
Pool résultant : À partir d'une génération initiale de candidats, les auteurs ont produit un pool de 4 141 lois non résolues (le « palier difficile ») ainsi qu'un ensemble plus restreint de lois « certifiées faciles ».

Vérification des réponses (Le juge automatisé) :
Le juge vérifie les soumissions via deux canaux distincts, entièrement automatisés et sans intervention humaine :

Côté Trivial : Le LLM soumet une chaîne d'égalités. Un harnais l'auto-formalise en une preuve Lean (vérifiée par le noyau de Lean) pour vérifier que $L \implies \forall a, b: a=b$ .
Côté Construction : Le LLM soumet un ensemble fini d'équations $E$ $E$ (une présentation). Le juge vérifie deux affirmations en utilisant des prouveurs de théorèmes automatisés (ex. Vampire, E, Twee) :
- Dérivation : $E \vdash L$ (Tout modèle de $E$ satisfait $L$ ).
- Satisfiabilité : $E \cup \{a \neq b\}$ est satisfaisable (Il existe un modèle de $E$ avec au moins deux éléments distincts).
- Si les deux sont vraies, le certificat d'admissibilité de l'instance garantit que le modèle est infini.

3. Contributions clés

Une tâche de construction à deux faces : Un benchmark où chaque instance est certifiée pour avoir une réponse déterminée (soit triviale, soit infinie), isolant ainsi le besoin de construction créative.
Corpus renouvelable et générateur : Un générateur public qui crée de nouvelles instances sans limite, garantissant que l'évaluation n'est jamais contaminée par les données d'entraînement.
Juge automatisé : Un système qui certifie les soumissions via des canaux indépendants (Lean pour la trivialité, certificats de prouveurs automatisés pour la construction) sans juges humains.
Ligne de base automatisée forte : Un portfolio de huit configurations de prouveurs de pointe (Vampire, E, Twee) qui établit la limite actuelle de l'automatisation liée aux méthodes (« method-bound »).

4. Résultats expérimentaux

Performance des prouveurs automatisés :

Un portfolio de huit configurations n'a résolu que 2,2 % du pool d'évaluation de 4 141 lois.
Augmenter le budget de calcul par un facteur de 20 n'a ajouté que 0,6 % de lois résolues supplémentaires (toutes des preuves de trivialité, aucune nouvelle construction de modèle).
97,2 % du pool reste non résolu par toute configuration testée, indiquant que l'obstacle est l'absence de méthodes pour construire des structures infinies sur mesure, et non un manque de puissance de calcul.
Résultat secondaire : Les auteurs ont résolu une loi d'ordre 5 précédemment laissée ouverte par l'Equational Theories Project (ETP), confirmant l'existence d'un modèle infini via la saturation.

Performance des LLM :

Côté Trivial : Sur un ensemble de 63 lois « certifiées faciles », le modèle le plus puissant testé (o3) a atteint un taux de réussite de 14 % (9 solutions) avec des points de passage (lemmes dérivés du prouveur) et 9,5 % sans eux. GPT-4.1 et o4-mini ont obtenu 0 %.
- Mode d'échec : Les LLM ont principalement échoué en soumettant des chaînes contenant des étapes invalides (étapes non dérivables de la loi), que le harnais a rejetées.
Côté Construction : Sur un échantillon de 25 lois du « palier difficile » (non résolues par l'automatisation), aucun LLM n'a produit de solution vérifiée.
- Mode d'échec : Les soumissions étaient soit trop fortes (impliquaient la loi mais s'effondraient en un seul élément, échouant au test de distinction) soit trop faibles (permettaient des éléments distincts mais ne parvenaient pas à impliquer la loi).
- o3 a réussi exactement l'un des deux tests sur l'ensemble des 25 lois. o4-mini et GPT-4.1 ont échoué aux deux tests sur de nombreuses lois.

5. Signification et affirmations

L'article affirme qu'ALPS parvient à isoler la créativité valide en éliminant les biais de mémorisation et d'exécution routinière.

Nécessité de la créativité : Le taux d'échec élevé des prouveurs automatisés et des LLM sur le « palier difficile » démontre que ces problèmes ne peuvent être résolus par les procédures générales existantes ou la recherche par force brute.
Nature de l'échec : Les profils d'échec spécifiques (étapes invalides dans les preuves de trivialité ; présentations « trop fortes/trop faibles » dans la construction) soulignent que les modèles actuels peinent avec la génération créative sous contraintes. Ils peuvent souvent esquisser une structure, mais échouent à équilibrer les spécifications globales sans basculer dans des solutions dégénérées.
Parallèle scientifique : L'article établit un parallèle avec le cycle « spécifier–construire–vérifier » de la découverte scientifique (ex. conception de molécules), notant qu'ALPS rend chaque phase vérifiable par machine.
Direction future : Les auteurs suggèrent que la voie à suivre réside dans les boucles « vérifier et affiner » (similaires à la synthèse inductive guidée par contre-exemple, CEGIS), où les solveurs esquissent des structures, reçoivent un feedback automatisé sur leur validité, puis les révisent.

Les auteurs restent modestes, notant que bien que les LLM les plus puissants montrent une certaine capacité sur les instances faciles, ils échouent actuellement à construire des structures infinies valides sur les instances difficiles, et que le benchmark reste largement non résolu par la technologie actuelle.