LeanPRM: supervisione del processo ancorata a Lean per la verifica delle dimostrazioni in linguaggio naturale

Abstract degli autori

I sistemi di IA scrivono ormai dimostrazioni matematiche lunghe e difficili, e verificarne la validità passaggio per passaggio sta diventando un collo di bottiglia. Un verificatore addestrato potrebbe controllarle a basso costo, ma per addestrarlo occorre un’etichetta di correttezza per ogni passaggio, difficile da ottenere per dimostrazioni aperte. I metodi esistenti ricorrono ad annotatori umani, con costi elevati, oppure ricavano le etichette dalle risposte finali, che le dimostrazioni non hanno; formalizzare ogni dimostrazione in Lean, invece, richiede il lavoro di esperti. Presentiamo LeanPRM, un framework che usa l’assistente alla dimostrazione Lean per creare etichette a livello di singolo passaggio per dimostrazioni in linguaggio naturale. Un modello scrive una dimostrazione in linguaggio naturale insieme alla corrispondente dimostrazione formale, senza ricevere riscontri da Lean. Lean etichetta quindi ogni passaggio, mentre un secondo modello scarta i fallimenti dovuti soltanto alla sintassi formale, affinché le etichette negative segnalino errori matematici. LeanPRM contiene 10.634 dimostrazioni con 152K passaggi etichettati e nessuna annotazione umana. Un verificatore Qwen3-4B addestrato su LeanPRM porta l’accuratezza nella corrispondenza esatta delle etichette dei passaggi dal 48,2 al 74,7 su un insieme di 200 dimostrazioni tenute da parte per la valutazione (LeanPRM-Bench), contro il 60,3 ottenuto addestrando lo stesso modello di base su PRM800K. Seleziona inoltre dimostrazioni migliori nella scelta della migliore tra N per problemi di livello IMO e supera il verificatore addestrato su PRM800K in tre dei quattro benchmark esterni di verifica. Su LeanPRM-Bench, Hard2Verify e IMO-GradingBench, l’addestramento su LeanPRM migliora i verificatori di tutte le dimensioni, da 0,6B a 8B parametri. Poiché le etichette non richiedono annotazione umana, LeanPRM può crescere con la disponibilità di enunciati formali, offrendo una via per fornire riscontri sui singoli passaggi delle dimostrazioni generate dall’IA che gli esseri umani faticano a verificare.