GPT-F è un prover automatizzato e un assistente di prova per il linguaggio di formalizzazione Metamath.
Recentemente, i ricercatori di OpenAI hanno introdotto GPT-F, un prover automatizzato e un assistente di prova per il linguaggio di formalizzazione Metamath. In un documento intitolato “Generative Language Modeling for Automated Theorem Proving”, i ricercatori hanno affermato che una comunità matematica formale ha approvato per la prima volta la dimostrazione di un sistema basato sull’apprendimento profondo.
Le reti neurali profonde hanno fatto passi da gigante nella comprensione del linguaggio, visione artificiale, riconoscimento vocale, generazione di immagini e altro ancora. Tuttavia, le capacità di ragionamento dei modelli di apprendimento profondo a volte sono insufficienti. Per affrontare l’inadeguatezza, i ricercatori hanno introdotto GPT-F applicando un modello di linguaggio del trasformatore alla dimostrazione automatizzata di teoremi.
Dietro GPT-F
I ricercatori hanno utilizzato la libreria Metamath come ambiente formale poiché le caratteristiche di Metamath consentono una prototipazione più rapida e tempi di iterazione ridotti a breve termine. Per l’architettura del modello, i ricercatori hanno utilizzato trasformatori solo decoder simili a GPT-2 e GPT-3. Il modello più grande che hanno studiato ha 36 strati e 774 milioni di parametri addestrabili.
Metamath è alimentato da un semplice sistema meta-logico basato su una singola regola di sostituzione. I ricercatori hanno affermato che la libreria principale di Metamath si chiama set.mm, una raccolta di circa 38.000 prove basata sulla teoria degli insiemi ZFC.
La verifica è rapida e può essere implementata in centinaia di righe di codice
I passaggi di prova sono privi di contesto.
L’accesso alle rappresentazioni degli obiettivi secondari pulite e compatte rende la ricerca dell’albero delle prove semplice in modo relativo.
set.mm è una delle più grandi librerie disponibili ed è compatibile con la matematica moderna.
“Uso lo strumento da un po ‘di tempo. Lo stato del database mm è che ha la conoscenza di uno studente universitario avanzato codificato in esso, circa 35k teoremi finora, puoi verificarlo qui. Lo strumento è quindi utile per scrivere nuove prove nel database. Quindi è ancora abbastanza lontano dalle frontiere della matematica. La maggior parte del lavoro al momento è codificare sempre di più ciò che è già stato dimostrato prima di affrontare teoremi non dimostrati. Tuttavia, GPT-F ha trovato nuove dimostrazioni, che sono più brevi ed eleganti, per teoremi attualmente provati. Direi anche, dall’uso dello strumento, che è meglio provare le cose di me, il che è piuttosto interessante “, ha detto un utente di Reddit .
Contributi
I ricercatori hanno verificato che la pre-formazione generativa migliora sostanzialmente le prestazioni e che la pre-formazione su dati matematici porta a prestazioni migliori rispetto alla pre-formazione su testo generico dal web.
Hanno scoperto che la dimensione del modello è positivamente correlata alle prestazioni, anche se la dimensione del set di dati Metamath è relativamente piccola.
I ricercatori hanno anche dimostrato che l’addestramento iterativo di una funzione di valore sulle dichiarazioni generate dal loro modello di linguaggio porta a miglioramenti nelle prestazioni di GPT-F.
Il modello migliore ha chiuso il 56,22% delle prove da un set di test tenuto fuori e ha dimostrato che l’architettura Transformer potrebbe essere adatta per il ragionamento formale.
