Vores First Proof-indsendelser

Vi kørte en intern model på alle 10 First Proof⁠(åbner i et nyt vindue)-problemer, en matematisk udfordring på forskningsniveau designet til at teste, om AI-systemer kan producere korrekte, kontrollerbare bevisforsøg. I modsætning til kortfattede svar eller konkurrenceprægede matematikopgaver kræver disse problemer opbygning af sammenhængende argumenter inden for specialiserede områder, og det er svært at fastslå rigtigheden uden ekspertvurdering. Forfatterne af First Proof-problemerne er førende eksperter inden for deres respektive områder, og mindst et par af problemerne var uløste i årevis, før forfatterne fandt løsningerne. Et akademisk institut, der har betydelig overlapning med fagområderne, kunne tænkes at løse mange af problemerne på en uge.

Vi delte⁠(åbner i et nyt vindue) vores bevisforsøg lørdag den 14. februar 2026 kl. 12:00 AM PT. Baseret på feedback fra eksperter mener vi, at mindst fem af modellens bevisforsøg (problem 4, 5, 6, 9 og 10) har stor sandsynlighed for at være korrekte, mens flere andre stadig er under revision. Vi troede oprindeligt, at vores forsøg på at løse problem 2 sandsynligvis var korrekt. Baseret på den officielle First Proof-kommentar og yderligere analyse fra fællesskabet mener vi nu, at det er forkert. Vi er taknemmelige for engagementet og ser frem til fortsat gennemgang. Vores fulde sæt bevisforsøg kan findes her⁠(åbner i et nyt vindue). Fortrykket indeholder alle ti bevisforsøg plus et nyligt tilføjet appendiks med promptmønstre og eksempler, der har til formål at simulere vores manuelle interaktioner med modellerne under processen.

Vi mener, at banebrydende forskning måske er den vigtigste måde at evaluere kapaciteten i næste generations AI-modeller på. Benchmarks er nyttige, men de kan overse nogle af de sværeste dele af forskningen: at opretholde lange ræsonneringskæder, vælge de rigtige abstraktioner, håndtere tvetydigheder i problemformuleringer og frembringe argumenter, der kan modstå eksperters kritiske blik. Banebrydende udfordringer som First Proof hjælper os med at stressteste disse evner i situationer, hvor det er svært at verificere korrektheden, og hvor fejltilstandene er informative.

Vi kørte modellen med begrænset menneskelig overvågning. Når vi under træningen præsenterede versioner af modellen, foreslog vi nogle gange at gentage strategier, der havde vist sig frugtbare i tidligere forsøg. For nogle forsøg bad vi modellen om at udvide eller præcisere dele af et bevis efter at have modtaget feedback fra eksperter, så ræsonneringen blev lettere at verificere. Vi faciliterede også en dialog mellem denne model og ChatGPT for at sikre verifikation, formatering og stil. For nogle problemer præsenterer vi det bedste af nogle få forsøg, udvalgt ved menneskelig vurdering. Dette var en hurtig sprint, og vores proces var ikke så ren, som vi kunne ønske i en korrekt kontrolleret evaluering. Vi ser frem til drøftelser med First Proof-arrangørerne om en mere stringent ramme for eksperimenter og evaluering i fremtidige iterationer.

Dette arbejde bygger på tidligere resultater fra banebrydende ræsonneringsmodeller inden for matematik og naturvidenskab. I juli 2025 opnåede vi præstation på guldmedaljeniveau⁠(åbner i et nyt vindue) ved den internationale matematikolympiade med en generel ræsonneringsmodel (35/42 point). I november 2025 delte vi “Tidlige eksperimenter i at fremskynde videnskab med GPT‑5”, et sæt casestudier, hvor GPT‑5 hjalp forskere med at gøre konkrete fremskridt inden for matematik, fysik, biologi og andre felter, sammen med de begrænsninger, vi observerede. Og for nylig rapporterede vi om et fysiksamarbejde, hvor GPT‑5.2 foreslog et kandidatudtryk til en gluonamplitudeformel, som derefter blev formelt bevist af en intern model og verificeret af forfatterne.

Vi ser frem til et dybere engagement med fællesskabet om, hvordan man evaluerer ræsonnering på forskningsniveau, herunder ekspertfeedback på disse forsøg, og vi er begejstrede for at gøre disse nye funktioner tilgængelige i fremtidige offentlige modeller.