🤖 AI

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Ce papier présente NSPI, un cadre neuro-symbolique qui exploite les grands modèles de langage pour proposer des conjectures approchées de sommes de carrés et utilise le calcul symbolique pour les affiner en preuves exactes vérifiées par machine dans Lean, permettant ainsi une preuve automatisée évolutive des inégalités polynomiales comportant jusqu'à 10 variables.

Auteurs originaux : Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Publié 2026-05-18

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

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 essayez de prouver qu'un gâteau complexe, à plusieurs couches, est toujours « suffisamment sucré » (mathématiquement, non négatif), peu importe comment vous le coupez ou modifiez ses ingrédients. Dans le monde des mathématiques, cela s'appelle prouver une inégalité polynomiale.

Pendant longtemps, les mathématiciens ont eu deux principales façons de faire cela, mais les deux présentaient des défauts majeurs :

La méthode « Pure Logique » (Symbolique) : C'est comme essayer de résoudre le problème du gâteau en écrivant chaque réaction chimique des ingrédients sur un tableau noir. C'est parfaitement exact, mais si le gâteau a trop d'ingrédients (variables), le tableau se remplit instantanément et la méthode s'effondre. Elle est trop lente et trop désordonnée pour les grands problèmes.
La méthode « Devinettes de l'IA » (LLM) : C'est comme demander à un chef très intelligent et créatif de deviner la recette. Le chef est rapide et bon pour les petits gâteaux, mais lorsque le gâteau devient énorme et compliqué, le chef commence à halluciner des ingrédients qui n'existent pas ou à commettre des erreurs mathématiques. Il ne peut pas prouver que sa réponse est vraie à 100 %.

