StochBench: un benchmark specifico per i processi stocastici in Lean

Abstract degli autori

I principali benchmark per la dimostrazione formale di teoremi con modelli linguistici di grandi dimensioni sono piccole raccolte di problemi tratti da gare di matematica, come l’IMO e la Putnam, che rappresentano poco le applicazioni specifiche dei singoli ambiti disciplinari. Presentiamo StochBench, un benchmark per Lean 4 composto da 450 problemi sui processi stocastici di livello post-laurea e con diversi gradi di astrazione, ciascuno abbinato alla propria fonte in linguaggio naturale. Dedicato a un ambito poco rappresentato in Mathlib, comprende catene di Markov finite e numerabili, processi di rinnovo, passeggiate aleatorie, martingale, tempi di arresto, code, moto browniano, calcolo stocastico, convergenza debole, processi di Poisson e processi di Markov a tempo continuo. Il nostro agente basato su Opus 4.8 raggiunge un tasso di dimostrazione del 34,9% (157/450), con un limite di 15 minuti per problema. StochBench rappresenta meglio la matematica applicata nei singoli ambiti disciplinari, pur restando impegnativo per i dimostratori avanzati.