Re$^2$Math: Nuovo benchmark per il recupero di teoremi nelle dimostrazioni matematiche

I ricercatori hanno introdotto Re$^2$Math, un benchmark progettato per valutare la capacità dei grandi modelli linguistici di recuperare teoremi rilevanti dalla letteratura matematica durante la costruzione di dimostrazioni. Ogni istanza di test deriva da una citazione all'interno di una dimostrazione di un teorema principale, fornendo un contesto gerarchico e un suggerimento facoltativo. Il compito è basato sulla fonte ma indipendente dalla citazione, accettando qualsiasi teorema ammissibile sufficiente per la transizione dimostrativa. Il benchmark utilizza un artefatto di recupero congelato per garantire la riproducibilità. Questo lavoro affronta la necessità di assistenti AI in grado di determinare se esiste un lemma necessario, identificare fonti accademiche adatte e verificare l'allineamento delle ipotesi con il contesto dimostrativo corrente. L'articolo è disponibile su arXiv.