IA et raisonnement mathématique : ce que les modèles savent vraiment faire

Une IA peut résoudre un problème de mathématiques, rédiger une démonstration convaincante et pourtant avoir tort. Elle peut aussi chercher une preuve pendant des heures, la traduire dans un langage formel et la faire vérifier mécaniquement. Ces deux situations portent le même mot, « raisonnement », mais elles n’offrent pas du tout le même niveau de confiance.

Les progrès sont réels. Des systèmes spécialisés ont atteint le niveau médaille d’argent aux Olympiades internationales de mathématiques, puis des résultats encore plus élevés ont été annoncés sur les éditions suivantes. Mais transformer cette avancée en outil fiable exige de comprendre ce qui produit la réponse : génération en langage naturel, recherche, calcul, code, vérificateur formel ou combinaison de plusieurs briques.

Ce guide explique ce qu’une IA sait réellement faire en mathématiques, pourquoi elle peut halluciner une preuve et comment l’utiliser sans confondre fluidité et exactitude.

Pourquoi les mathématiques sont un test difficile

Une réponse mathématique doit être correcte à chaque étape importante. Une erreur discrète dans un signe, une hypothèse implicite ou un cas oublié peut invalider toute la conclusion.

Le langage naturel tolère parfois l’approximation. Une synthèse peut rester utile même si une phrase est imparfaite. Une preuve ne bénéficie pas de cette marge. Elle doit relier les hypothèses à la conclusion par des transformations valides.

Les mathématiques testent donc plusieurs capacités en même temps :

• comprendre un énoncé ;

• représenter les objets ;

• choisir une stratégie ;

• effectuer des calculs ;

• maintenir une chaîne logique ;

• vérifier les cas particuliers ;

• expliquer le résultat.

Un modèle de langage peut être très bon sur certaines étapes et fragile sur d’autres. C’est pour cela qu’une réponse élégante ne suffit pas.

Trois manières pour une IA de faire des maths

1. Générer une solution en langage naturel

Le modèle prédit une suite de texte plausible à partir de l’énoncé et de ses connaissances. Il peut reconnaître une famille de problèmes, rappeler un théorème et proposer une démonstration.

Cette approche est rapide et flexible. Elle fonctionne bien pour expliquer une notion, proposer une piste ou résoudre des exercices proches de ceux vus pendant l’entraînement.

Sa faiblesse est l’absence de garantie. Une étape peut sembler logique sans être valide. Le modèle peut inventer un lemme, oublier une condition ou conclure trop vite.

2. Utiliser des outils

L’IA peut appeler une calculatrice, exécuter du code, interroger un logiciel de calcul symbolique ou tester des exemples.

L’outil ne remplace pas le raisonnement, mais il réduit certaines erreurs. Un programme peut vérifier une identité sur des valeurs, explorer des cas ou effectuer un calcul long.

Cette méthode est particulièrement utile pour :

• l’arithmétique ;

• les statistiques ;

• l’algèbre symbolique ;

• les simulations ;

• les recherches combinatoires ;

• la vérification de résultats intermédiaires.

Il faut encore contrôler que le bon calcul a été demandé. Un résultat exact produit par le mauvais modèle reste faux pour la question.

3. Produire une preuve formelle

Une preuve formelle est écrite dans un langage interprété par un assistant de preuve comme Lean. Chaque étape doit respecter des règles logiques vérifiées par la machine.

Google DeepMind décrit cette approche avec AlphaProof. Le système traduit des problèmes vers un langage formel, cherche des preuves ou des réfutations et utilise les preuves vérifiées pour améliorer sa recherche.

Le bénéfice est majeur : le vérificateur ne juge pas si le texte semble intelligent. Il contrôle la validité de la preuve dans le cadre formel.

La difficulté se déplace. Il faut formaliser correctement l’énoncé, disposer des bons théorèmes dans la bibliothèque et trouver une preuve dans un espace de recherche immense.

Ce qu’a montré AlphaProof

Lors de l’IMO 2024, AlphaProof et AlphaGeometry 2 ont résolu quatre problèmes sur six selon Google DeepMind. Les solutions ont été évaluées avec les règles de la compétition par des mathématiciens reconnus.

