Deux modèles ouverts en tête d'ArXivLean, à dix millions de jetons l'énoncé

MathArena, tenu par le laboratoire SRI de l'ETH Zurich et l'INSAIT, a ajouté une entrée à son classement ArXivLean : un attelage de deux modèles ouverts — Leanstral 1.5, de Mistral, comme démonstrateur, et Kimi K3, de Moonshot, comme coordinateur — y prend la première place sur douze avec 38 énoncés démontrés sur 46, soit 82,61 %. Derrière lui, GPT-6 Astra d'OpenAI à 65,22 % et Opus-5 d'Anthropic à 32,61 %. ArXivLean formalise en Lean des énoncés tirés d'articles récents d'arXiv et renouvelle son jeu pour limiter la contamination ; une démonstration ne compte que si le vérificateur Lean l'accepte. C'est Mistral qui a fait tourner l'attelage, mais la vérification, elle, est mécanique.

Le prix est dans la colonne voisine : dix millions de jetons produits par énoncé, contre 21 560 pour le modèle d'OpenAI — 465 fois plus. Les deux modèles étant à poids ouverts, le classement ne chiffre pas leur coût, là où il donne 8,54 dollars par énoncé à GPT-6 Astra. L'écart de score n'est pas net pour autant : les intervalles de confiance, ± 10,95 et ± 13,76 points, se recouvrent.