Dans cet article, nous présentons FormulaOne, un benchmark qui se concentre sur des problèmes de recherche réels plutôt que sur des casse-têtes de programmation compétitifs, afin de révéler les limites des capacités des modèles d'IA de pointe. FormulaOne est composé de problèmes combinant théorie des graphes, logique et algorithmes, et liés à des problèmes d'optimisation à grande échelle du monde réel, tels que le routage, l'ordonnancement et la conception de réseaux. Les problèmes sont générés selon la logique monadique du second ordre (MSO), facile à générer automatiquement, et certains problèmes sont étroitement liés à des problèmes complexes de l'informatique théorique, comme l'hypothèse de temps exponentiel fort (SETH). Les résultats expérimentaux montrent que les modèles de pointe, comme o3 d'OpenAI, résolvent moins de 1 % des problèmes de FormulaOne, ce qui montre qu'ils sont loin d'être maîtrisés par les experts dans certains domaines. Pour soutenir la recherche, nous fournissons également FormulaOne-Warmup, un ensemble de problèmes plus simples avec des distributions similaires.
