Il team di LeanDojo in collaborazione con il California Institute of Technology ha presentato Lean Co-pilot, una nuova piattaforma collaborativa progettata per consentire un’interazione efficiente tra l’intelligenza artificiale (LLM) e gli esseri umani, al fine di creare dimostrazioni matematiche formali al 100% precise.
Questo innovativo sistema utilizza LLM per suggerire tattiche di dimostrazione all’interno del dimostratore del teorema Lean, offrendo un ambiente in cui l’intervento umano può avvenire in modo continuo e mirato.
L’automazione nella dimostrazione di teoremi è stata spesso ostacolata dalla limitata affidabilità degli attuali sistemi di intelligenza artificiale nei compiti matematici e di ragionamento, che possono facilmente commettere errori o generare risultati errati. Le dimostrazioni matematiche tradizionali richiedevano principalmente un lavoro manuale accurato e una verifica scrupolosa.
Lean, un potente dimostratore di teoremi, è noto per la sua capacità di effettuare verifiche formali, ma presentava sfide quando si trattava di scrittura in Lean da parte degli esseri umani. Lean Co-pilot affronta questa sfida sfruttando LLM per automatizzare la suggerimento di tattiche di prova in Lean, accelerando notevolmente il processo di sintesi della dimostrazione. Il sistema consente interventi umani solo quando necessario, creando una collaborazione equilibrata tra l’automazione e l’ingegno umano.
Le caratteristiche principali di Lean Co-pilot includono suggerimenti basati su LLM per le varie fasi della dimostrazione, la ricerca di dimostrazioni e la selezione di lemmi utili da una vasta libreria matematica. Lo strumento si integra senza problemi nel flusso di lavoro di Visual Studio Code di Lean, offrendo un’esperienza intuitiva agli utenti.
Gli utenti hanno la possibilità di configurare Lean Co-pilot come pacchetto Lean, utilizzando i modelli integrati di LeanDojo o incorporando modelli personalizzati, che possono essere eseguiti sia in locale che in cloud.
LeanDojo, la piattaforma che supporta Lean Co-pilot, promuove l’accessibilità offrendo modelli e strumenti open source sotto licenza MIT. Lo strumento è compatibile con diverse piattaforme, inclusi Linux, macOS e Windows WSL, con opzionale supporto per GPU abilitate CUDA.
I requisiti per l’utilizzo di Lean Co-pilot includono Git LFS, CUDA e cuDNN (opzionali ma consigliati per il supporto GPU), e CMake >= 3.7 insieme a un compilatore compatibile con C++17 per la compilazione di Lean Co-pilot.
L’introduzione di Lean Co-pilot ha l’obiettivo di rendere LLM più accessibili agli utenti di Lean, contribuendo a creare un ciclo di feedback positivo in cui l’automazione delle prove contribuisce a migliorare la qualità dei dati, portando infine a miglioramenti nei sistemi di intelligenza artificiale per le attività matematiche.