A method for the automated generation of proof exercises with comparable levels of proving complexity

Cet article présente une méthode automatisée pour générer des exercices de preuve mathématique de complexité comparable, en utilisant des preuves par tableaux analytiques sans symboles logiques pour évaluer et contrôler la difficulté des exercices destinés aux cours de mathématiques discrètes du premier cycle.

L'essentiel

Imaginez que vous êtes un professeur de mathématiques. Votre plus grand défi n'est pas d'expliquer les concepts, mais de créer des exercices de preuve (des problèmes où l'étudiant doit démontrer qu'une affirmation est vraie) qui sont juste à la bonne difficulté.

Si vous donnez un exercice trop facile, l'étudiant s'ennuie. Trop dur, il se décourage. Le problème, c'est que créer ces exercices à la main prend un temps fou. Les ordinateurs peuvent déjà générer des questions, mais ils sont souvent incapables de dire : "Tiens, cette question est exactement aussi difficile que celle-ci", car ils ne comprennent pas la "structure" du raisonnement nécessaire pour résoudre le problème.

Ce papier propose une solution intelligente pour générer automatiquement des exercices de preuve qui ont exactement le même niveau de difficulté.

Voici comment cela fonctionne, expliqué avec des analogies simples :

1. Le Problème : La Difficulté est un Mystère

Habituellement, pour juger la difficulté d'un exercice, on regarde sa forme (combien de symboles, de mots, etc.). C'est comme juger la difficulté d'un plat en comptant le nombre d'ingrédients.

• Le piège : Un plat avec 5 ingrédients simples peut être plus difficile à cuisiner qu'un plat avec 10 ingrédients complexes. De même, deux exercices de logique peuvent avoir la même apparence, mais l'un demande un raisonnement très complexe, tandis que l'autre est trivial.

2. La Solution : La "Recette de Cuisine" (Les Règles Théoriques)

Les auteurs ont créé un système qui ne regarde pas la surface, mais la recette interne pour résoudre le problème.

Imaginez que chaque exercice de mathématiques est un labyrinthe.

• La méthode traditionnelle regarde la taille du labyrinthe (le nombre de murs).
• Cette nouvelle méthode regarde le nombre de virages et la complexité des chemins qu'il faut emprunter pour sortir.

Pour faire cela, ils utilisent des "Tableaux Théoriques". C'est un peu comme un arbre généalogique du raisonnement. Au lieu d'utiliser des symboles logiques compliqués (comme des signes "ET", "OU", "SI... ALORS"), ils traduisent tout en règles simples, comme des instructions de cuisine :

• Règle : "Si tu as un 'et', tu peux le séparer en deux parties."
• Règle : "Si tu as une inclusion, tu peux regarder les éléments un par un."

Ces règles sont extraites automatiquement de la théorie mathématique (comme la théorie des ensembles) et sont conçues pour être pures (sans symboles logiques superflus).

3. Le Secret : L'Isomorphisme (Les Jumeaux Identiques)

C'est le cœur de la méthode. Pour trouver un nouvel exercice de même difficulté, le système ne cherche pas un exercice "similaire", il cherche un exercice jumeau structurel.

Imaginez que vous avez un moule à gâteau (la structure du raisonnement).

1. Vous prenez un exercice existant (le "gâteau original").
2. Le système analyse le moule : il compte les étapes, les embranchements, la profondeur du raisonnement.
3. Ensuite, il prend ce même moule et y verse une nouvelle pâte (de nouveaux symboles, de nouvelles variables).

Exemple concret :

• Exercice A : "Prouver que si un élément est dans l'intersection de deux ensembles, il est dans le premier."
• Exercice B (généré) : "Prouver que si un élément est dans la différence de deux ensembles, il est dans le premier."

Même si les mots "intersection" et "différence" changent, la structure du chemin pour prouver la chose est identique. C'est comme si vous aviez deux maisons construites avec exactement le même plan d'architecte, mais avec des briques de couleurs différentes. Pour l'architecte (l'ordinateur), elles sont de la même complexité.

4. Comment l'Ordinateur fait-il cela ?

Le processus se déroule en deux étapes magiques :

1. L'Analyse (Le Scanner) : L'ordinateur prend votre exercice d'entrée et construit le "chemin le plus court" (la preuve minimale) pour le résoudre. Il compte chaque pas nécessaire. C'est comme mesurer la distance exacte entre le point A et le point B.
2. La Génération (Le Miroir) : L'ordinateur cherche d'autres combinaisons de mots et de symboles qui, lorsqu'on applique les mêmes règles, créent exactement le même chemin. Il remplace les symboles (comme changer un "∩" par un "∪") mais s'assure que le nombre de pas et la logique restent identiques.

