LLM possono generare dimostrazioni matematiche che possono essere rigorosamente verificate? Scopri LeanDojo un playground AI open-source con toolkit, benchmark e modelli per i Large Language Models per dimostrare teoremi formali nell’assistente di proof Lean.

LeanDojo è un playground AI open-source con toolkit, benchmark e modelli per i Large Language Models. È possibile utilizzarlo per dimostrare teoremi formali nell'assistente di proof Lean.

L’Intelligenza Artificiale e il Machine Learning sono i campi di tendenza dell’attuale periodo. Con i progressi immensi che si stanno compiendo nell’AI, nuove innovazioni stanno trasformando il modo in cui gli esseri umani interagiscono con le macchine. Il ragionamento nell’intelligenza umana è una parte significativa dell’Intelligenza Artificiale. Sono stati studiati diversi approcci alla dimostrazione dei teoremi, come la dimostrazione automatica dei teoremi (ATP), che è il processo di produrre automaticamente prove per teoremi espressi in logica formale. L’ATP è una sfida a causa dello spazio di ricerca massivo, quindi è emersa la dimostrazione interattiva dei teoremi (ITP) come paradigma alternativo in cui esperti umani interagiscono con strumenti software chiamati assistenti di prova per costruire prove.

I modelli di linguaggio estesi (LLM), che hanno dimostrato straordinarie capacità di generazione di codice, affrontano anche difficoltà nella dimostrazione dei teoremi a causa di difetti nella factualità e nell’allucinazione. Per superare queste limitazioni, un team di ricercatori provenienti da Caltech, NVIDIA, MIT, UC Santa Barbara e UT Austin ha introdotto LeanDojo, che è un toolkit open source per la dimostrazione dei teoremi basata su LLM. LeanDojo è stato costruito attorno all’assistente di prova Lean, che è popolare tra i matematici. Offre risorse per lavorare con Lean ed estrarre dati.

Nell’estrazione dei dati, i dati di addestramento vengono raccolti da alberi di prove e stati intermedi delle prove che non sono immediatamente evidenti nel codice Lean originale. LeanDojo è stato reso in grado di consentire ai modelli di comunicare con Lean in modo programmabile. Ciò consente loro di vedere gli stati delle prove, eseguire azioni o tattiche di prova e ottenere feedback da Lean. Il playground di Lean open-source è composto da numerosi elementi, tra cui toolkit, dati, modelli e benchmark, per consentire l’interazione programmata con l’ambiente delle prove ed estrarre dati da Lean.

• Baidu Ernie 3.5 si presenta come il campione dell’IA nel linguaggio cinese ma è davvero migliore di ChatGPT?
• Approcci di Apprendimento In-Context in Modelli di Lingua di Grandi Dimensioni
• Contextual AI presenta LENS un framework di intelligenza artificiale per modelli di linguaggio potenziati dalla visione che supera Flamingo del 9% (56->65%) su VQAv2.

LeanDojo fornisce annotazioni dettagliate delle premesse nelle prove, che sono preziose per la selezione delle premesse, un collo di bottiglia critico nella dimostrazione dei teoremi. Utilizzando le capacità di estrazione dati di LeanDojo, i ricercatori hanno anche sviluppato ReProver, il primo dimostratore basato su LLM potenziato con il recupero per la selezione delle premesse da una vasta libreria matematica. A differenza dei metodi precedenti che dipendevano da set di dati privati che richiedevano risorse computazionali consistenti, ReProver è stato progettato per essere più accessibile ed economico. Richiede meno potenza di calcolo e può essere addestrato con una sola GPU alla settimana.

La capacità di analisi dei programmi di LeanDojo è stata utilizzata dal meccanismo di recupero di ReProver per trovare premesse accessibili e produrre esempi concreti di ciò che potrebbe andare storto. Di conseguenza, il dimostratore si comporta meglio e la procedura di recupero è più efficace. Per valutazione e ulteriori ricerche, il team ha sviluppato un nuovo set di dati di benchmark composto da 96.962 teoremi e prove estratti dalla libreria matematica di Lean. Questo set di dati di benchmark presenta una divisione dei dati impegnativa che richiede al dimostratore di generalizzare a teoremi che si basano su premesse nuove che non sono state utilizzate durante l’addestramento. I risultati sperimentali hanno dimostrato che ReProver si comporta bene rispetto ai baselines senza recupero e a GPT-4 quando si utilizza questo set di dati di benchmark per l’addestramento e la valutazione.

In conclusione, questa soluzione open-source per la dimostrazione dei teoremi basata su LLM sembra promettente per il futuro. Supera le barriere del codice privato, dei dati e dei requisiti di calcolo elevati fornendo toolkit, dati, modelli e benchmark accessibili.