LANTERN: alla luce le conoscenze matematiche nascoste nei modelli linguistici

Abstract degli autori

I modelli linguistici sono ormai in grado di dimostrare teoremi, ma sono ancora le persone a decidere quali problemi affrontare. Ci chiediamo se le rappresentazioni interne di un modello possano aiutare a individuare connessioni matematiche promettenti. Abbiamo sviluppato LANTERN, un processo rapido ed efficiente in termini di costi che usa un classificatore applicato alle attivazioni di un modello preaddestrato per ordinare le possibili relazioni in base alla loro rilevanza. Seguono un filtraggio in più fasi, la formulazione di ipotesi, una verifica eseguibile e un controllo analitico. Applicato alla On-Line Encyclopedia of Integer Sequences (OEIS), LANTERN ha classificato 50 milioni di coppie tra 10.000 sequenze citate di frequente e ha prodotto 62 relazioni verificate tra coppie prive di un rimando incrociato già esistente nell’OEIS. Una selezione basata sul contenuto ha conservato 13 relazioni che vale la pena presentare; nove sono informative o illuminanti, tra cui quattro del tutto nuove per quanto ne sappiamo: nessuna compare nell’OEIS né nella letteratura individuata dalla nostra ricerca mirata. L’intero processo, dall’inizio alla fine, compresi l’addestramento del classificatore, la classificazione delle possibili relazioni, il filtraggio e la verifica, ha richiesto meno di 8 ore.