Pourquoi c'est génial pour les professeurs ?

• Gain de temps : Plus besoin de passer des heures à inventer des variantes d'exercices.
• Équité : Tous les étudiants peuvent recevoir des exercices différents, mais qui demandent le même effort mental. Personne n'a de la chance ou de la malchance sur la difficulté.
• Personnalisation : Un tuteur peut générer des exercices adaptés au niveau de chaque élève, en gardant la même structure de raisonnement mais en changeant la "couleur" du problème.

En résumé

Ce papier propose un générateur de "jumeaux de difficulté". Au lieu de deviner si un exercice est dur, il le décompose en une structure logique pure, puis recrée des exercices qui sont des copies conformes de cette structure, mais avec des ingrédients mathématiques différents. C'est comme avoir un chef cuisinier robot capable de créer un millier de plats différents, tous ayant exactement le même temps de cuisson et la même complexité de préparation.

Résumé technique

Voici un résumé technique détaillé de l'article en français, structuré selon les points demandés.

Titre de l'article

Une méthode pour la génération automatique d'exercices de preuve avec des niveaux de complexité de preuve comparables.

1. Le Problème

La génération automatique de questions (AQG - Automatic Question Generation) vise à réduire la charge de travail des éducateurs dans la conception d'exercices. Cependant, un obstacle majeur à l'adoption de ces outils dans l'enseignement, en particulier pour les matières formelles comme la logique et les mathématiques discrètes, est l'incapacité à contrôler finement la difficulté des exercices générés.

Les approches existantes souffrent de plusieurs limitations :

• Manque de contrôle pédagogique : La plupart des outils ne permettent pas de garantir que les exercices générés correspondent au niveau de compétence attendu.
• Dépendance au jugement humain ou au ML : Les méthodes basées sur l'estimation de la difficulté via le texte (QDET) ou l'apprentissage profond dépendent de jugements humains subjectifs (qui peuvent être incohérents) ou de modèles "boîte noire" sans explication.
• Limites structurelles : Les méthodes basées uniquement sur la complexité syntaxique (nombre de connecteurs, profondeur) ne reflètent pas nécessairement l'effort réel requis pour résoudre la preuve, car deux formules de structure syntaxique identique peuvent nécessiter des stratégies de preuve très différentes.

L'objectif est donc de créer une méthode capable de générer des exercices de preuve dont la complexité de preuve est strictement comparable à celle d'un exercice de référence, en se basant sur la structure de la solution plutôt que sur la forme superficielle de l'énoncé.

2. Méthodologie

La méthode proposée repose sur une approche formelle utilisant des tableaux sémantiques basés sur la coupure (cut-based tableaux) adaptés aux théories mathématiques spécifiques, sans utiliser de symboles logiques dans les nœuds de la preuve.

A. Théories Définitionnelles et Règles Spécifiques

• Théorie Définitionnelle : Définie comme un triplet $\langle L, Ax, < \rangle$ où $L$ est un langage du premier ordre, $Ax$ un ensemble d'axiomes définitionnels (formules closes), et $<$ une relation bien-fondée sur les symboles de prédicat.
• Extraction de Règles : À partir des axiomes définitionnels, le système extrait un ensemble de règles spécifiques à la théorie. Ces règles sont dérivées en transformant les axiomes en une forme normale appelée RINF (Rule Implicational Normal Form).
  • Les règles sont linéaires (une seule conclusion).
  • Elles ne contiennent aucun symbole logique (ni $\land, \lor, \neg, \to$) dans leurs prémisses ni dans leurs conclusions.
  • Elles respectent des restrictions analytiques : les variables de la conclusion sont présentes dans les prémisses, et le prédicat de la conclusion est "plus petit" (selon $<$) ou la profondeur syntaxique est réduite.
• Exemple : Pour la théorie des ensembles, les axiomes sur $\cup, \cap, \setminus, \in$ sont transformés en règles d'inférence comme $+ x \in y \cup z \vdash + x \in y$ ou $+ x \in y \cap z \vdash + x \in y$.

B. Preuves et Complexité

