OpenAI mette i risultati matematici dove possono essere controllati

Una lista di problemi che un modello dice di avere risolto lascia fuori la domanda più importante: le dimostrazioni reggono? OpenAI ha pubblicato il 6 ottobre un insieme di risultati matematici in un repository GitHub, con procedure per revisioni e citazioni.

Nel repository sono presenti formalizzazioni di molte dimostrazioni in Lean, un linguaggio che consente il controllo matematico da parte del computer. OpenAI prevede di aggiungerne altre. Pubblicazione di un manoscritto e verifica formale restano quindi passaggi distinti.

L’azienda condivide anche dieci sintesi del ragionamento del modello, statistiche sui problemi tentati e stime della potenza di calcolo impiegata. Per il risultato medio indica un consumo equivalente a circa tre ore di elaborazione di ChatGPT Pro. Il modello che ha prodotto i risultati è interno; la società dice di lavorare al suo rilascio.

OpenAI ha consultato il gruppo indipendente su matematica e AI dell’Institute for Advanced Study per le modalità di divulgazione. Il vantaggio di questi materiali è concreto: danno alla comunità qualcosa da esaminare, correggere e citare, invece di chiedere fiducia in una classifica aziendale.