Naši rezultati na izzivu First Proof
Predstavljamo naše poskuse podajanja dokazov za First Proof, sklop zahtevnih matematičnih problemov, ki preverja, ali lahko umetna inteligenca (UI) pripravi dokaze, ki jih je mogoče preveriti, za domensko specifične probleme.
Interni model smo uporabili pri vseh 10 problemih First Proof(odpre se v novem oknu), raziskovalnem matematičnem izzivu, zasnovanem za preverjanje, ali lahko sistemi umetne inteligence pripravijo pravilne in preverljive poskuse podajanja dokazov. Za razliko od nalog s kratkim odgovorom ali tekmovalne matematike ti problemi zahtevajo oblikovanje argumentov od začetka do konca v specializiranih domenah, pri čemer je pravilnost brez strokovnega pregleda težko zanesljivo ugotoviti. Avtorji problemov First Proof so vodilni strokovnjaki na svojih področjih, pri čemer sta bila vsaj dva problema odprta več let, preden so avtorji našli rešitve. Akademski oddelek, ki ima znatno vsebinsko prekrivanje s temi področji, bi lahko v enem tednu rešil številne probleme.
Poskuse podajanja dokazov smo objavili(odpre se v novem oknu) v soboto, 14. februarja 2026, ob 12.00 po pacifiškem času (PT). Na podlagi povratnih informacij strokovnjakov menimo, da ima vsaj pet poskusov podajanja dokazov modela (problemi 4, 5, 6, 9 in 10) visoko verjetnost pravilnosti, več drugih pa je še vedno v postopku pregleda. Sprva smo menili, da je naš poskus za problem 2 verjetno pravilen. Na podlagi uradnega komentarja First Proof in nadaljnje analize skupnosti zdaj menimo, da je napačen. Hvaležni smo za sodelovanje in se veselimo nadaljnjega pregleda. Naš celoten nabor poskusov podajanja dokazov je dostopen tukaj(odpre se v novem oknu). Predtisk vključuje vseh deset poskusov podajanja dokazov ter na novo dodano prilogo z vzorci pozivov in primeri, katerih namen je simulirati naše ročne interakcije z modeli med postopkom.
Verjamemo, da je napredno raziskovanje morda najpomembnejši način za ocenjevanje zmožnosti modelov umetne inteligence naslednje generacije. Primerjalni preizkusi so uporabni, vendar lahko spregledajo nekatere najzahtevnejše vidike raziskovanja: vzdrževanje dolgih verig sklepanja, izbira ustreznih abstrakcij, obvladovanje dvoumnosti v besedilu problemov in oblikovanje argumentov, ki prestanejo strokovni nadzor. Napredni izzivi, kot je First Proof, nam omogočajo, da te zmožnosti izvedemo obremenitveni test v okoljih, kjer pravilnosti ni mogoče trivialno preveriti in so načini odpovedi informativni.
»Trenutno učimo nov model, pri katerem je glavni poudarek na povečanju ravni rigoroznosti pri razmišljanju, s ciljem, da lahko model neprekinjeno razmišlja več ur in ostane zelo prepričan o svojih zaključkih. Ko so objavili probleme First Proof, se je to zdelo kot popolno testno okolje, zato sem ga čez vikend preizkusil. Že takrat mu je uspelo rešiti dva problema (#9 in #10). Ko se je učil, je postajal vse bolj sposoben in je sčasoma rešil (po naši oceni) še vsaj tri. Še posebej smo bili zadovoljni, ko je rešil 6. problem in nato, dva dni pozneje še 4. problem, saj sta bila ta problema s področij, ki so mnogim od nas poznana. Res je neverjetno opazovati, kako model iz dneva v dan postaja otipljivo pametnejši.
– James R. Lee (raziskovalec pri OpenAI, sklepanje)
Model smo izvajali z omejenim človeškim nadzorom. Pri pozivanju različic modela med učenjem smo včasih predlagali ponovitev strategij, ki so se v prejšnjih poskusih izkazale za obetavne. Pri nekaterih poskusih smo modelu ukazali, naj po prejemu strokovnih povratnih informacij razširi ali pojasni dele dokaza, da bi bilo sklepanje lažje preveriti. Prav tako smo omogočili izmenjavo med tem modelom in ChatGPT‑jem za preverjanje, oblikovanje in slog. Pri nekaterih problemih predstavimo najboljše izmed nekaj poskusov, izbrane na podlagi človeške presoje. To je bila hitra izvedba, zato naš postopek ni bil tako čist, kot bi si želeli v ustrezno nadzorovani evalvaciji. Veselimo se razprav z organizatorji First Proof o bolj rigoroznem eksperimentu in evalvacijskem okviru za prihodnje iteracije.
To delo nadgrajuje prejšnje rezultate modelov sklepanja na meji zmogljivosti na področju matematike in naravoslovja. Julija 2025 smo z modelom sklepanja dosegli uspeh na ravni zlate medalje(odpre se v novem oknu) na Mednarodni matematični olimpijadi (35/42 točk). Novembra 2025 smo predstavili »Zgodnji eksperimenti pri pospeševanju znanosti z GPT‑5«, nabor študij primerov, v katerih je GPT‑5 raziskovalcem pomagal doseči konkreten napredek na področjih matematike, fizike, biologije in drugih ved, skupaj z omejitvami, ki smo jih pri tem opazili. Nedavno smo poročali tudi o sodelovanju na področju fizike, pri katerem je GPT‑5.2 predlagal izraz za formulo gluonske amplitude, ki ga je nato interni model formalno dokazal, avtorji pa preverili.
Veselimo se poglobljenega sodelovanja s skupnostjo o tem, kako ocenjevati sklepanje na ravni raziskav, vključno s strokovnimi povratnimi informacijami o teh poskusih, in navdušeni smo, da bomo te nove zmožnosti dali na voljo v prihodnjih javnih modelih.
Avtor
Berite naprej
