Oltre la compilazione: valutare la fedeltà della formalizzazione di enunciati dal linguaggio naturale in Lean

Abstract degli autori

Lean verifica che una dichiarazione generata sia correttamente tipizzata, ma non può controllare se esprima ciò che l’utente intendeva. Misuriamo quanto la compilazione sovrastimi la fedeltà nell’autoformalizzazione di enunciati in assenza di versioni canoniche in Lean. Il nostro criterio richiede che il codice venga compilato da Lean e che due valutatori basati su LLM di famiglie di modelli diverse siano concordi. In una verifica indipendente su un campione casuale, il criterio concorda con la maggioranza dei valutatori umani nel 91,5% dei casi: raramente accetta un risultato infedele, ma ne respinge alcuni fedeli. Su 227 enunciati di livello universitario, per otto sistemi la differenza tra la percentuale di risultati compilati e quella di risultati accettati varia da 1,3 a 29,5 punti percentuali: il nostro agente dotato di strumenti compila l’87,2% degli enunciati, ma solo il 57,7% viene accettato. La revisione umana di tutti i risultati dell’agente respinti conferma che 23,8 dei 29,5 punti di differenza sono dovuti a veri errori di traduzione. Per le differenze dei sette sistemi one-shot, una revisione in due fasi condotta da Claude Opus 5.5 con Lean e GPT-6.1 Sol, validata rispetto a queste valutazioni umane, rileva che, per sei di essi, il 78-100% è dovuto a veri errori di traduzione. Quando GPT-5.2, uno dei due valutatori, giudica le traduzioni di due modelli pubblicati dopo di esso, GPT-6 Astra e Claude Opus 5.5, accetta l’83% degli enunciati per ciascuno, contro il 21% di GPT-5.2 in modalità one-shot. Per questi due modelli, la stessa revisione classifica come errori di traduzione solo 4 dei loro 54 risultati respinti (7%): la maggior parte della differenza misurata è quindi dovuta a errori dei valutatori, non a errori di traduzione. Ciò è coerente con il fatto che questi sistemi commettono meno errori, mentre il valutatore no: meno errori commette un sistema, minore è la quota dei suoi risultati respinti dovuta a errori di traduzione. Infine, uno studio di ablazione dell’agente su 2^3 configurazioni degli strumenti mostra che il feedback di Lean determina la maggior parte dell’aumento dei risultati compilati e che quasi metà di tale aumento non soddisfa il criterio semantico. Codice e dati sono disponibili all’indirizzo https://github.com/grenadeComing/beyond-compilation.