Le système a obtenu 28 points sur 42, soit l’extrémité haute de la catégorie médaille d’argent cette année-là. Le seuil de l’or commençait à 29 points.

Le résultat est impressionnant, mais les détails comptent.

Les problèmes avaient été traduits manuellement en langage formel. Un problème a été résolu en quelques minutes, tandis que d’autres ont demandé jusqu’à trois jours. Les deux problèmes de combinatoire sont restés sans solution.

AlphaProof s’appuyait sur Lean et sur une boucle d’apprentissage par renforcement inspirée d’AlphaZero. AlphaGeometry 2 combinait un modèle de langage et un moteur symbolique spécialisé.

Ce n’était donc pas un chatbot recevant une photo de l’épreuve et répondant comme un élève dans le temps officiel. C’était un système de recherche mathématique spécialisé, doté d’outils et de temps de calcul.

Cette nuance ne réduit pas la performance. Elle explique ce qui l’a rendue possible.

Langage naturel contre preuve formelle

Le langage naturel est souple. Il permet d’explorer une idée, de donner une intuition et de relier des concepts. Mais cette souplesse laisse passer les ambiguïtés.

La preuve formelle est stricte. Chaque symbole a une définition et chaque étape doit être acceptée par le vérificateur. Elle fournit une confiance logique beaucoup plus forte, au prix d’un travail de formalisation.

Les deux approches ne sont pas ennemies.

Un bon workflow peut utiliser le langage naturel pour :

• reformuler le problème ;

• proposer plusieurs stratégies ;

• trouver un exemple ;

• expliquer une preuve ;

• identifier le théorème pertinent.

Puis utiliser un outil formel pour :

• vérifier l’énoncé ;

• contrôler les étapes ;

• révéler une hypothèse manquante ;

• certifier la conclusion.

L’avenir utile ressemble moins à un modèle unique qui « sait tout » qu’à un agent qui choisit les bons outils de raisonnement.

Pourquoi un modèle hallucine une preuve

Il optimise la continuité du texte

Un modèle de langage apprend à produire une suite cohérente. La cohérence stylistique n’est pas la validité logique.

Il reconnaît un problème voisin

Deux énoncés peuvent se ressembler tout en exigeant des conditions différentes. Le modèle applique alors une méthode familière au mauvais cas.

Il saute une étape difficile

La phrase « il est alors évident que » peut cacher le cœur du problème. Un humain fait parfois la même chose, mais l’IA peut employer ce raccourci avec une assurance trompeuse.

Il oublie les domaines de définition

Division par zéro, racine d’un nombre négatif dans les réels, logarithme non défini ou permutation impossible : une manipulation symbolique peut masquer une condition essentielle.

Il invente une référence

Le modèle peut attribuer un résultat à un théorème inexistant ou citer une propriété proche mais différente.

Le remède n’est pas seulement « demande-lui de réfléchir davantage ». Il faut modifier la boucle de vérification.

Comment vérifier une réponse mathématique

Refaire les calculs

Utilise un outil indépendant pour contrôler l’arithmétique, les dérivées, les intégrales ou les résultats numériques.

Tester des cas simples

Choisis des valeurs faciles, des cas limites et des contre-exemples possibles. Une formule générale qui échoue sur un cas élémentaire est immédiatement suspecte.

Exiger les hypothèses

Demande au système de lister le domaine, les conditions et les théorèmes utilisés. Une preuve solide doit dire sous quelles règles elle fonctionne.

Séparer recherche et critique

Fais produire une solution, puis demande une seconde passe consacrée uniquement à la réfutation. Idéalement, utilise un autre modèle ou un outil.

Formaliser quand l’enjeu le justifie

Pour une démonstration importante, la preuve formelle offre un niveau de contrôle supérieur. Ce n’est pas nécessaire pour chaque exercice scolaire, mais c’est précieux pour la recherche, le logiciel critique ou un résultat réutilisé.

Conserver les sources