Cet article présente une nouvelle équipe appelée NSPI (Preuve d'inégalités polynomiales neuro-symbolique). Imaginez NSPI comme un partenariat parfait entre un chef créatif et un inspecteur qualité rigoureux.

Voici comment leur « chaîne de montage » fonctionne, étape par étape :

Étape 1 : Le Chef Créatif (Le LLM)

D'abord, l'équipe demande à un Modèle de Langage (le « Chef ») d'examiner un problème mathématique difficile. Le Chef ne tente pas de faire les calculs difficiles immédiatement. Au lieu de cela, il utilise sa créativité pour deviner une structure.

L'analogie : Imaginez que le Chef dit : « Je parie que ce gâteau est composé de trois couches spécifiques de cubes de sucre empilés ensemble. »
En termes mathématiques, le LLM devine une décomposition en somme de carrés (SOS). Il suggère : « Cette expression compliquée est probablement juste la somme de quelques choses plus simples élevées au carré. »
Point crucial : La devinette du Chef est généralement une approximation. Elle est proche, mais elle peut comporter de minuscules erreurs décimales (comme dire qu'un cube de sucre pèse 1,0000001 gramme au lieu d'exactement 1).

Étape 2 : L'Inspecteur Qualité (Correction Symbolique)

La devinette du Chef est transmise à l'« Inspecteur Qualité », qui est un puissant système d'algèbre informatique.

L'analogie : L'Inspecteur prend l'ébauche approximative du Chef et utilise un microscope pour corriger les minuscules erreurs. Il utilise une technique appelée méthode de Newton (une façon mathématique de zoomer sur la réponse exacte) et la Récupération Rationnelle (transformer des décimales désordonnées en fractions exactes et propres).
Si le Chef a deviné que les couches étaient « approximativement » 1,5, 2,3 et 0,7, l'Inspecteur calcule les nombres exact : 3/2, 23/10 et 7/10.
Maintenant, la devinette a été transformée en un certificat mathématique parfait et exact.

Étape 3 : Le Juge de la Salle d'Audience (Vérification Lean)

Enfin, l'équipe présente ce certificat exact à un « Juge » nommé Lean.

L'analogie : Lean est un juge strict et ininterrompu qui vérifie chaque étape du travail de l'Inspecteur. Il ne se soucie pas de « sentiment » ou de « devinette ». Il n'accepte que des preuves qui sont logiquement infaillibles.
Parce que l'Inspecteur a fourni un certificat exact, le Juge peut facilement vérifier : « Oui, si vous mettez ces nombres exacts au carré et les additionnez, vous obtenez le gâteau original. Et comme les carrés sont toujours positifs, le gâteau est toujours sucré. »
Le Juge émet ensuite une preuve vérifiée par machine garantie à 100 % comme étant correcte.

Pourquoi est-ce une grande nouvelle ?

L'article a testé cette équipe sur 522 problèmes mathématiques très difficiles, certains comportant jusqu'à 10 variables différentes (ingrédients).

Les anciennes méthodes de logique ont abandonné lorsque les problèmes devenaient trop grands (trop d'ingrédients).
Les anciennes méthodes d'IA se sont perdues et ont fait des erreurs sur les grands problèmes.
L'équipe NSPI a réussi là où les autres ont échoué. Ils ont pu résoudre des problèmes avec 10 variables qu'aucune autre méthode ne pouvait aborder.

La Conclusion

L'article affirme qu'en laissant une IA deviner la forme de la solution, puis en utilisant des outils mathématiques pour corriger les détails et un ordinateur pour vérifier la vérité, ils ont construit un système capable de résoudre des problèmes d'inégalités complexes plus rapidement et plus fiablement que jamais auparavant. Ils n'ont pas seulement deviné ; ils ont construit un pont entre une « bonne devinette » et un « fait prouvé ».

Ce qu'ils n'ont PAS affirmé :

Ils n'ont pas dit que cela guérirait des maladies ou prédirait le marché boursier.
Ils n'ont pas affirmé que cela fonctionne pour tous les types de problèmes mathématiques, seulement pour prouver que certaines expressions polynomiales sont toujours positives.
Ils n'ont pas affirmé que cela remplace entièrement les mathématiciens humains, mais plutôt qu'il automatise un type de raisonnement très spécifique et difficile.

Résumé technique : Des conjectures générées par LLM aux formalisations Lean

Énoncé du problème

La preuve automatisée des inégalités polynomiales constitue un défi fondamental en raisonnement mathématique, en particulier pour les cas de grande dimension et multivariés. Les approches existantes rencontrent des limitations significatives en matière d'évolutivité :

Méthodes purement symboliques : Bien qu'elles offrent de solides garanties, les méthodes basées sur la décomposition en somme de carrés (SOS) et la programmation semi-définie (SDP) souffrent d'une explosion combinatoire et d'une croissance rapide des expressions intermédiaires à mesure que le nombre de variables ou le degré augmente. Elles échouent souvent à produire des preuves structurées et lisibles par un humain.
Méthodes purement basées sur les LLM : Les grands modèles de langage (LLM) intégrés à des assistants de preuve (par exemple, Lean, Isabelle) ont montré des promesses, mais sont limités par la rareté des données d'entraînement formalisées de haute qualité. Ils peinent avec les inégalités algébriques complexes, en particulier celles dépassant 5 variables, et manquent souvent de la capacité à générer des certificats rigoureux et vérifiables par machine.

Le défi central consiste à combler le fossé entre la découverte heuristique et la vérification formelle rigoureuse, permettant la preuve automatisée d'inégalités polynomiales non contraintes dans des contextes de grande dimension (jusqu'à 10 variables) avec une correction vérifiée par machine.

Méthodologie : Cadre NSPI

Les auteurs proposent NSPI (Preuve d'inégalités polynomiales neuronale-symbolique basée sur SOS), un cadre qui intègre les forces complémentaires des LLM et du calcul symbolique dans un pipeline de bout en bout. Le processus se compose de trois étapes principales :

1. Conjecture neuronale (Génération SOS guidée par LLM)

Au lieu d'utiliser les LLM uniquement pour guider la recherche, NSPI les élève au rang de générateurs principaux de conjectures.

Construction des données : Les auteurs construisent un jeu de données à grande échelle de paires polynôme non négatif–SOS en utilisant deux stratégies novatrices :
- Piloté par le calcul : Génération de matrices de Gram par décalage spectral ou optimisation LMI pour assurer la semi-définition positive (PSD) avec des coefficients contrôlés.
- Piloté par la structure : Exploitation de structures algébriques telles que les matrices à dominance diagonale (dd) et à dominance diagonale mise à l'échelle (sdd), qui garantissent les propriétés PSD par conception.
Entraînement : Un schéma d'entraînement en deux étapes est employé :
- Démarrage à froid : Affinement supervisé (SFT) sur plus d'un million de paires polynôme-SOS synthétiques pour établir un raisonnement structurel fondamental.
- Apprentissage par renforcement progressif : L'optimisation de politique relative de groupe basée sur un curriculum (GRPO) est appliquée à des instances difficiles (augmentation du nombre de variables de 3–5 à 9–10). La fonction de récompense combine la précision (fidélité numérique), le respect du format et des pénalités de structure algébrique pour garantir que le LLM génère des structures SOS plausibles.
Sortie : Le LLM propose une décomposition SOS approximative (une somme de termes carrés) pour un polynôme donné.

2. Correction symbolique (Récupération rationnelle exacte)

Pour transformer la conjecture approximative du LLM en une preuve rigoureuse, un module de correction symbolique affine la sortie :

Raffinement Gauss-Newton : La structure SOS approximative est affinée à l'aide de méthodes itératives de type Newton pour minimiser l'erreur arrière entre la somme de carrés conjecturée et le polynôme cible. Cela produit une matrice de Gram numérique de haute précision.
Récupération rationnelle : La matrice numérique est convertie en une matrice PSD rationnelle exacte. Selon que la solution se trouve à l'intérieur ou sur la frontière du cône PSD, le système emploie une projection orthogonale ou une factorisation LDL $^\top$ tronquée combinée à une approximation diophantienne simultanée. Cette étape garantit que le certificat SOS résultant est exact et exempt d'erreurs d'virgule flottante.

3. Vérification formelle (Génération de preuve Lean)

Le certificat SOS rationnel exact est automatiquement converti en une preuve Lean vérifiable par machine.

Modèles de preuve : Des modèles Lean prédéfinis sont remplis avec les termes SOS exacts.
Vérification : Le prouveur Lean vérifie deux conditions :
1. Égalité : Le polynôme cible est égal à l'expression SOS développée (vérifié via linear_combination).
2. Non-négativité : L'expression SOS est non négative (vérifiée via la tactique positivity, qui applique récursivement des règles telles que $x^2 \ge 0$ ).

Contributions clés

Pipeline neuro-symbolique : La proposition de NSPI, un cadre de bout en bout qui automatise la génération de preuves formelles complètes pour les inégalités polynomiales en enchaînant la conjecture neuronale, la correction symbolique et la vérification formelle.
Pont de fiabilité principiel : Une méthode novatrice pour intégrer la génération heuristique basée sur les LLM avec une certification exacte symbolique. Cela transforme les conjectures neuronales en preuves vérifiables par machine, permettant l'évolutivité vers des cas multivariés de grande dimension (jusqu'à 10 variables) sans dépendre de quantités massives de données d'entraînement formalisées préexistantes.
Référence et évaluation : La construction de PolyIneqBench, une référence exigeante contenant 522 problèmes d'inégalités (3 à 10 variables), incluant des problèmes de compétition réels et des instances synthétiques de grande dimension. Des expériences extensives démontrent que NSPI surpasse les solveurs symboliques de l'état de l'art (Maple, Z3), les prouveurs LLM purs (DeepSeek-Prover-V2, Goedel-Prover) et les systèmes hybrides existants (LIPS), en particulier dans les scénarios de grande dimension.

Résultats expérimentaux

Performance : Sur PolyIneqBench, NSPI a atteint un taux de réussite de 11,7 % pour les problèmes à 10 variables, tandis que les méthodes symboliques (Maple, Z3) et les prouveurs LLM purs sont tombés à près de 0 % ou à des chiffres uniques.
Efficacité : NSPI a maintenu le temps d'exécution moyen le plus faible parmi les solveurs réussis, démontrant une accélération de plus de 10 fois par rapport à plusieurs prouveurs basés sur les LLM.
Évolutivité : La stratégie d'apprentissage par renforcement progressif a réussi à déplacer la limite des capacités du modèle vers des dimensions plus élevées, avec des gains de performance observés à mesure que le curriculum passait de 3–5 variables à 9–10 variables.
Ablation : Les expériences ont confirmé que l'entraînement de démarrage à froid synthétique et le GRPO basé sur un curriculum sont tous deux critiques pour le succès du système.

Importance et affirmations

L'article affirme établir un nouveau paradigme dans la preuve de théorèmes neuro-symbolique où les LLM fonctionnent comme des moteurs de conjecture symbolique centraux plutôt que de simples guides de recherche. En traitant les LLM comme des générateurs de priors symboliques (structures SOS) et en s'appuyant sur le calcul symbolique pour la précision et la vérification formelle pour la correction, l'approche résout le goulot d'étranglement de la rareté des données des méthodes neuronales pures et les limites d'évolutivité des méthodes symboliques pures.

Les auteurs positionnent NSPI comme une extension significative de la frontière de la preuve automatisée d'inégalités polynomiales, gérant avec succès des cas de grande dimension (jusqu'à 10 variables) qui étaient auparavant intraitables pour les systèmes automatisés existants. Le travail démontre que la combinaison de la découverte heuristique avec une certification rigoureuse peut considérablement élargir la portée pratique du raisonnement mathématique automatisé.