miniF2F
Aussi appelé : mini Formal-to-Formal · mini-F2F
Mis à jour le
miniF2F est un benchmark de 244 problèmes de mathématiques de niveau olympiade, formalisés dans Lean et d'autres assistants de preuve, utilisé pour évaluer la capacité des IA à démontrer des théorèmes.
📖 Définition
💬 En termes simples
C'est un peu comme faire passer le même examen de mathématiques, traduit dans plusieurs langues, à des étudiants formés dans des écoles différentes : on peut ainsi comparer équitablement leurs résultats, peu importe l'assistant de preuve qu'ils utilisent.
🎯 Exemple concret
Un laboratoire qui entraîne un nouveau modèle de raisonnement mathématique le fait tourner sur les 244 problèmes de miniF2F traduits en Lean 4, puis publie son taux de réussite : ce chiffre devient un point de comparaison standard face aux autres modèles testés sur le même jeu de problèmes.
💡 Le saviez-vous ?
Le nom « miniF2F » vient de « formal-to-formal » (F2F) : contrairement à d'autres benchmarks qui demandent de traduire un énoncé en langage naturel vers un langage formel, miniF2F part d'énoncés déjà formalisés et demande seulement de produire la preuve, ce qui isole la capacité de raisonnement pur du modèle.
❓ Questions fréquentes
Combien de problèmes contient miniF2F ?
Qui a créé miniF2F ?
À quoi sert miniF2F ?
📚 Sources
- OpenAI - dépôt GitHub miniF2F (OpenAI, 2021)
- Zheng, Han, Polu - MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (arXiv) (Kunhao Zheng, Jesse Michael Han, Stanislas Polu, 2021)
🔗 Termes liés
🏷️ Catégorie parente