Нашиот поднесок за First Proof

Извршивме внатрешен модел на сите 10 проблеми од First Proof⁠(се отвора во нов прозорец), истражувачки математички предизвик дизајниран да тестира дали системите за вештачка интелигенција можат да произведат точни и проверливи обиди за докази. За разлика од кратки одговори или натпреварувачка математика, овие проблеми бараат градење на целосни аргументи во специјализирани области, а точноста е тешко да се утврди без преглед од експерт. Авторите на проблемите од First Proof се водечки експерти во своите области, и барем неколку од проблемите беа отворени со години пред авторите да ги најдат решенијата. Академски оддел со значително преклопување во предметните области би можел да реши многу од проблемите за една недела.

Ние споделивме⁠(се отвора во нов прозорец) наши обиди за докажување во сабота, 14.02.2026 г. во 00:00 ч. по пацифичко време. Врз основа на повратните информации од експертите, веруваме дека најмалку пет од обидите за докажување на моделот (проблеми 4, 5, 6, 9 и 10) имаат голема веројатност да бидат точни, а неколку други сè уште се разгледуваат. На почетокот верувавме дека нашиот обид за проблем 2 е веројатно точен. Врз основа на официјалниот коментар за First Proof и понатамошната анализа на заедницата, сега веруваме дека тоа е неточно. Благодарни сме за ангажманот и со нетрпение очекуваме понатамошен преглед. Целосниот збир на нашите обиди за доказ може да се најде овде⁠(се отвора во нов прозорец). Претходниот принт ги вклучува сите десет обиди за докажување, плус новододаден додаток со шаблони за промптови и примери кои имаат за цел да ги симулираат нашите рачни интеракции со моделите за време на процесот.

Веруваме дека новото гранично истражување е можеби најважниот начин за оценување на способностите на моделите на вештачка интелигенција од следната генерација. Реперите се корисни, но можат да пропуштат некои од најтешките аспекти на истражувањето: одржување долги синџири на расудување, избор на соодветни апстракции, справување со двосмисленост во изјавите за проблемот и создавање аргументи што издржуваат стручна проверка. Гранични предизвици како First Proof ни помагаат да ги тестираат тие способности во услови каде што е тешко да се провери точноста, а режимите на неуспех даваат корисни информации.

Го извршивме моделот со ограничен човечки надзор. Кога предлагавме верзии на моделот за време на обуката, понекогаш препорачувавме стратегии за повторен обид кои се покажаа успешни во претходните обиди. За некои обиди, го замоливме моделот да ги прошири или разјасни деловите од доказот откако добивме повратни информации од експерти, за да биде расудувањето полесно за проверка. Ние исто така овозможивме размена на информации помеѓу овој модел и ChatGPT за верификација, форматирање и стил. За некои проблеми, го прикажуваме најдоброто од неколку обиди, избрано со човечка проценка. Ова беше брз спринт, и нашиот процес не беше толку уреден како што би сакале во правилно контролирана евалуација. Со нетрпение очекуваме дискусии со организаторите на First Proof за поригорозен експеримент и рамка за евалуација за идните итерации.

Оваа работа се надоврзува на претходни резултати од гранични модели со расудување во математиката и науката. Во јули 2025 година, постигнавме перформанси на ниво на златен медал⁠(се отвора во нов прозорец) на Меѓународната математичка олимпијада со модел со расудување за општа намена (35/42 поени). Во ноември 2025 г., споделивме „Рани експерименти за забрзување на науката со GPT‑5“, збирка од студии на случај каде што GPT‑5 им помогна на истражувачите да постигнат конкретен напредок во математиката, физиката, биологијата и други области, заедно со ограничувањата што ги забележавме. И најнеодамна, известивме за соработка во физиката каде што GPT‑5.2 предложи кандидатски израз за формула за амплитуда на глуони, која потоа беше формално докажана од внатрешен модел и потврдена од авторите.

Со нетрпение очекуваме подлабока соработка со заедницата за тоа како да се оценува расудување на истражувачко ниво, вклучувајќи експертски повратни информации за овие обиди, и возбудени сме што ќе ги направиме овие нови можности достапни во идните јавни модели.