La compilation Lean gonfle la précision de l'autoformalisation : jusqu'à 29,5 points de pourcentage d'écart

Lean accepte une déclaration dès lors qu'elle est correctement typée. Ce qu'elle exprime sur le fond, le compilateur ne le vérifie pas. Les auteurs de l'étude « Beyond Compilation » ont mesuré de combien la métrique « ça compile » surestime la qualité de l'autoformalisation, c'est-à-dire de la traduction d'énoncés mathématiques du langage naturel vers Lean. Le chiffre le plus parlant : l'agent doté d'outils compile 87,2% des 227 énoncés universitaires, mais le critère sémantique n'en laisse passer que 57,7%. Cet écart de 29,5 points de pourcentage correspond à du code Lean d'apparence irréprochable, qui formule autre chose que ce qui était demandé.

Comment fonctionne la vérification

La plupart des tâches n'ont pas de traduction Lean de référence : impossible donc de comparer à une réponse « étalon ». Les auteurs introduisent un critère composite : un énoncé est accepté s'il compile dans Lean et si deux LLM issus de familles différentes le jugent, indépendamment l'un de l'autre, comme une traduction fidèle de la formulation d'origine.

Le critère a été testé sur un audit aléatoire indépendant. Il coïncide avec l'avis de la majorité des annotateurs humains dans 91,5% des cas. Ses erreurs sont asymétriques : il laisse rarement passer une traduction fausse, mais rejette une partie des traductions correctes. L'évaluation est donc conservatrice et tend plutôt à sous-estimer les résultats des systèmes.

Principaux résultats sur les huit systèmes :

• l'écart entre la part d'énoncés compilés et la part d'énoncés acceptés va de 1,3 à 29,5 points de pourcentage ;
• agent avec outils : 87,2% de compilation contre 57,7% d'énoncés acceptés ;
• des humains ont examiné tous les rejets de l'agent : 23,8 des 29,5 points de pourcentage correspondent à de réelles erreurs de traduction ;
• pour six des sept systèmes en un seul passage (one-shot), 78–100% de l'écart relèvent de véritables erreurs de traduction, d'après une revue en deux étapes réalisée par Claude Opus 5.5 avec Lean et GPT-6.1 Sol, recoupée avec l'annotation humaine.

Quand c'est le juge qui se trompe

La partie la plus surprenante concerne les modèles récents. GPT-5.2 était l'un des deux juges. Les auteurs lui ont fait évaluer les traductions de deux modèles plus récents, GPT-6 Astra et Claude Opus 5.5. Le juge a accepté 83% des énoncés pour chacun. Son propre résultat one-shot, lui, est de 21%.

La revue en deux étapes a ensuite examiné les rejets de ces deux modèles. Sur 54 énoncés rejetés, seuls 4 étaient de réelles erreurs de traduction, soit 7%. Les autres rejets sont des erreurs du juge. Cela s'accorde avec une logique simple : moins un système se trompe, moins ses rejets contiennent de vraies erreurs, et plus le bruit du juge devient visible. Un juge qui ne progresse pas au même rythme que les modèles évalués devient le goulot d'étranglement du benchmark.

Pour le secteur, la conclusion est inconfortable. Une métrique fondée sur un LLM-juge est presque fiable pour les systèmes faibles, mais commence à sous-estimer la qualité des systèmes forts. Il est impossible de comparer des modèles de générations différentes avec cette métrique sans revérifier les rejets.

Ce que montre l'ablation des outils

Les auteurs ont soumis l'agent à une ablation 2^3 : trois outils activés et désactivés dans les huit combinaisons possibles. L'essentiel du gain de compilation vient du retour d'erreurs de Lean : l'agent voit les erreurs et corrige son code. Mais près de la moitié de ce gain ne passe pas le critère sémantique. L'agent apprend à obtenir la compilation, pas la précision du sens. Effet typique : pour éliminer une erreur, une condition disparaît de l'énoncé, un quantificateur est affaibli ou la structure est remplacée.

Ce qu'il faut changer dans la pratique

Si vous construisez un pipeline d'autoformalisation ou entraînez un modèle à partir du signal de Lean, la compilation comme unique récompense donne une estimation biaisée et pousse vers des formulations dégénérées. Il faut au moins une couche sémantique : des juges issus de familles différentes et une vérification humaine par échantillonnage des rejets.

Avec de nouveaux modèles, il convient de vérifier que le juge ne prend pas de retard sur le système évalué. Si la plupart des rejets sont des erreurs du juge et non de la traduction, il est temps de revoir la métrique. Le code et les données sont publiés sur GitHub (grenadeComing/beyond-compilation) : l'approche peut donc être reproduite sur vos propres énoncés.