FATE-H et FATE-X
Aussi appelé : Formal Algebra Theorem Evaluation · FATE benchmark · FATE-M · FATE-H · FATE-X
Mis à jour le
FATE-H et FATE-X sont les niveaux difficile et extrêmement difficile du benchmark FATE, qui teste en Lean 4 la capacité des IA à démontrer des théorèmes d'algèbre de niveau doctorat et recherche.
📖 Définition
💬 En termes simples
Si miniF2F et PutnamBench ressemblent à des concours de mathématiques pour étudiants brillants, FATE-H et FATE-X ressemblent plutôt à des problèmes tirés directement des thèses de doctorat et des articles de recherche en algèbre : le niveau de difficulté grimpe d'un cran supplémentaire, jusqu'à des concepts que même la bibliothèque Lean n'a pas encore formalisés.
🎯 Exemple concret
Un modèle qui obtient un score honorable sur miniF2F ou PutnamBench peut voir sa performance chuter drastiquement sur FATE-X, révélant que sa capacité de raisonnement s'effondre dès que les problèmes dépassent le niveau des concours pour atteindre celui de la recherche en algèbre.
💡 Le saviez-vous ?
FATE-X est présenté par ses créateurs comme le premier benchmark qui dépasse à la fois le niveau des examens de qualification doctorale et la couverture de Mathlib : certains de ses problèmes exigent de formaliser en Lean des notions mathématiques qui n'avaient jamais été encodées auparavant.
❓ Questions fréquentes
Quelle est la différence entre FATE-H et FATE-X ?
Qui a créé la série de benchmarks FATE ?
Comment les modèles d'IA sont-ils évalués sur FATE ?
📚 Sources
- Westlake University - FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels (arXiv) (Westlake University, 2026)
- frenzymath - dépôt GitHub FATE-H (frenzymath, 2026)
🔗 Termes liés
🏷️ Catégorie parente