Ang aming mga isinumite para sa First Proof
Ibinabahagi namin ang aming mga pagtatangka sa patunay para sa First Proof, isang hamon sa matematika na sumusubok kung makakagawa ang AI ng mga matatasang patunay sa mga problema na partikular sa domain.
Nagpatakbo kami ng panloob na modelo sa 10 First Proof(magbubukas sa bagong window) na problema, isang hamon sa antas ng pananaliksik sa matematika na dinisenyo upang subukan kung makakagawa ang mga sistema ng AI ng tama at masusuring mga pagtatangka ng patunay. Hindi tulad ng short-answer o estilong kompetisyon sa matematika, ang mga problemang ito ay nangangailangan ng pagbuo ng end-to-end na mga argumento sa mga espesyalisadong domain, at mahirap matiyak ang pagiging tama nang walang pagsusuri ng eksperto. Ang mga may-akda ng mga problema sa First Proof ay mga nangungunang eksperto sa kani-kanilang larangan, at hindi bababa sa dalawa sa mga problemang ito ay nanatiling bukas sa loob ng maraming taon bago nakahanap ng solusyon ang mga may-akda. Ang isang akademikong departamento na malawak ang saklaw sa mga larangan ng paksa ay maaaring makalutas ng marami sa mga problema sa loob ng isang linggo.
Kami ay nagbahagi(magbubukas sa bagong window) ng aming mga pagtatangka sa patunay noong Sabado, Pebrero 14, 2026, sa 12:00 AM PT. Batay sa feedback mula sa mga eksperto, naniniwala kami na hindi bababa sa lima sa mga pagtatangka ng patunay ng modelo (mga problema 4, 5, 6, 9, at 10) ay may mataas na tsansang tama, at ilan pa ang nananatiling sinusuri. Sa simula, naniniwala kami na malamang tama ang aming pagtatangka para sa problem 2. Batay sa opisyal na komentaryo ng First Proof at karagdagang pagsusuri ng komunidad, naniniwala kami ngayon na mali ito. Nagpapasalamat kami sa inyong paglahok at umaaso kami sa patuloy na pagsusuri. Makikita dito(magbubukas sa bagong window) ang aming buong pangkat ng mga pagtatangka sa patunay. Kasama sa preprint ang sampung pagtatangka sa patunay, pati na rin ang bagong idinagdag na apendise na naglalaman ng mga pattern ng prompt at mga halimbawa na naglalayong gayahin ang aming mga manu-manong pakikipag-ugnayan sa mga modelo sa panahon ng proseso.
Naniniwala kami na ang makabagong frontier na pananaliksik ay marahil ang pinakamahalagang paraan upang suriin ang mga kakayahan ng susunod na henerasyon ng mga modelo ng AI. Kapaki-pakinabang ang mga pamantayan, ngunit maaaring hindi nila masaklaw ang ilan sa pinakamahihirap na bahagi ng pananaliksik: tuloy-tuloy at matagalang pangangatuwiran, pagpili ng tamang mga abstraksyon, pangaganiswa ng hindi malinaw na mga pahayag ng problema, at pagbuo ng mga argumento na papasa sa masusing pagsusuri ng mga eksperto. Ang mga hamon sa frontier tulad ng First Proof ay tumutulong sa amin na subukan ang mga kakayahan sa mga sitwasyon kung saan mahirap berepikahin ang tamang resulta at kung saan nagbibigay-kaalaman ang mga mode ng pagkabigo.
“Kasalukuyan naming sinasanay ang isang bagong modelo na ang pangunahing pokus ay ang pagtataas ng antas ng kahigpitan sa pag-iisip nito, kung saan ang layunin ay makapag-isip ang modelo nang tuluy-tuloy sa loob ng maraming oras at manatiling lubos na sigurado sa mga konklusyon nito. Nang ianunsyo ang mga problema sa First Proof, tila ito ang perpektong testbed, kaya't sinubukan ko ito noong katapusan ng linggo. Nakalutas na ito ng dalawa sa mga problema (#9 at #10). Habang ito ay nagsasanay, ito ay naging mas may kakayahan, at sa huli, ayon sa aming pagtataya, nalutas nito ang hindi bababa sa tatlo pa. Labis kaming natuwa nang nalutas nito ang #6 at pagkatapos, makalipas ang dalawang araw, ang #4, dahil ang mga problemang iyon ay mula sa mga larangang pamilyar sa marami sa amin. "Talagang kahanga-hangang panoorin ang isang modelo na nagiging mas matalino sa malinaw na paraan araw-araw.”
– James R. Lee (Mananaliksik ng OpenAI, Pangangatuwiran)
Pinatakbo namin ang modelo na may limitadong pangangasiwa ng tao. Kapag nagpo-prompt ng mga bersyon ng modelo habang nagsasanay, paminsan-minsan ay nagmumungkahi kami ng mga estratehiya sa muling pagsubok na nagpakita ng tagumpay sa mga naunang pagtatangka. Para sa ilang pagtatangka, hiniling namin sa modelo na palawakin o linawin ang ilang bahagi ng patunay matapos makatanggap ng feedback mula sa mga eksperto, upang gawing mas madali ang pagbeberipika ng pangangatuwiran. Pinadali rin namin ang pagpapalitan ng impormasyon sa pagitan ng modelong ito at ChatGPT para sa pagbeberipika, pag-format, at estilo. Para sa ilang problema, ipinapakita namin ang pinakamahusay mula sa ilang pagtatangka, na pinili batay sa paghatol ng tao. Naging mabilis ito, at ang proseso namin ay hindi kasing linis gaya ng hinangad namin sa maayos at kontroladong pagsusuri. Inaasahan namin ang mga talakayan kasama ang mga tagapag-ayos ng First Proof tungkol sa mas mahigpit na balangkas ng eksperimento at pagsusuri para sa mga susunod na bersyon.
Ang gawaing ito ay nakabatay sa mga naunang resulta mula sa mga modelong frontier na nangangatuwiran sa matematika at agham. Noong Hulyo 2025, naabot namin ang antas ng pagganap na katumbas ng gintong medalya(magbubukas sa bagong window) sa International Mathematical Olympiad gamit ang modelo na karaniwan ang pangagatuwiran (35/42 puntos). Noong Nobyembre 2025, ibinahagi namin ang “Mga unang eksperimento sa pagpapabilis ng agham gamit ang GPT‑5”, isang pangkat ng mga pag-aaral ng kaso kung saan tinulungan ng GPT‑5 ang mga mananaliksik na makagawa ng kongkretong pag-unlad sa matematika, pisika, biyolohiya, at iba pang larangan, kasama ang mga limitasyong naobserbahan namin. At kamakailan lang, inulat namin ang isang kolaborasyon sa pisika kung saan iminungkahi ng GPT‑5.2 ang isang kandidatong ekspresyon para sa pormula ng gluon-amplitude na pagkatapos ay pormal na pinatunayan ng isang panloob na modelo at sinuri ng mga may-akda.
Inaasahan namin ang mas malalim na pakikipag-ugnayan sa komunidad tungkol sa kung paano suriin ang pangangatuwiran na para sa pananaliksik, kabilang ang feedback ng eksperto sa mga pagtatangkang ito, at nasasabik kaming magamit ang bagong kakayahang ito sa mga susunod na pampublikong modelo.