• Preuves Spécifiques à la Théorie : Une preuve est un tableau clos construit uniquement avec ces règles spécifiques.
• Mesure de la Complexité : La complexité n'est pas mesurée par la taille de la formule, mais par la taille déductive de la preuve minimale.
  • Arbres de Justification : Chaque branche fermée d'un tableau est associée à un arbre de justification (racine = nœud de fermeture, enfants = nœuds justifiant la fermeture).
  • Isomorphisme Déductif : Deux preuves sont considérées de complexité comparable si leurs arbres de justification sont isomorphes (même structure de dépendance logique) et si les formules correspondantes sont syntaxiquement isomorphes.
  • Taille Déductive : Somme des nœuds des arbres de justification d'une preuve.

C. Procédure de Génération

L'algorithme se déroule en deux étapes principales :

1. Recherche de Preuves Minimales : Pour un exercice d'entrée (représenté par un ensemble de formules signées), le système explore systématiquement les tableaux ($T_1, T_2, \dots$) jusqu'à trouver les preuves minimales (taille déductive la plus faible).
2. Recherche d'Ensembles Isomorphes : Le système génère de nouveaux ensembles de formules signées en remplaçant les symboles (prédicats et fonctions) de l'exercice d'entrée par d'autres symboles de la même théorie, tout en respectant les contraintes d'isomorphisme déductif.
   • Filtrage : Seules les substitutions qui préservent la structure de la preuve minimale (via des "symboles de correspondance déductive") sont autorisées. Cela réduit considérablement l'espace de recherche par rapport à une approche par force brute.

3. Contributions Clés

• Nouvelle Métrique de Difficulté : Introduction d'une mesure de difficulté basée sur la complexité de preuve (structure de la solution) plutôt que sur la complexité syntaxique de l'énoncé.
• Tableaux sans Symboles Logiques : Développement d'une méthode de tableaux (inspirée de la méthodologie KE) où les règles d'inférence sont extraites automatiquement des axiomes et sont dépourvues de connecteurs logiques, permettant une formalisation plus proche des preuves informelles utilisées en classe.
• Concept d'Isomorphisme Déductif : Définition formelle permettant d'identifier des exercices différents mais dont la résolution requiert le même effort cognitif et logique.
• Procédure Automatisée : Implémentation d'un algorithme complet (disponible sur GitHub) qui prend un exercice et une théorie, et génère une famille d'exercices de difficulté équivalente.

4. Résultats

• Validation par l'Exemple : L'article démontre la méthode sur la théorie des ensembles (ensembles, intersections, unions, différence symétrique).
• Génération d'Exercices : Le système a réussi à générer des exercices variés (ex: remplacer $\cap$ par $\setminus$ ou $\triangle$) qui possèdent des preuves minimales isomorphes à celle de l'exercice original.
• Réduction de l'Espace de Recherche : Grâce à l'utilisation des "symboles de correspondance déductive", le nombre de cas à tester pour trouver des exercices isomorphes a été réduit drastiquement (ex: de plusieurs milliers à quelques centaines dans l'exemple fourni).
• Preuves Comparables : Les exercices générés (ex: "Prouver que $x \in y \cap (w \cup z) \implies x \in (y \cap w) \cup z$" et sa variante avec $\setminus$ et $\triangle$) partagent la même structure de preuve minimale, garantissant une difficulté comparable.

5. Signification et Perspectives

• Impact Pédagogique : Cette méthode permet aux enseignants de créer des banques d'exercices personnalisés où la difficulté est contrôlée objectivement. Elle facilite la création d'évaluations adaptatives et de feedback personnalisé, évitant que certains élèves ne soient avantagés par des questions trop faciles.
• Explicabilité : Contrairement aux modèles d'apprentissage automatique, la difficulté est expliquée par la structure de la preuve minimale, offrant une transparence totale.
• Limites et Travaux Futurs :
  • La méthode actuelle ne couvre pas les exercices dont la description logique ne peut pas être convertie en forme normale STSNF.
  • Certaines restrictions analytiques empêchent l'extraction de règles pour certains axiomes.
  • Les auteurs prévoient d'étudier les invariances (ex: commutativité de l'intersection) pour enrichir la génération et de valider empiriquement la notion de complexité de preuve auprès d'étudiants réels (vérifier si la structure de la preuve correspond bien à la perception de difficulté).

En résumé, cet article propose une avancée significative dans le domaine de l'AQG formelle en remplaçant les heuristiques statistiques ou syntaxiques par une analyse structurelle rigoureuse des preuves, offrant ainsi un contrôle précis et justifiable sur la difficulté des exercices générés.