Learning to Disprove: Formal Counterexample Generation with Large Language Models

Cet article présente une méthode pour affiner des modèles de langage afin de générer des contre-exemples mathématiques formels vérifiables dans Lean 4, en utilisant une stratégie de mutation symbolique et un cadre d'itération experte pour combler le fossé actuel entre la construction de preuves et la réfutation d'énoncés faux.

L'essentiel

🧠 Le Grand Défi : Ne pas seulement construire, mais aussi détruire

Imaginez que vous apprenez à un robot à faire des mathématiques. Jusqu'à présent, on lui a surtout appris à construire des preuves. C'est comme lui apprendre à bâtir un château de cartes solide : il doit montrer que chaque carte est bien placée pour que la tour tienne. C'est le travail de "prouver que quelque chose est VRAI".

Mais dans la vraie vie des mathématiques, il y a une autre compétence cruciale : prouver que quelque chose est FAUX. Pour cela, il faut trouver un contre-exemple. C'est comme trouver la seule carte dans le monde qui fait effondrer tout le château. Si vous trouvez cette carte, vous avez prouvé que la règle "toutes les cartes tiennent" est fausse.

Le problème ? Les intelligences artificielles actuelles sont excellentes pour construire des châteaux, mais elles sont très mauvaises pour trouver la carte qui fait tout tomber. Elles essaient souvent de prouver que le château est solide, même quand il devrait s'effondrer.

🛠️ La Solution : L'Art du "Détournement" (Mutation Symbolique)

Les chercheurs de ce papier ont eu une idée géniale pour entraîner leurs robots à trouver ces erreurs. Ils ont utilisé une technique qu'on pourrait appeler "le détournement de théorèmes".

Voici comment ça marche, avec une analogie de cuisine :

1. La Recette Parfaite (Le Théorème) : Imaginez une recette de gâteau qui dit : "Si vous utilisez de la farine (H1) ET du sucre (H2), alors vous obtiendrez un gâteau délicieux (C)." C'est une vérité absolue.
2. Le Détournement (La Mutation) : Le robot prend cette recette et dit : "Et si on enlevait la farine ?" Il crée une nouvelle règle : "Si vous utilisez du sucre (H2), vous obtiendrez un gâteau délicieux (C)."
3. Le Problème : Cette nouvelle règle est fausse ! Sans farine, le gâteau ne tient pas.
4. La Mission du Robot : Le robot doit maintenant trouver un exemple concret (un "contre-exemple") où l'on a du sucre mais pas de farine, et où le résultat est un gâteau raté.

En faisant cela automatiquement sur des milliers de théorèmes, les chercheurs ont créé une énorme bibliothèque d'exercices où le robot doit systématiquement trouver les failles. C'est comme donner au robot des milliers de puzzles où il doit trouver l'erreur cachée.

🎯 Le Système de Récompense Double (Le "Double Score")

Entraîner un robot à trouver des erreurs est difficile. Si le robot échoue, il ne reçoit aucune récompense, et il ne sait pas comment s'améliorer (c'est ce qu'on appelle un "signal de récompense rare").

Pour résoudre ça, les chercheurs ont mis en place un système de double récompense :

