LeanPRM : Lean annote 152 000 étapes de preuve sans humains et fait passer la précision à 74,7 %

La vérification des longues preuves mathématiques rédigées par les modèles de langage devient un goulot d'étranglement. Les auteurs de LeanPRM proposent d'obtenir une annotation étape par étape auprès de l'assistant de preuve Lean, sans annotateurs. Le résultat : un jeu de données de 10 634 preuves et 152 000 étapes annotées. Un vérificateur basé sur Qwen3-4B, entraîné sur ces données, fait passer sa correspondance exacte avec l'étiquette de l'étape de 48,2 à 74,7 sur le jeu mis de côté LeanPRM-Bench (200 preuves). Le même modèle de base, entraîné sur PRM800K, atteint 60,3.

D'où viennent les étiquettes

On ne peut entraîner un vérificateur de processus (PRM) que sur des données où chaque étape porte une évaluation « correcte » ou « incorrecte ». Pour les preuves ouvertes, ces étiquettes sont difficiles à obtenir. Les annotateurs humains coûtent cher. Les étiquettes dérivées de la réponse finale n'aident pas : une preuve n'a pas de valeur numérique à laquelle comparer le résultat. Quant à la formalisation de chaque preuve en Lean, elle exige le travail d'experts.

LeanPRM contourne ces limites de la façon suivante. Le modèle écrit une preuve en langage naturel et, en parallèle, une preuve formelle, sans aucun retour de Lean. Lean vérifie ensuite la version formelle et attribue une étiquette à chaque étape. Un second modèle écarte les cas où l'échec tient uniquement à la syntaxe du texte formel. Les étiquettes négatives reflètent ainsi de véritables erreurs mathématiques, et non des défauts de notation.

Ce que montrent les chiffres

Principaux résultats de l'article :

• jeu de données : 10 634 preuves, 152 000 étapes annotées, aucune annotation manuelle ;
• LeanPRM-Bench (200 preuves mises de côté) : Qwen3-4B passe de 48,2 à 74,7 de correspondance exacte par étape ;
• référence PRM800K sur le même modèle : 60,3 ;
• sur trois des quatre benchmarks externes, le vérificateur entraîné sur LeanPRM dépasse la version entraînée sur PRM800K ;
• en sélection best-of-N sur des problèmes de niveau IMO, il choisit des preuves de meilleure qualité ;
• le gain est confirmé sur des modèles de 0,6B à 8B paramètres, sur LeanPRM-Bench, Hard2Verify et IMO-GradingBench.

La constance de l'effet selon la taille compte autant que le chiffre record. L'amélioration apparaît aussi bien sur un tout petit modèle que sur un modèle de huit milliards de paramètres. Elle tient donc à la qualité du signal, et non au choix heureux d'une configuration unique.

Les points à examiner de plus près

L'écart principal, 48,2 contre 74,7, a été mesuré sur un benchmark que les auteurs ont eux-mêmes constitué, avec les mêmes procédures de génération et d'annotation. Pour un tel échantillon, l'entraînement sur LeanPRM bénéficie d'un avantage naturel. Les tests externes ont donc plus de poids : le gain y apparaît sur trois benchmarks sur quatre, donc pas partout. Le descriptif disponible de l'article ne dit rien du quatrième ; mieux vaut le vérifier dans le texte complet.

Il existe aussi une limite structurelle. Les étiquettes ne sont fiables que dans la mesure où la preuve formelle correspond à la preuve en langage naturel. Si le modèle écrit une version formelle qui diverge du texte, Lean évalue autre chose que ce que lit un humain. Le filtre du second modèle réduit le risque de bruit d'origine syntaxique, mais ne garantit pas une correspondance parfaite entre les deux versions. La couverture est elle aussi limitée : on ne peut annoter que ce qui a pu être formalisé.

L'intérêt pratique réside dans le passage à l'échelle. Le volume de données croît avec le nombre d'énoncés formels disponibles, et non avec le budget consacré aux experts. Pour les équipes qui entraînent des modèles mathématiques avec du best-of-N ou du RL à base de récompenses de processus, c'est l'occasion d'obtenir un signal dense sur les étapes de raisonnement sans acheter d'annotation. Pour évaluer l'approche, il vaut la peine de tester son propre vérificateur sur Hard2Verify et IMO-GradingBench. Il est également utile de mesurer dans quelle mesure le gain se maintient sur des preuves éloignées des domaines formalisés en Lean.