Innsent efni fyrir First Proof

Við keyrðum innra líkan á öllum 10 First Proof⁠(opnast í nýjum glugga) dæmunum, rannsóknarstigs stærðfræðiáskorun sem er hönnuð til að prófa hvort gervigreindarkerfi geti skapað réttar, yfirfarðar sönnunartilraunir. Ólíkt stuttum svörum eða keppnisstærðfræði, krefjast þessi verkefni þess að byggja upp heildstæð rök á sérhæfðum sviðum, og erfitt er að staðfesta réttmæti án yfirferðar sérfræðings. Höfundar First Proof dæmanna eru leiðandi sérfræðingar á sínum sviðum, og að minnsta kosti tvö dæmanna voru óleyst í mörg ár áður en höfundarnir fundu lausnir. Deild innan háskóla sem hefur verulega skörun við viðfangsefnin gæti hugsanlega leyst mörg dæmin á einni viku.

Við deildum⁠(opnast í nýjum glugga) sönnunartilraunum okkar laugardaginn 14. febrúar 2026 kl. 00:00 PT. Byggt á endurgjöf frá sérfræðingum teljum við að að minnsta kosti fimm af sönnunartilraunum líkansins (dæmi 4, 5, 6, 9 og 10) hafi miklar líkur á að vera réttar og nokkur önnur eru enn til skoðunar. Við töldum í upphafi að tilraun okkar við dæmi 2 væri líklega rétt. Með hliðsjón af opinberum athugasemdum við First Proof og frekari greiningu samfélagsins teljum við nú að þetta sé rangt. Við erum þakklát fyrir þátttökuna og hlökkum til áframhaldandi endurskoðunar. Allar sönnunartilraunir okkar má finna hér⁠(opnast í nýjum glugga). Forprentið inniheldur allar tíu sönnunartilraunirnar, auk nýlega bætts viðauka með kvaðningamynstrum og dæmum sem miða að því að líkja eftir handvirkum samskiptum okkar við líkönin á meðan á ferlinu stendur.

Við teljum að nýstárleg rannsókn á framarlegum sviðum sé ef til vill mikilvægasta leiðin til að meta getu næstu kynslóðar gervigreindarlíkana. Viðmið eru gagnleg, en þau geta misst af sumum erfiðustu þáttum rannsókna: að viðhalda löngum röksemdafærslum, að velja réttar abstraksjónir, að takast á við óvissu í dæmalýsingum og að setja fram rök sem standast gagnrýna skoðun sérfræðinga. Framarlegar áskoranir eins og First Proof hjálpa okkur að álagsprófa þessa getu í aðstæðum þar sem réttmæti er ekki auðvelt að sannreyna og bilunarhættirnir veita gagnlegar upplýsingar.

Við keyrðum líkanið með takmörkuðu mannlegu eftirliti. Þegar við gáfum útgáfum af líkaninu kvaðningu á meðan á þjálfun stóð, lögðum við stundum til endurtekningaraðferðir sem höfðu reynst árangursríkar í fyrri tilraunum. Í sumum tilraunum báðum við líkanið um að útvíkka eða skýra hluta af sönnuninni eftir að hafa fengið ábendingar frá sérfræðingum, til að auðvelda sannprófun rakanna. Við auðvelduðum einnig samskipti fram og til baka milli þessa líkans og ChatGPT til staðfestingar, uppsetningar og stíls. Fyrir sum dæmi sýnum við bestu tilraunina úr nokkrum, valda með mannlegri dómgreind. Þetta var hraður sprettur og ferlið okkar var ekki eins snyrtilegt og við myndum vilja í vel stýrðu mati. Við hlökkum til að ræða við skipuleggjendur First Proof um strangari tilraun og matsramma fyrir framtíðarítranir.

Þetta verk byggir á fyrri niðurstöðum frá framarlega rakalíkönum í stærðfræði og vísindum. Í júlí 2025 náðum við gullverðlaunaárangri⁠(opnast í nýjum glugga) á Alþjóðlegu Stærðfræðikeppninni með almennu rakalíkani (35/42 stig). Í nóvember 2025 deildum við „Fyrstu tilraunir til að flýta fyrir vísindum með GPT‑5“, safni dæmisagna þar sem GPT‑5 hjálpaði vísindamönnum að ná áþreifanlegum framförum í stærðfræði, eðlisfræði, líffræði og öðrum sviðum, ásamt þeim takmörkunum sem við urðum vör við. Og nýlega greindum við frá samstarfi á sviði eðlisfræði þar sem GPT‑5.2 lagði til mögulega framsetningu fyrir formúlu um límeindabreidd sem síðan var formlega sönnuð af innra líkani og staðfest af höfundunum.

Við hlökkum til aukna þátttöku af samfélaginu um hvernig eigi að meta rök á rannsóknarstigi, þar á meðal að fá endurgjöf frá sérfræðingum um þessar tilraunir, og við erum spennt að gera þessa nýju getu aðgengilega í framtíðar opinberum líkönum.