DreamProver: un framework AI che evolve librerie di lemmi trasferibili per la dimostrazione di teoremi

DreamProver è stato presentato dai ricercatori come un framework agentico che impiega un paradigma di induzione di programmi wake-sleep per identificare lemmi riutilizzabili per la dimostrazione formale di teoremi. I metodi tradizionali dipendono da librerie di lemmi statiche, che limitano la flessibilità, o generano lemmi intermedi altamente specifici per particolari teoremi, privi di applicabilità più ampia. DreamProver colma questa lacuna con il suo approccio iterativo in due fasi. Durante la fase di veglia, cerca di dimostrare teoremi da un set di addestramento utilizzando la libreria di lemmi esistente, suggerendo al contempo nuovi lemmi candidati. Nella fase di sonno, astrae, raffina e consolida questi candidati per migliorare e snellire la libreria. Questo processo alternato consente a DreamProver di sviluppare una collezione compatta di lemmi trasferibili di alto livello, migliorando significativamente le prestazioni nei compiti di dimostrazione formale di teoremi, come mostrato dai risultati sperimentali.