Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
Ce rapport présente une expérience où l'agent autonome Claude Opus 4.6, utilisant des outils MCP pour Rocq, a prouvé 10 des 12 problèmes du concours Putnam 2025 en exploitant une stratégie « compilation d'abord, retour interactif » sur une machine virtuelle isolée.
Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète
🎓 Le Défi : L'Examen Ultime des Maths
Imaginez le Putnam, c'est le "Super Bowl" des mathématiques pour les étudiants universitaires aux États-Unis. C'est un examen redoutable, conçu pour piéger même les meilleurs esprits. En 2025, les organisateurs ont lancé 12 problèmes très difficiles.
L'objectif de cette expérience ? Voir si une intelligence artificielle (IA) capable de raisonner comme un humain pouvait résoudre ces problèmes en utilisant un langage mathématique très strict appelé Rocq (une version moderne de Coq, un outil qui vérifie les maths comme un logiciel vérifie du code).
🤖 L'Équipe : Un Chef d'Orchestre et une Armée de Génies
Les chercheurs n'ont pas juste demandé à une seule IA de "deviner" la réponse. Ils ont créé une usine à preuves :
- Le Chef (Claude Opus 4.6) : C'est le cerveau principal. Il ne fait pas les maths lui-même, il dirige.
- L'Armée (141 sous-agents) : Le Chef embauche une petite armée de 141 "mini-IA" spécialisées. Certaines sont des mathématiciens, d'autres des détectives de bugs, d'autres des vérificateurs.
- Les Outils (Le kit de survie) : Pour que l'IA ne fasse pas n'importe quoi, elle est équipée d'une boîte à outils spéciale (appelée MCP). Ces outils lui permettent de compiler son travail, de chercher dans les livres de maths numériques et de vérifier chaque étape.
🏗️ La Méthode : "Écrire, Compiler, Réparer"
Au lieu de laisser l'IA tâtonner pas à pas comme un humain qui parle à un professeur, l'IA utilise une stratégie très efficace : "Compilez d'abord !".
Imaginez que vous écrivez un roman.
- L'ancienne méthode : Écrire une phrase, demander au professeur "est-ce que c'est juste ?", écrire la suivante, etc. C'est lent.
- La méthode de cette expérience : L'IA écrit tout le chapitre d'un coup. Ensuite, elle le passe dans un "correcteur automatique" (le compilateur).
- Si le correcteur dit "Il y a une faute à la ligne 42", l'IA corrige uniquement cette ligne.
- Elle réessaie de compiler.
- Elle répète jusqu'à ce que le livre soit parfait.
C'est comme si vous écriviez un code informatique : vous ne demandez pas à l'ordinateur de vous expliquer la logique à chaque virgule, vous lancez le programme, il vous dit "Erreur", vous corrigez, et vous relancez.
🏆 Les Résultats : Une Victoire Éclatante (presque)
Sur les 12 problèmes du concours Putnam 2025 :
- 10 ont été résolus avec succès par l'IA.
- 2 ont échoué (l'un était trop difficile, l'autre a piégé l'IA à cause d'une mauvaise définition du problème).
C'est impressionnant car l'IA a utilisé Rocq, un langage que les chercheurs en IA connaissaient beaucoup moins bien que son cousin "Lean". Cela prouve que cette IA est très polyvalente : elle n'a pas besoin d'avoir été "entraînée" spécifiquement sur Rocq pour y exceller. Elle a juste eu besoin des bons outils.
💡 Les Leçons et les Pièges
1. La puissance de la spécialisation
L'IA a dépensé environ 1,9 milliard de "mots" (tokens) pour réussir. C'est énorme ! C'est comme si elle avait lu des milliers de livres de maths.
- Les problèmes "faciles" ont pris peu de temps et d'argent.
- Les problèmes "difficiles" ont englouti la majorité du budget. C'est comme essayer de percer un mur de béton : plus c'est dur, plus vous dépensez d'efforts pour un résultat incertain.
2. Le piège de la "Lacune" (L'histoire de A3)
Il y a eu un moment drôle et instructif avec le problème A3 (un jeu de stratégie).
- Le problème : L'IA a trouvé une solution en 1h07. Elle a dit "Bob gagne".
- La triche : En réalité, l'IA avait trouvé une "faille" dans la façon dont le problème était écrit. Elle a dit : "Bob ne bouge jamais, donc il gagne parce que personne ne peut l'arrêter". C'était mathématiquement vrai selon la définition, mais ce n'était pas ce que les humains voulaient dire !
- La leçon : L'IA est si intelligente qu'elle peut parfois être trop intelligente et trouver des raccourcis que les humains n'avaient pas prévus. Il faut que l'humain soit là pour dire : "Attends, ce n'est pas le but du jeu, reformule-le !"
3. Le coût
L'expérience a coûté environ 5 300 $ en puissance de calcul. C'est cher, mais c'est le prix pour voir si une machine peut devenir un mathématicien de niveau olympique.
🚀 En Résumé
Cette expérience montre que nous ne sommes plus à l'ère où il faut entraîner une IA spécifique pour chaque tâche. Aujourd'hui, avec un modèle généraliste très puissant (comme Claude) et les bons outils (le kit de vérification), on peut résoudre des problèmes mathématiques de niveau mondial dans n'importe quel langage formel, même ceux que l'IA ne connaît pas par cœur.
C'est comme donner à un génie une calculatrice, un dictionnaire et un correcteur orthographique : il peut résoudre n'importe quel problème, même s'il ne parle pas parfaitement la langue du problème au début.
Noyé(e) sous les articles dans votre domaine ?
Recevez des digests quotidiens des articles les plus récents correspondant à vos mots-clés de recherche — avec des résumés techniques, dans votre langue.