LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Ce papier présente LeanTutor, un système de tutorat mathématique basé sur l'IA qui combine les forces des grands modèles de langage et des prouveurs de théorèmes pour fournir des preuves vérifiables, évalué grâce à un nouveau jeu de données nommé PeanoBench.

L'essentiel

🎓 LeanTutor : Le Tuteur Mathématique "Infaillible"

Imaginez que vous apprenez à jouer du piano. Vous avez deux options pour vous aider :

1. Un ami très bavard (l'IA classique) : Il vous donne des conseils super gentils, mais il peut se tromper de note, inventer des mélodies qui n'existent pas, ou vous donner la réponse complète avant même que vous ayez essayé. C'est comme un ami qui chante faux mais avec beaucoup de confiance.
2. Un métronome robotique (le prouveur de théorèmes) : Il est parfait. Il ne se trompe jamais. Mais il est très strict, parle un langage incompréhensible (des codes bizarres) et ne vous explique pas pourquoi vous avez raté votre note. C'est frustrant pour un débutant.

LeanTutor, c'est le mariage parfait entre ces deux mondes. C'est un tuteur qui parle comme un humain (en langage naturel) mais qui vérifie chaque étape avec la rigueur d'un robot infaillible.

🧩 Comment ça marche ? (Les 3 Super-Pouvoirs)

Le système est composé de trois modules qui travaillent ensemble, comme une équipe de trois experts :

1. Le Traducteur (L'Autoformalisateur) :

   • Le problème : Vous écrivez votre preuve en français ("Je suppose que X est vrai..."). L'ordinateur, lui, ne comprend que le "Lean" (un langage de code très précis).
   • La solution : Ce module traduit instantanément vos mots en code Lean. C'est comme un interprète qui écoute votre conversation et la transcrit en temps réel pour le robot.

2. Le Gardien du Code (Le Vérificateur) :

   • Le problème : Les IA classiques (comme ChatGPT) peuvent halluciner et dire "C'est bon !" alors que c'est faux.
   • La solution : Le robot Lean vérifie chaque phrase traduite. Si vous faites une erreur de logique, le robot dit : "Non, ça ne compile pas". Il ne ment jamais.

3. Le Coach Bienveillant (Le Générateur de Feedback) :

   • Le problème : Si le robot dit juste "Erreur", vous ne comprenez pas pourquoi.
   • La solution : Le tuteur analyse l'erreur et vous donne un indice en français. Au lieu de vous donner la réponse, il vous dit : "Hé, regarde ta base de départ, tu as oublié un petit détail ici". Il vous guide sans tricher.

🛠️ L'Expérience : Le "Jeu des Nombres Naturels"

Pour tester ce système, les chercheurs ont créé un terrain de jeu appelé PeanoBench.
Imaginez un jeu vidéo éducatif où l'on doit prouver des règles de base de l'arithmétique (comme "l'addition est commutative", c'est-à-dire que 2+3 = 3+2).

• Ils ont pris 371 niveaux de ce jeu.
• Pour chaque niveau, ils ont une solution parfaite (écrite par des experts) et des centaines de tentatives d'étudiants (parfois correctes, parfois pleines d'erreurs logiques).
• Ils ont demandé à LeanTutor de corriger ces tentatives.

📊 Les Résultats : Ce qui a bien fonctionné (et ce qui reste difficile)

Les bonnes nouvelles :

• Pas d'hallucinations : Contrairement aux IA classiques, LeanTutor ne vous donne jamais de fausses réponses. Si c'est faux, il le sait.
• Meilleur que la base : Quand on compare LeanTutor à une IA standard, LeanTutor identifie mieux les erreurs et donne des conseils plus pertinents.
• Le secret du succès : Le système fonctionne mieux quand il a une "solution de référence" (la réponse du prof) sous les yeux pour comparer avec ce que l'étudiant écrit.

Les défis restants (Les limites) :

• La traduction est fragile : Si un étudiant écrit une phrase très bizarre ou mal structurée, le "Traducteur" peut se tromper en passant du français au code. Si la traduction est fausse, le robot pense que l'étudiant a fait une erreur alors qu'il n'a fait que mal s'exprimer.
• Pas encore pour les maths complexes : Pour l'instant, ça marche bien sur des maths de niveau lycée/université débutant (arithmétique de Peano). Pour des maths très avancées, le système doit encore apprendre.

💡 En résumé

LeanTutor, c'est comme avoir un professeur de maths qui a lu tous les livres de la bibliothèque (grâce à l'IA) mais qui possède aussi une règle magique qui ne permet aucune erreur (grâce au prouveur Lean).

Son but n'est pas de faire les devoirs à votre place, mais de vous tenir la main pour que vous trouviez la solution par vous-même, en s'assurant que chaque pas que vous faites est mathématiquement vrai. C'est une étape vers un futur où l'IA nous aide à apprendre à penser, et pas seulement à copier.

Résumé technique

Voici un résumé technique détaillé du papier "LeanTutor: Towards a Verified AI Mathematical Proof Tutor", présenté en français.

1. Problématique

L'utilisation croissante des Modèles de Langage (LLM) comme ChatGPT ou Claude dans l'éducation pose un problème majeur pour l'apprentissage des preuves mathématiques. Bien que ces modèles permettent une communication fluide en langage naturel, ils souffrent de plusieurs défauts pédagogiques et techniques :

• Tendance aux hallucinations : Ils génèrent souvent des réponses convaincantes mais incorrectes.
• Manque de rigueur : Ils ont du mal à identifier les erreurs de raisonnement et ne fournissent pas toujours la justification logique correcte.
• Pédagogie inadaptée : Ils tendent à donner directement la réponse plutôt que de guider l'étudiant vers la découverte, ce qui nuit au développement de la pensée critique.

À l'inverse, les prouveurs de théorèmes formels (comme Lean) garantissent une correction absolue, mais leur syntaxe complexe et leur courbe d'apprentissage abrupte les rendent inaccessibles à la plupart des étudiants.

Le défi central est donc de créer un tuteur intelligent capable de combiner la fluidité du langage naturel des LLMs avec la rigueur vérifiable des prouveurs de théorèmes, sans exiger de l'étudiant qu'il maîtrise la syntaxe formelle.

2. Méthodologie : Le système LeanTutor

Les auteurs proposent LeanTutor, un système de preuve de concept qui orchestre trois modules interconnectés pour interagir avec l'étudiant en langage naturel tout en utilisant Lean en arrière-plan pour la vérification.

Architecture du système

1. Autoformalisateur / Vérificateur de preuves :

   • Il convertit les étapes de preuve écrites en langage naturel (NL) par l'étudiant en code Lean (FL) étape par étape.
   • Il compile chaque étape via l'outil LeanInteract.
   • Si la compilation échoue (erreur de syntaxe ou de logique), le système identifie l'étape comme erronée.
   • Innovation clé : Contrairement aux approches précédentes qui tentent de formaliser une preuve entière d'un coup, LeanTutor procède étape par étape, ce qui permet une détection plus fine des erreurs et une meilleure gestion des preuves incomplètes.

2. Générateur de prochaine étape (Next Step Generator - NSG) :

   • Activé lorsque la preuve est incomplète ou incorrecte.
   • Il effectue une recherche en profondeur (Depth-First Search) dirigée par un LLM pour trouver une tactique Lean valide qui mène à la preuve complète.
   • Il génère 12 tactiques candidates, les filtre via une "vérification de progression" (pour éviter les boucles et l'utilisation de théorèmes interdits) et construit un arbre de recherche jusqu'à trouver une preuve valide (limitée à une profondeur de 8).

3. Générateur de feedback en langage naturel :

   • Il synthétise les informations des modules précédents (l'erreur détectée, le message d'erreur du compilateur Lean, et la prochaine étape valide générée).
   • Il produit trois types de retours pédagogiques :
     1. Identification de l'erreur : Explique pourquoi l'étape est fausse.
     2. Indice / Question : Guide l'étudiant sans donner la réponse (scaffolding).
     3. Étape explicite : Donne la prochaine action possible (similaire à un "bottom-out hint").

Données : PeanoBench

Pour entraîner et évaluer le système, les auteurs ont créé PeanoBench, un jeu de données de 371 preuves d'arithmétique de Peano.

• Source : Dérivé du "Natural Numbers Game" (NNG4).
• Structure : Chaque preuve possède une version en langage naturel et une version formelle équivalente en Lean.
• Variété : Le dataset inclut des preuves correctes (générées selon des "personas" : style algébrique ou style justifié) et des preuves incorrectes générées algorithmiquement en sautant des étapes logiques pour simuler des erreurs d'étudiants.

3. Contributions Clés

• Cadre hybride LLM-Prouveur : Une architecture qui délègue la vérification de la vérité mathématique au prouveur formel (Lean) tout en utilisant le LLM pour l'interface utilisateur et la génération de feedback pédagogique.
• Approche étape par étape : Une méthode d'autoformalisation incrémentale qui surpasse les approches de "preuve entière" pour gérer les erreurs partielles et les preuves non terminées.
• Nouvelle métrique d'évaluation : Les auteurs proposent une métrique de "correspondance détendue" (relaxed exact matching) pour évaluer la fidélité de l'autoformalisation. Cette métrique compare non seulement les chaînes de caractères des tactiques, mais aussi les états de preuve (proof states) après exécution, en normalisant les noms de variables pour ignorer les différences syntaxiques mineures.
• Dataset PeanoBench : Une ressource publique avec des preuves alignées NL/FL et des erreurs simulées, spécifiquement conçue pour le tutorat.

4. Résultats Expérimentaux

Les expériences ont été menées sur le modèle gpt-4o-mini avec une évaluation humaine par des enseignants de mathématiques.

• Performance d'Autoformalisation :

  • L'ajout de la "Solution du personnel" (Staff Solution) comme contexte améliore considérablement la précision (passant de ~33% à ~57% pour les tactiques correctes).
  • L'approche étape par étape surpasse l'approche "preuve entière" de 8% sur les preuves incorrectes, ce qui est crucial pour un système de tutorat.
  • Le système montre une forte dépendance à la solution de référence fournie en contexte, ce qui limite sa capacité à formaliser des preuves dont la structure diffère radicalement de la référence.

• Qualité du Feedback (Évaluation Humaine) :

  • LeanTutor surpasse la ligne de base (un LLM simple recevant la preuve erronée) sur les axes de Précision (Accuracy) et de Pertinence (Relevance).
  • Les scores de Lisibilité et de Fuite de réponse (Answer Leakage) sont comparables entre les deux modèles.
  • Note importante : L'évaluation par "LLM-as-a-judge" (gpt-4) a donné des résultats contradictoires (favorisant la ligne de base), soulignant la nécessité d'évaluations humaines pour les tâches pédagogiques complexes.

5. Signification et Perspectives

Ce travail démontre la faisabilité d'un tuteur de preuves mathématiques vérifié formellement.

• Impact Éducatif : Il offre une solution de compromis ("happy medium") permettant aux étudiants de bénéficier d'un feedback instantané et privé sans sacrifier la rigueur mathématique ni encourager la triche par copier-coller de solutions erronées.
• Limitations actuelles : Le système suppose une correspondance 1-to-1 entre les étapes NL et les tactiques FL, ce qui ne scale pas encore aux preuves complexes. De plus, il dépend de l'existence d'une solution formelle de référence.
• Futur : Les auteurs visent à déployer LeanTutor dans des cours universitaires (maths discrètes, algèbre linéaire) et à améliorer la capacité du système à gérer des preuves sans solution de référence préexistante, tout en affinant les facteurs humains de l'interaction homme-IA.

En résumé, LeanTutor représente une avancée significative vers des systèmes éducatifs IA qui ne se contentent pas de "parler" mathématiques, mais qui les comprennent et les vérifient véritablement.