Si la solution repose sur un théorème, garde une référence fiable. Une page ou un article primaire est plus utile qu’une citation reconstruite de mémoire.

L’IA comme professeur de mathématiques

Pour apprendre, l’IA est souvent plus utile comme tuteur interactif que comme distributeur de réponses.

Elle peut :

• reformuler un concept à plusieurs niveaux ;

• générer un exercice proche ;

• donner un indice sans révéler la solution ;

• analyser une erreur ;

• comparer deux méthodes ;

• construire une progression.

Le meilleur prompt pédagogique ne demande pas « donne-moi la réponse ». Il demande un dialogue qui conserve l’effort de l’élève.

Exemple :

Ne résous pas immédiatement. Demande-moi d’abord ma stratégie, repère la première erreur, puis donne un indice minimal. À la fin, fais-moi reconstruire la solution sans regarder.

Ce cadre change la fonction du modèle. Il ne remplace pas le raisonnement de l’utilisateur. Il l’entraîne.

Il faut toutefois rester vigilant. Une explication fausse mais claire peut ancrer une mauvaise compréhension. Le cours, le professeur ou une source reconnue reste l’autorité.

L’IA pour les étudiants

Un étudiant peut utiliser l’IA sur quatre niveaux.

Compréhension

Demander une autre explication, un dessin mental ou un exemple concret.

Entraînement

Générer des exercices avec difficulté croissante, puis faire contrôler les réponses.

Diagnostic

Présenter sa démarche et demander où apparaît la première erreur, sans réécriture complète.

Vérification

Comparer le résultat avec un calcul indépendant ou une solution officielle.

Le piège est de sauter directement à la solution finale. Tu gagnes cinq minutes et tu perds le mécanisme que l’exercice devait construire.

Une IA pédagogique est utile quand elle réduit la friction sans supprimer l’effort cognitif.

L’IA pour les professionnels

Les mathématiques professionnelles ne ressemblent pas toujours à une Olympiade. Elles apparaissent dans un tableur, une analyse statistique, un modèle financier, une prévision ou une règle de calcul métier.

L’agent peut accélérer :

• l’écriture d’une formule ;

• l’exploration d’un jeu de données ;

• la traduction d’une logique en code ;

• la recherche d’une erreur ;

• la génération de tests ;

• l’explication d’un modèle.

Mais la validation doit suivre l’enjeu.

Pour un tableau interne peu risqué, quelques tests peuvent suffire. Pour une décision financière, médicale ou scientifique, il faut une revue compétente, des sources et des contrôles reproductibles.

L’IA n’a pas besoin d’être infaillible pour être utile. Elle doit être intégrée dans une chaîne où ses erreurs sont détectables.

L’IA peut-elle faire de nouvelles découvertes ?

Oui, certains systèmes ont déjà produit des résultats nouveaux dans des domaines bornés.

Google DeepMind présente par exemple FunSearch comme une méthode combinant un modèle de langage et un évaluateur automatique pour chercher de nouveaux programmes associés à des problèmes mathématiques. Le point déterminant est l’évaluateur : les propositions peuvent être testées au lieu d’être acceptées parce qu’elles semblent plausibles.

Cette architecture contient une leçon générale.

Pour obtenir une découverte fiable, il faut souvent :

1. générer plusieurs candidats ;

2. les tester avec une règle objective ;

3. conserver les meilleurs ;

4. produire de nouvelles variantes ;

5. faire vérifier le résultat.

Le modèle apporte de l’exploration. Le vérificateur apporte de la sélection.

Sans cette seconde brique, une « découverte » peut n’être qu’un texte original et faux.

Raisonnement long : plus de temps suffit-il ?

Donner plus de temps ou plus de calcul peut améliorer les performances. Le système explore davantage de chemins, vérifie certaines étapes ou compare plusieurs réponses.

Mais le temps supplémentaire n’apporte pas une garantie automatique.

Un modèle peut approfondir une mauvaise représentation du problème. Il peut répéter la même hypothèse fausse dans plusieurs formulations. Il peut aussi consommer beaucoup de calcul sur une tâche qu’un outil spécialisé résout immédiatement.