• Récompense 1 (La Preuve de l'Erreur) : Le robot doit prouver que son exemple (le gâteau raté) fonctionne bien pour la nouvelle règle fausse.
• Récompense 2 (La Preuve de la Cause) : Le robot doit aussi prouver que ce qui manque (l'absence de farine) est bien la cause du problème.

Même si le robot ne trouve pas la solution parfaite immédiatement, s'il arrive à prouver la "cause" (Récompense 2), il reçoit quand même un petit point. Cela l'encourage à continuer d'essayer, même sur les problèmes très difficiles. C'est comme dire à un élève : "Tu n'as pas trouvé la réponse finale, mais tu as bien identifié la cause de l'erreur, bravo !"

🚀 Les Résultats : Un Robot qui devient un Détective

Grâce à cette méthode, les chercheurs ont entraîné un modèle d'IA capable de :

1. Penser à l'aveugle (trouver un exemple concret dans sa tête).
2. Écrire la preuve formelle (écrire le code mathématique rigoureux qui prouve que l'exemple est correct).
3. Se faire vérifier par un ordinateur (un "juge" mathématique) qui dit : "C'est vrai, c'est un contre-exemple !"

Les résultats sont impressionnants. Sur des tests difficiles, leur modèle a surpassé les meilleurs modèles existants de 47 % à 74 %.

🌟 En Résumé

Imaginez que vous voulez apprendre à un enfant à ne pas se tromper en mathématiques. Au lieu de lui donner seulement des exercices où il doit prouver que $2+2=4$, vous lui donnez des exercices où il doit trouver pourquoi$2+2=5$ est faux.

Ce papier montre que si on entraîne les intelligences artificielles à détruire des affirmations fausses (en trouvant des contre-exemples), elles deviennent non seulement de meilleurs détectives d'erreurs, mais aussi de meilleurs bâtisseurs de vérités. C'est un pas de géant vers des IA plus fiables et plus intelligentes en mathématiques.

Résumé technique

1. Problématique et Contexte

Le raisonnement mathématique exige deux compétences complémentaires : la construction de preuves rigoureuses pour les énoncés vrais et la découverte de contre-exemples pour réfuter les énoncés faux. Bien que les travaux récents sur les modèles de langage (LLM) en mathématiques se concentrent presque exclusivement sur la génération de preuves formelles, la tâche de trouver des contre-exemples reste négligée, malgré son importance cruciale pour le développement théorique, le raffinement des conjectures et l'évaluation de la fiabilité des modèles.

L'article identifie deux défis majeurs entravant le développement de LLMs spécialisés dans la génération de contre-exemples formels :

1. La pénurie de données d'entraînement : Il existe très peu de jeux de données étiquetés pour cette tâche (seul CounterMath existe, avec seulement 1 216 problèmes en langage naturel, insuffisant pour le fine-tuning).
2. La rareté des signaux de récompense : Dans les approches par apprentissage par renforcement ou itération d'experts, si le modèle échoue à trouver un contre-exemple correct pour un problème complexe, la récompense est nulle, ce qui empêche l'apprentissage et conduit à un plateau de performance.

2. Méthodologie

Les auteurs proposent un cadre intégré en deux étapes pour surmonter ces obstacles : la synthèse de problèmes par mutation symbolique et un entraînement guidé par une récompense multi-objectifs.

A. Synthèse de Données par Mutation Symbolique

Au lieu de collecter manuellement des contre-exemples, l'équipe génère automatiquement des problèmes d'entraînement à partir de théorèmes existants et prouvables (extraits de Mathlib, Leanworkbook, MiniF2F, etc.).

• Principe : Pour un théorème universel prouvable de la forme $\forall x, H_1(x) \land H_2(x) \implies C(x)$, l'algorithme supprime une hypothèse nécessaire (par exemple $H_1$).
• Résultat : La version mutée devient fausse ($\exists x, H_2(x) \land \neg H_1(x) \land C(x)$ est faux, ou plus précisément, on cherche à prouver $\exists x, H_2(x) \to C(x)$ qui est faux sans $H_1$, mais le but est de trouver un $x$ qui satisfait $H_2$ et $C$ tout en violant $H_1$).
• Validation : Un prouveur de théorèmes (Lean 4) vérifie que l'hypothèse supprimée était bien nécessaire et que la nouvelle version est effectivement réfutable, garantissant ainsi la validité des problèmes générés.
• Échelle : Cette stratégie a permis de synthétiser 575 000 instances de contre-exemples.

B. Entraînement Guidé par Récompense Multi-Objectifs (Multi-Reward)

Pour pallier le problème de la récompense sparse, les auteurs introduisent un mécanisme de double récompense basé sur l'itération d'experts :

1. Génération : Le LLM propose un contre-exemple candidat ($x^*$).
2. Double Vérification : Le modèle doit générer deux preuves formelles :
   • Une preuve que $x^*$ satisfait la version mutée du théorème.
   • Une preuve que $x^*$ réfute l'hypothèse supprimée (c'est-à-dire $\neg H_1(x^*)$).
3. Signal de Récompense : La récompense est la somme pondérée de la validité de ces deux preuves. Même si la preuve du théorème muté est difficile, la preuve de la réfutation de l'hypothèse (souvent plus simple) fournit un signal de récompense partiel, évitant le blocage de l'apprentissage.
4. Architecture : Le système utilise deux modèles distincts : un pour le raisonnement informel (proposition du contre-exemple) et un pour le raisonnement formel (génération de la preuve en Lean 4).

3. Contributions Clés

• Premier cadre complet pour la génération de contre-exemples formels : L'article formalise la tâche comme une génération de contre-exemples vérifiables automatiquement dans Lean 4, combinant raisonnement informel et preuve formelle.
• Stratégie de mutation symbolique : Une méthode novatrice pour générer massivement des données d'entraînement de haute qualité en exploitant la structure logique des théorèmes existants, résolvant le problème de la rareté des données.
• Mécanisme de récompense robuste : L'introduction d'une fonction de récompense multi-objectifs qui maintient un signal d'apprentissage même lorsque la résolution complète du problème est difficile, améliorant ainsi l'efficacité de l'entraînement.
• Benchmarks et Évaluation : Création de trois nouveaux benchmarks (FOR-COUNTER, VERI-REASON, VERI-FORMALIZE) pour évaluer la recherche de contre-exemples, la vérification de résultats auto-formalisés et la vérification des étapes de raisonnement.

4. Résultats Expérimentaux

Les expériences ont été menées sur des modèles de base comme Qwen3 8B (raisonnement informel) et DeepSeek-Prover-v2 7B (raisonnement formel).

• Performance sur les Benchmarks : Le modèle fine-tuné avec le cadre proposé surpasse significativement les modèles de l'état de l'art (y compris des modèles propriétaires comme GPT-4.1 et DeepSeek-R1, ainsi que des prouveurs neuronaux open-source).
  • Sur le benchmark FOR-COUNTER, le modèle atteint un taux de réussite Pass@1 de 222 problèmes résolus, contre 127 pour le meilleur modèle open-source précédent (DeepSeek-Prover-v2).
  • Cela représente une amélioration relative de 47 % à 74 % par rapport aux meilleures bases de référence.
• Efficacité de l'entraînement : La courbe d'apprentissage montre que l'approche multi-récompense converge plus rapidement et atteint une performance finale supérieure par rapport à un entraînement à récompense unique.
• Analyse des échecs : L'étude de cas révèle que les erreurs proviennent principalement de deux sources : un raisonnement informel incorrect (ex: utiliser des nombres complexes au lieu d'entiers) ou un échec à suivre les instructions pour formaliser le contre-exemple correct dans Lean 4.

5. Signification et Impact

Ce travail marque une avancée significative dans le domaine du raisonnement mathématique par IA :

• Changement de paradigme : Il déplace l'attention de la simple "construction de preuves" vers la "démonstration de fausseté", une compétence essentielle pour la découverte scientifique et la vérification de conjectures.
• Auto-vérification : En apprenant à générer des contre-exemples, les LLMs acquièrent une capacité d'auto-vérification et d'auto-correction, renforçant leur fiabilité et leur pouvoir explicatif.
• Outil pratique : Le cadre proposé offre un "copilote" pratique pour les mathématiciens, capable non seulement de prouver des théorèmes, mais aussi de tester et de réfuter des conjectures potentielles de manière rigoureuse.

En résumé, cette recherche comble un vide critique dans les capacités de raisonnement des LLMs en fournissant une méthode scalable et efficace pour apprendre à "prouver par l'absurde" et à réfuter formellement des énoncés mathématiques.