PutnamBench
Aussi appelé : Putnam Bench · Putnam benchmark
Mis à jour le
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