La bonne question est donc : quel budget de raisonnement, quel outil et quel contrôle pour cette mission ?

Pour une addition, utilise un calculateur.

Pour une démonstration exploratoire, utilise plusieurs stratégies.

Pour une preuve importante, utilise un assistant formel.

Pour une explication pédagogique, préserve le dialogue et l’effort.

Construire un agent de raisonnement mathématique

Un agent fiable peut suivre cette architecture.

1. Classifier le problème

Algèbre, géométrie, statistique, optimisation, preuve, calcul numérique ou autre.

2. Définir le niveau de preuve

Intuition, résultat numérique, dérivation détaillée, tests ou preuve formelle.

3. Choisir les outils

Calculatrice, code, solveur symbolique, moteur de recherche documentaire ou assistant de preuve.

4. Produire plusieurs candidats

Une seconde approche peut révéler un conflit ou une hypothèse cachée.

5. Exécuter les vérifications

Tests numériques, cas limites, unités, dimensions, invariants et contrôle formel.

6. Rédiger la réponse

La réponse distingue les faits vérifiés, les hypothèses et les limites.

7. Escalader

Si les méthodes se contredisent ou si l’enjeu est élevé, l’agent demande une revue humaine.

Cette structure ressemble à n’importe quel agent IA utile : source, outils, validation et règle d’arrêt.

Les erreurs de cadrage à éviter

Confondre benchmark et usage quotidien

Résoudre un problème de compétition ne prouve pas qu’un modèle produira un tableur juste sur tes données.

Confondre explication et preuve

Une explication aide à comprendre. Une preuve établit une conclusion dans un cadre défini.

Confondre calcul et décision

Un résultat numérique ne choisit pas automatiquement la bonne hypothèse métier.

Confondre confiance et précision

Le ton du modèle varie peu entre une réponse correcte et une réponse fausse.

Confondre spécialisation et intelligence générale

AlphaProof est construit pour la preuve formelle. Sa performance ne signifie pas que le même système maîtrise n’importe quelle tâche de bureau.

FAQ

ChatGPT est-il fiable en mathématiques ?

Il peut être très utile, mais sa fiabilité dépend du problème, du modèle, des outils et de la vérification. Une réponse non vérifiée ne doit pas être traitée comme une preuve.

Une IA peut-elle remplacer un professeur ?

Elle peut expliquer, entraîner et diagnostiquer. Elle ne remplace pas l’autorité pédagogique, la progression du cours ni la responsabilité d’un professeur.

Pourquoi une IA se trompe sur un calcul simple ?

Un modèle de langage génère du texte. Sans outil de calcul, il peut produire une suite plausible plutôt qu’exécuter une opération fiable.

Une preuve Lean peut-elle être fausse ?

Une preuve acceptée par Lean respecte les règles du système et les définitions utilisées. Une mauvaise formalisation de l’énoncé peut toutefois certifier le mauvais problème.

Comment utiliser l’IA pour progresser ?

Demande des indices, expose ta démarche, fais identifier la première erreur et reconstruis ensuite la solution sans assistance.

À retenir

L’IA mathématique la plus fiable n’est pas celle qui écrit la démonstration la plus élégante. C’est celle qui associe génération, outils et vérification au bon niveau.

Les systèmes modernes savent explorer des stratégies, exécuter du code, utiliser des moteurs symboliques et produire des preuves formelles. Les résultats de DeepMind aux Olympiades montrent que cette combinaison peut atteindre un niveau exceptionnel sur des problèmes très difficiles.

Mais la règle reste simple :

• une réponse fluide n’est pas une preuve ;

• un benchmark n’est pas ton cas d’usage ;

• un calcul exact peut partir d’une mauvaise hypothèse ;

• une vérification indépendante vaut plus qu’une seconde formulation confiante.

Utilise l’IA pour multiplier les pistes, accélérer les calculs et mieux expliquer. Ajoute un vérificateur dès que le résultat compte.

C’est là que le raisonnement assisté devient utile : pas quand la machine paraît certaine, mais quand le système sait prouver pourquoi tu peux lui faire confiance.