PutnamBench
Aussi appelé : Putnam Bench · Putnam benchmark
Mis à jour le
En bref
PutnamBench est un benchmark de 640 problèmes du concours universitaire William Lowell Putnam, formalisés en Lean 4, Isabelle et Coq, utilisé pour évaluer la capacité des IA à démontrer des théorèmes mathématiques complexes.
📖 Définition
💬 En termes simples
C'est comme faire passer à une IA les questions d'un concours universitaire réputé difficile, mais en exigeant en plus que chaque solution soit rédigée dans un langage si précis qu'un ordinateur puisse vérifier lui-même, sans aucune ambiguïté, qu'elle est correcte.
🎯 Exemple concret
Un laboratoire de recherche teste son nouveau modèle de raisonnement sur les 640 problèmes formalisés en Lean 4 de PutnamBench et communique le nombre de problèmes résolus, ce score devenant un indicateur comparable de la progression du raisonnement mathématique de l'IA d'une année à l'autre.
💡 Le saviez-vous ?
Le concours Putnam, dont s'inspire PutnamBench, est réputé pour sa difficulté extrême : il n'est pas rare que la médiane des scores des participants, pourtant déjà des étudiants universitaires très forts en mathématiques, soit proche de zéro sur douze problèmes.
❓ Questions fréquentes
D'où viennent les problèmes de PutnamBench ?
Dans quels langages formels PutnamBench est-il disponible ?
PutnamBench est-il facile à résoudre pour une IA ?
📚 Sources
- Tsoukalas et al. - PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition (arXiv) (trishullab, 2024)
- trishullab - dépôt GitHub PutnamBench (trishullab, 2024)
🔗 Termes liés
🏷️ Catégorie parente