Imparare a scoprire matematica interessante

Abstract degli autori

Negli ultimi tempi, i modelli linguistici di grandi dimensioni (LLM) sono diventati sempre più capaci di risolvere problemi matematici avanzati, tra cui molti rimasti irrisolti per decenni. Questo apre la strada a un’espansione delle conoscenze matematiche su una scala senza precedenti. Tuttavia, anche se gli LLM potrebbero riuscire a formulare congetture e dimostrare sempre più teoremi, resta da capire se queste nuove conoscenze matematiche siano interessanti o utili. Definiamo l’interesse intrinseco di un teorema come il rapporto tra la lunghezza della sua dimostrazione e quella del suo enunciato. Mostriamo che questa misura è fortemente correlata a una misura estrinseca dell’utilità successiva di un teorema. Individuiamo nella difficoltà di una dimostrazione, dato un insieme di premesse, un elemento di base utile per calcolare queste metriche e addestriamo un modello 27B che prevede la difficoltà delle dimostrazioni con maggiore accuratezza rispetto ai modelli generalisti più avanzati. L’ottimizzazione in base alla nostra metrica produce un modello capace di generare teoremi più interessanti, riducendo al contempo la sovrapposizione sostanziale o totale con Mathlib dal 91,9% al 30,6% e mettendo così in evidenza la creazione di una maggiore quantità di matematica fuori distribuzione. Mostriamo che il nostro sistema può generare teoremi candidati, selezionare i più interessanti e ampliare iterativamente una libreria matematica che si espande autonomamente. Queste metriche forniscono un segnale pratico e quantificabile per classificare le congetture e guidare la ricerca di dimostrazioni all’interno di librerie matematiche formali. Il nostro approccio apre la strada a librerie matematiche verificate automaticamente, capaci di espandersi autonomamente e di scegliere enunciati di valore senza dipendere da obiettivi forniti dagli esseri umani.