Nos soumissions First Proof

Nous avons appliqué un modèle interne à l'ensemble des 10 problèmes First Proof⁠(ouverture dans une nouvelle fenêtre), un défi mathématique de niveau recherche conçu pour évaluer si les systèmes d'IA peuvent produire des tentatives de preuve correctes et vérifiables. Contrairement aux mathématiques de type concours ou à réponse courte, ces problèmes nécessitent la construction d'arguments complets dans des domaines spécialisés, et il est difficile d'établir leur exactitude sans l'avis d'un expert. Les auteurs des problèmes First Proof sont des experts de premier plan dans leurs domaines respectifs, et au moins deux de ces problèmes sont restés sans solution pendant des années avant que les auteurs ne trouvent des solutions. Un département universitaire dont les domaines d'étude recoupent largement ceux-ci pourrait vraisemblablement résoudre bon nombre de ces problèmes en une semaine.

Nous avons partagé⁠(ouverture dans une nouvelle fenêtre) nos tentatives de preuve le samedi 14 février 2026 à minuit, heure du Pacifique. Sur la base du feedback des experts, nous estimons qu'au moins cinq des tentatives de démonstration du modèle (problèmes 4, 5, 6, 9 et 10) ont de fortes chances d'être correctes, et plusieurs autres sont toujours en cours d'examen. Nous pensions initialement que notre tentative pour le problème 2 était probablement correcte. D'après le commentaire officiel de First Proof et une analyse plus approfondie de la communauté, nous pensons désormais qu'elle est incorrecte. Nous sommes reconnaissants de votre engagement et nous nous réjouissons de poursuivre ce projet. L'ensemble de nos tentatives de démonstration est disponible ici⁠(ouverture dans une nouvelle fenêtre). La prépublication comprend les dix tentatives de preuve, ainsi qu'une annexe nouvellement ajoutée contenant des modèles et des exemples visant à simuler nos interactions manuelles avec les modèles au cours du processus.

Nous estimons que la recherche exploratoire innovante constitue peut-être le moyen le plus important d'évaluer les capacités des modèles d'IA de nouvelle génération. Les benchmarks sont utiles, mais ils peuvent passer à côté de certains des aspects les plus complexes de la recherche : soutenir de longues chaînes de raisonnement, choisir les bonnes abstractions, gérer l'ambiguïté dans les énoncés de problèmes et présenter des arguments à la hauteur de l'examen minutieux des experts. Les défis de pointe tels que First Proof nous aident à tester ces capacités dans des contextes où la vérification de l'exactitude n'est pas triviale et où les modes de défaillance sont instructifs.

Nous avons exécuté le modèle avec une supervision humaine limitée. Lors de la suggestion de versions du modèle au cours de la formation, nous avons parfois proposé de réessayer des stratégies qui s'étaient révélées fructueuses lors de tentatives précédentes. Pour certaines tentatives, nous avons demandé au modèle de développer ou de clarifier certaines parties d'une preuve après avoir reçu le feedback d'experts, afin de faciliter la vérification du raisonnement. Nous avons également facilité les échanges entre ce modèle et ChatGPT à des fins de vérification, de mise en forme et de style. Pour certains problèmes, nous présentons la meilleure des quelques tentatives, sélectionnée à l'issue d'un jugement humain. Il s'agissait d'un sprint rapide, et notre processus n'était pas aussi rigoureux que nous l'aurions souhaité dans le cadre d'une évaluation correctement contrôlée. Nous sommes impatients de rencontrer les organisateurs de First Proof afin de discuter d'un cadre d'expérimentation et d'évaluation plus rigoureux pour les prochaines itérations.

Ce travail s'appuie sur les résultats antérieurs obtenus à partir de modèles de raisonnement de pointe en mathématiques et en sciences. En juillet 2025, nous avons atteint un niveau de performance médaillé d'or⁠(ouverture dans une nouvelle fenêtre) aux Olympiades internationales de mathématiques grâce à un modèle de raisonnement polyvalent (35/42 points). En novembre 2025, nous avons partagé « Premières expériences pour accélérer la recherche scientifique avec GPT‑5 », un ensemble d'études de cas dans lesquels GPT‑5 a aidé des chercheurs à réaliser des progrès concrets en mathématiques, physique, biologie et dans d'autres domaines, ainsi que les limites que nous avons observées. Et plus récemment, nous avons rendu compte d'une collaboration en physique dans le cadre de laquelle GPT‑5.2 a proposé une expression candidate pour une formule d'amplitude de gluon qui a ensuite été formellement prouvée par un modèle interne et vérifiée par les auteurs.

Nous sommes impatients de collaborer plus étroitement avec la communauté sur la manière d'évaluer le raisonnement de niveau recherche, y compris le feedback d'experts sur ces tentatives, et nous sommes ravis de mettre ces nouvelles fonctionnalités à disposition dans les futurs modèles publics.