InternLM publie AdvancedMathBench, GPT-4.5-xhigh plafonne a 75,8 %

Un banc publie par l'equipe InternLM sur Hugging Face merite qu'on s'y attarde, moins pour la nouveaute du chantier que pour le plafond qu'il met a nu. AdvancedMathBench prend explicitement le contre-pied des olympiades de lycee ou les frontieres saturent depuis un an, et cherche a mesurer les capacites des LLMs sur des mathematiques reellement avancees.

Le dispositif se lit en deux temps. ProverBench regroupe 296 problemes couvrant les niveaux licence et qualifications doctorales pour evaluer la construction de preuves. VerifierBench propose 888 trajectoires de preuves generees par des modeles avec verite terrain expertisee, pour tester la capacite a juger de la validite d'une demonstration. Une pipeline de verification automatique complete l'ensemble, entrainee sur des annotations expertes a grande echelle, avec un accord fort revendique avec les jugements humains sur les trajectoires tenues en reserve.

Les chiffres racontent la vraie histoire. En generation, le meilleur systeme, GPT-4.5-xhigh, atteint 75,8 au niveau licence et retombe a 66,1 sur les problemes de qualifications doctorales. En verification, le meilleur modele plafonne a 65,1 en F1 equilibre, avec un taux de vrais negatifs faible, ce qui signifie en clair que les modeles ratent les erreurs de raisonnement dans les preuves qu'on leur soumet. Les auteurs le formulent sans detour : la detection d'erreurs dans la verification reste un goulot pour les modeles frontiere actuels.

Pourquoi c'est important si vous n'entrainez pas de LLMs. La promesse d'un raisonnement de niveau doctorat est devenue un argument commercial standard. Ce banc suggere qu'il faut la lire avec precaution, parce que la generation de preuves avancees n'est ni fiable, ni auto-verifiable a ce stade, et cela limite ce qu'on peut deleguer a un modele en recherche mathematique appliquee ou en assistance a la demonstration.

Le bemol honnete est que la fiche du papier reste discrete sur plusieurs points qu'un lecteur voudrait creuser, notamment la typologie precise des erreurs qui echappent aux verificateurs, le comportement des principaux modeles open source face aux frontiere fermes, ou l'extension eventuelle vers des preuves formelles verifiables machine. La direction reste neanmoins claire, et c'est la l'interet : un banc calibre sur des mathematiques reellement avancees, plutot qu'un enieme leaderboard olympiade, donne enfin un signal fiable sur ce qui coince.