Meie First Proofi raames esitatu
Jagame esimese tõestuse jaoks oma tõestuskatseid - First Proof on on matemaatikaväljakutse, mis testib, kas tehisintellekt suudab domeenipõhiste probleemide kohta koostada kontrollitavaid tõestusi.
Käivitasime sisemise mudeli kõigi 10 First Proof(avaneb uues aknas) ülesande jaoks, mis on uurimistöö tasemel matemaatika väljakutse, et testida, kas TI-süsteemid suudavad koostada korrektseid, kontrollitavaid tõestuskatseid. Erinevalt lühivastustega või võistlusstiilis matemaatikast nõuavad need probleemid spetsialiseeritud valdkondades argumentide otsast lõpuni konstrueerimist ning nende korrektsust on ilma eksperthinnanguta raske kindlaks teha. First Proofi probleemide autorid on oma valdkondade juhtivad eksperdid ning vähemalt paar probleemi olid aastaid lahendamata, enne kui autorid neile lahendused leidsid. Akadeemiline osakond, millel on märkimisväärne kattuvus õppevaldkondadega, võiks teoreetiliselt lahendada paljud probleemid ühe nädalaga.
Me jagasime(avaneb uues aknas) oma tõestuskatseid laupäeval, 14. veebruaril 2026 kell 12:00 PT. Ekspertide käest saadud tagasiside põhjal usume, et vähemalt viiel mudeli tõestuskatsetest (ülesanded 4, 5, 6, 9 ja 10) on suur tõenäosus olla õiged ning mitmed teised on endiselt läbivaatamisel. Alguses arvasime, et meie katse ülesande 2 lahendamiseks oli tõenäoliselt õige. Ametliku First proofi kommentaari ja täiendava kogukondliku analüüsi põhjal usume nüüd, et see on ebaõige. Me oleme tänulikud kaasamise eest ja ootame huviga jätkuvat ülevaatamist. Meie täieliku tõestuskatsete komplekti leiad siit(avaneb uues aknas). Eeltrükk sisaldab kõiki kümmet tõestuskatset, lisaks äsja lisatud lisa viibamustrite ja näidetega, mille eesmärk on simuleerida seda, milline oli protsessi käigus meie manuaalne suhtlus mudelitega.
Me usume, et uudne eesrindlik uurimistöö on võib-olla kõige olulisem viis järgmise põlvkonna TI-mudelite võimekuse hindamiseks. Võrdlusalused on kasulikud, kuid need võivad mööda vaadata mõnest uurimistöö kõige raskemast osast: pikkade arutluste säilitamine, õigete abstraktsioonide valimine, probleemikirjelduste mitmetimõistetavuse käsitlemine ning selliste argumentide esitamine, mis peavad vastu ekspertide kriitikale. Tipptasemel väljakutsed, nagu First Proof, aitavad meil neid võimekusi stressitestida olukordades, kus korrektsust on keeruline kontrollida ja kus ebaõnnestumise viisid pakuvad väärtuslikku teavet.
“Me treenime praegu uut mudelit, mille peamine eesmärk on suurendada selle mõtlemise rangust, et mudel suudaks pidevalt mõelda mitu tundi ja jääda oma järeldustes väga kindlaks. Kui First Proofi probleemid välja kuulutati, tundus see ideaalne katseplatvorm, nii et proovisin seda nädalavahetusel. See suutis juba lahendada kaks probleemi (nr 9 ja nr 10). Treeningu käigus muutus see üha võimekamaks, lahendades lõpuks – meie hinnangul – vähemalt veel kolm ülesannet. Meil oli eriti hea meel, kui see lahendas probleemi nr 6 ja siis, kaks päeva hiljem, nr 4, kuna need probleemid olid valdkondadest, mis olid paljudele meist tuttavad. "On üsna uskumatu jälgida, kuidas mudel muutub päev-päevalt käegakatsutavalt nutikamaks.”
– James R. Lee (OpenAI teadlane, arutlus)
Käitasime mudelit piiratud inimjärelevalve all. Kui mudeli versioone treenimise käigus viipasime, soovitasime mõnikord uuesti katsetamise strateegiaid, mis olid varasematel juhtudel paljulubavad. Mõne katse puhul palusime mudelil pärast ekspertide tagasiside saamist tõestuse osi laiendada või täpsustada, et oleks lihtsam arutluskäiku verifitseerida. Samuti hõlbustasime edasi-tagasi suhtlust selle mudeli ja ChatGPT vahel verifitseerimiseks, vormindamiseks ja stiili kohandamiseks. Mõne probleemi puhul esitame erinevate katsete seast valitud parima katse, parima katse on valinud inimene oma otsustusvõime alusel. See oli kiire sprint ja meie protsess ei olnud nii puhas, kui me sooviksime korralikult kontrollitud hindamise korral. Ootame põnevusega arutelusid First Proofi korraldajatega rangema eksperimendi- ja hindamisraamistiku osas tulevaste iteratsioonide jaoks.
See töö tugineb varasematele tulemustele tipptasemel arutlusmudelitest matemaatikas ja teaduses. 2025. aasta juulis tegime rahvusvahelisel matemaatikaolümpiaadil üldotstarbelise arutlusmudeliga kuldmedali väärilise soorituse(avaneb uues aknas) (35/42 punkti). 2025. aasta novembris jagasime “Varased katsed teaduse kiirendamiseks GPT‑5‑ga” – juhtumiuuringute kogumit, kus GPT‑5 aitas teadlastel saavutada konkreetseid edusamme matemaatikas, füüsikas, bioloogias ja teistes valdkondades, koos meie täheldatud piirangutega. Ja kõige hiljutisemalt teatasime füüsikaalases koostöös, kus GPT‑5.2 pakkus välja gluuoni amplituudi valemi jaoks kandidaatavaldisi, mille seejärel formaalselt tõestas sisemine mudel ja mille autorid kinnitasid.
Ootame põnevusega sügavamat koostööd kogukonnaga, et arutada, kuidas hinnata uurimistöö tasemel arutlust, sealhulgas saada ekspertide tagasisidet nende katsete kohta. Me oleme põnevil, et saame need uued võimalused tulevastes avalikes mudelites kättesaadavaks teha.
Autor
Jätka lugemist
