Le nostre proposte per First Proof
Condividiamo i nostri tentativi di dimostrazione per First Proof, una sfida matematica che mette alla prova la capacità dell’IA di produrre dimostrazioni verificabili su problemi specifici di settore.
Abbiamo eseguito un modello interno su tutti e 10 i problemi di First Proof(si apre in una nuova finestra), una sfida matematica a livello di ricerca progettata per verificare se i sistemi di IA possono produrre tentativi di dimostrazione corretti e verificabili. A differenza della matematica a risposta breve o da competizione, questi problemi richiedono la formulazione di argomentazioni complete in domini specialistici e la correttezza è difficile da stabilire senza la revisione di esperti. Gli autori dei problemi di First Proof sono esperti di fama mondiale nei rispettivi campi e almeno un paio dei problemi sono rimasti irrisolti per anni prima che gli autori trovassero delle soluzioni. Un dipartimento accademico con significative competenze nelle aree tematiche coinvolte potrebbe, in teoria, risolvere molti dei problemi in una settimana.
Abbiamo condiviso(si apre in una nuova finestra) i nostri tentativi di prova sabato 14 febbraio 2026 alle 00:00 PT. Sulla base del feedback degli esperti, riteniamo che almeno cinque dei tentativi di dimostrazione del modello (problemi 4, 5, 6, 9 e 10) abbiano un'alta probabilità di essere corretti, mentre diversi altri sono ancora in fase di revisione. Inizialmente credevamo che il nostro tentativo per il problema n.2 fosse probabilmente corretto. Sulla base dei commenti ufficiali di First Proof e di ulteriori analisi della community, riteniamo ora che non sia corretto. Siamo grati per il coinvolgimento e attendiamo con interesse la revisione continua. Il nostro set completo di tentativi di dimostrazione è disponibile qui(si apre in una nuova finestra). Il preprint include tutti e dieci i tentativi di dimostrazione, oltre a un'appendice recentemente aggiunta con schemi di prompt ed esempi che mirano a simulare le nostre interazioni manuali con i modelli durante il processo.
Crediamo che la ricerca di frontiera innovativa sia forse il modo più importante per valutare le capacità dei modelli di IA di prossima generazione. I benchmark sono utili, ma possono non cogliere alcune delle parti più difficili della ricerca, come sostenere lunghe catene di ragionamento, scegliere le giuste astrazioni, gestire l’ambiguità negli enunciati dei problemi e produrre argomentazioni che superino il vaglio degli esperti. Sfide di frontiera come First Proof ci aiutano a testare queste capacità in contesti in cui la correttezza è difficile da verificare e le modalità di fallimento forniscono informazioni utili.
“Stiamo attualmente addestrando un nuovo modello, il cui obiettivo principale è quello di aumentare il livello di rigore nel suo ragionamento, così da poter pensare per molte ore consecutive e restare altamente sicuro delle proprie conclusioni. Quando sono stati annunciati, i problemi di First Proof sembravano il banco di prova perfetto, quindi nel fine settimana l'ho provato. Già era riuscito a risolvere due dei problemi (n. 9 e n. 10). Via via che veniva addestrato, diventava sempre più capace, arrivandone infine a risolvere, a nostro avviso, almeno altri tre. Siamo stati particolarmente soddisfatti quando ha risolto il problema n. 6 e poi, due giorni dopo, il n. 4, poiché si trattava di problemi provenienti da ambiti familiari a molti di noi. È davvero incredibile vedere un modello diventare sempre più intelligente, giorno dopo giorno".
– James R. Lee (OpenAI Researcher, Reasoning)
Abbiamo eseguito il modello con supervisione umana limitata. Nel corso del prompting delle versioni del modello durante l'addestramento, a volte abbiamo suggerito strategie di ripetizione che si erano dimostrate utili nei tentativi precedenti. Per alcuni tentativi, abbiamo chiesto al modello di espandere o chiarire parti di una dimostrazione dopo avere ricevuto il feedback degli esperti, per rendere il ragionamento più facile da verificare. Abbiamo anche facilitato uno scambio tra questo modello e ChatGPT per la verifica, la formattazione e lo stile. Per alcuni problemi, presentiamo il meglio di alcuni tentativi, scelti in base al giudizio umano. Questo è stato uno sprint veloce e il nostro processo non è stato così ordinato come avremmo desiderato in una valutazione adeguatamente controllata. Non vediamo l'ora di discutere con gli organizzatori di First Proof un quadro sperimentale e di valutazione più rigoroso per le future iterazioni.
Questo lavoro si basa su risultati precedenti di modelli di ragionamento di frontiera nel campo della matematica e delle scienze. Nel luglio 2025, abbiamo ottenuto una prestazione da medaglia d'oro(si apre in una nuova finestra) alle Olimpiadi Internazionali di Matematica con un modello di ragionamento generico (35/42 punti). Nel novembre 2025, abbiamo condiviso “Early experiments in accelerating science with GPT‑5”, una serie di casi studio in cui GPT‑5 ha aiutato i ricercatori a fare progressi concreti in matematica, fisica, biologia e altri campi, insieme alle limitazioni che abbiamo osservato. Più recentemente abbiamo annunciato una collaborazione in fisica in cui GPT‑5.2 ha proposto un'espressione candidata per una formula di ampiezza del gluone, successivamente formalmente dimostrata da un modello interno e verificata dagli autori.
Non vediamo l’ora di interagire più a fondo con la comunità sulla valutazione del ragionamento di livello di ricerca, inclusi i feedback degli esperti su questi tentativi, e siamo lieti di rendere disponibili queste nuove funzionalità nei modelli pubblici futuri.
Autore
Continua a leggere
