TLA$^{+}$-Bench: Benchmark basato sull'esecuzione per la generazione di specifiche TLA$^{+}$ da linguaggio naturale

Un nuovo dataset e benchmark chiamato TLA$^{+}$-Bench è stato sviluppato da ricercatori per valutare la capacità dei grandi modelli linguistici di produrre specifiche formali TLA$^{+}$ a partire da descrizioni in linguaggio naturale. A differenza dei dataset precedenti, che valutavano in base alla somiglianza con un riferimento o al successo del parsing, TLA$^{+}$-Bench valuta tramite esecuzione: ogni specifica gold è abbinata a una configurazione che il model checker TLA$^{+}$ utilizza per esplorare l'intero spazio degli stati raggiungibili, verificando in modo conclusivo se la specifica soddisfa le proprietà specificate. Il dataset comprende 403 specifiche gold verificate con model checking e 897 specifiche silver solo parse da 13 repository pubblici, includendo precedenti dataset di generazione TLA$^{+}$. Inoltre, presenta quattro descrizioni scritte da modelli in due stili da due fonti, complete di etichette di difficoltà e categoria. Un'osservazione significativa è che un oracolo esatto produce una gamma di metriche di correttezza basate sul metodo di valutazione utilizzato.