Agentified Assessment of Logical Reasoning Agents

Each language version is independently generated for its own context, not a direct translation.

Immagina di dover organizzare un grande torneo di scacchi per testare quanto sono intelligenti diversi giocatori (gli "agenti"). Fino a poco tempo fa, il modo di giudicare questi giocatori era un po' caotico: se un giocatore sbagliava a muovere il pezzo o se il cronometro si rompeva, il giudice spesso confondeva l'errore di movimento con un errore di strategia, dando un voto unico e poco chiaro.

Questo paper, presentato al workshop AIWILD di ICLR 2026, propone un modo rivoluzionario per fare questi test.

1. Il Nuovo Arbitro: "L'Agente Giudice"

Invece di avere un semplice foglio di regole statico, gli autori creano un Arbitro Intelligente (chiamato Assessor Agent).

Come funziona prima: Il giudice era come un umano che doveva correggere i compiti a mano, mescolando errori di calcolo con errori di logica. Se il computer si bloccava, il voto era sbagliato.
Come funziona ora: L'Arbitro è un software specializzato che:
1. Assegna il compito.
2. Controlla il tempo (se il giocatore impiega troppo, lo ferma gentilmente).
3. Legge la risposta e la traduce in un formato chiaro.
4. Se il giocatore sbaglia a scrivere la risposta (es. "Ho pensato che..."), l'Arbitro non si arrabbia, ma registra esattamente dove è fallito: "Errore di tempo", "Errore di calcolo" o "Non ho capito la domanda".

È come avere un arbitro che non solo fischia il fallo, ma ti dice: "Hai sbagliato perché hai calciato la palla fuori dal campo, non perché non sapevi dove tirare". Questo rende il test trasparente e onesto.

2. Il Campo di Gioco: "Il Puzzle della Logica"

Per testare questi agenti, hanno usato un gioco chiamato FOLIO. Immaginalo come un enorme libro di indovinelli logici tratti da Wikipedia.

La sfida: Ti danno una storia (premesse) e una conclusione. Tu devi dire se la storia è Vera (logica), Falsa (contraddittoria) o Incerta (non si può sapere).
Il problema: Il libro originale aveva alcune pagine sbagliate o traduzioni confuse.
La soluzione: Gli autori hanno assunto un "team di correttori" (un mix di software e umani) per ripulire il libro. Hanno usato un "super-calcolatore" (un prover matematico) per controllare ogni indovinello. Se il libro diceva "Vero" ma la matematica diceva "Falso", hanno corretto la pagina. Ora hanno un campo di gioco perfetto e pulito.

3. I Due Giocatori: "Il Ragionatore vs. L'Architetto"

Hanno messo alla prova due tipi di giocatori su questo campo pulito:

Giocatore A (Il Ragionatore a Catena): È come uno studente che legge la domanda e prova a ragionare passo dopo passo, scrivendo tutto su un foglio.
- Risultato: Va bene, ma a volte si confonde o sbaglia i calcoli. Ha ottenuto un 74% di risposte corrette.
Giocatore B (L'Architetto della Logica): Questo è il vero protagonista. Non si limita a "pensare" a parole. Quando riceve il problema, lo traduce immediatamente in un linguaggio di programmazione (un codice che un computer può eseguire).
- Immagina che invece di dire "Se piove, il terreno è bagnato", l'Architetto scriva un piccolo programma che fa il calcolo da solo.
- Se il programma si blocca per un errore di sintassi, l'Architetto ha un "meccanismo di auto-riparazione": legge l'errore, si corregge da solo e riprova fino a 3 volte.
- Risultato: È molto più preciso. Ha ottenuto un 87% di risposte corrette.

4. Perché è importante?

Il punto chiave di questo studio non è solo che l'Architetto ha vinto, ma come è stato giudicato.
Grazie all'Arbitro Intelligente, sappiamo esattamente perché l'Architetto ha vinto:

Ha sbagliato meno calcoli grazie all'uso di un "motore matematico" (il solver).
È stato molto bravo a gestire i casi in cui la risposta non è chiara (l'incertezza).
Il sistema ha registrato ogni singolo errore tecnico, rendendo il risultato impossibile da falsificare.

In sintesi

Questo paper ci dice che per testare l'intelligenza artificiale non basta più chiedergli "Qual è la risposta?". Dobbiamo costruire un sistema dove:

Il campo di gioco (i dati) sia pulito e corretto.
L'arbitro sia un software che registra ogni dettaglio, non solo il voto finale.
Gli agenti possano usare strumenti (come calcolatrici o codici) per risolvere i problemi, non solo "indovinare" le parole.

È come passare dal far scrivere un tema a mano a un bambino, al dargli una calcolatrice e un correttore automatico, e poi far valutare il risultato da un computer che sa esattamente dove ha fatto errore. Il risultato è un'intelligenza artificiale più affidabile e comprensibile.

Each language version is independently generated for its own context, not a direct translation.

1. Il Problema

La valutazione e il benchmarking degli agenti di ragionamento logico presentano sfide significative dovute alla natura multistrato dei fallimenti, che possono verificarsi sia nel ragionamento del modello che nell'esecuzione degli strumenti.

Limiti delle valutazioni statiche: I sistemi di valutazione tradizionali tendono a confondere i fallimenti operativi (es. timeout, errori di runtime, fallimenti nel parsing dell'output) con errori di ragionamento logico, nascondendo spesso queste modalità di fallimento dietro un singolo numero di accuratezza.
Accoppiamento rigido: Le configurazioni tradizionali legano strettamente la logica del benchmark all'implementazione dell'agente, rendendo l'integrazione complessa e costosa (costo di integrazione $O(n)$ rispetto al numero di benchmark).
Qualità dei dati: Dataset esistenti come FOLIO possono contenere errori di etichettatura e disallineamenti tra le annotazioni in linguaggio naturale e quelle formali, compromettendo l'affidabilità del benchmark.

2. Metodologia

Gli autori propongono un approccio innovativo basato su due pilastri principali: un framework di valutazione "agentificato" e un processo di pulizia dei dati rigoroso.

A. Valutazione Agentificata (Agentified Assessment - AAA)

Invece di utilizzare script statici, la valutazione viene formalizzata come un'interazione tra due agenti:

Agente sotto test (Agent Under Test): Esegue il compito di ragionamento e deve esporre solo un'interfaccia standardizzata "Agent-to-Agent" (A2A).
Agente Valutatore (Assessor Agent): Controlla l'esecuzione del compito, impone budget (es. timeout), analizza l'output, assegna punteggi e registra fallimenti strutturati.

Vantaggio: Questo approccio disaccoppia la logica di valutazione dall'agente, permettendo un'integrazione "plug-and-play" con costo $O(1)$ per agente, indipendentemente dal numero di benchmark.
Gestione degli errori: L'agente valutatore non scarta i fallimenti, ma li categorizza in modo strutturato (es. TIMEOUT, RUNTIMEERROR, PARSEERROR) per un'analisi granulare.

B. Pipeline di Pulizia e Verifica dei Dati (FOLIO)

Per creare un benchmark affidabile, gli autori hanno implementato una pipeline di pulizia sul dataset FOLIO (First-Order Logic Inference):

Verifica Simbolica: Utilizzo del teorema di Vampire per verificare la consistenza delle premesse e le relazioni di implicazione logica.
Identificazione e Riparazione: Quando i risultati di verifica confliggono con le etichette originali, vengono utilizzati due agenti LLM:
- Un agente critico diagnostica errori di traduzione (es. parentesi sbilanciate, errori lessicali).
- Un agente rifinitore esegue correzioni mirate.
Iterazione: Il processo di riparazione e riesecuzione continua fino alla risoluzione o fino a un limite di iterazioni, dopodiché i casi problematici vengono revisionati manualmente.
Risultato: È stato rilasciato un split di FOLIO "ripulito e riparato" (disponibile su Hugging Face) con un tasso ridotto di errori di etichettatura.

C. Agenti Sperimentali

Sul benchmark pulito sono stati testati due agenti:

Baseline Chain-of-Thought (CoT): Utilizza il prompting per ragionare passo-passo e outputta un'etichetta finale.
Agente di Auto-Formalizzazione:
- Fase 1 (Generazione Codice): Traduce premesse e conclusioni in linguaggio naturale in codice eseguibile Z3Py (Python per il solver SMT Z3).
- Fase 2 (Esecuzione e Verifica): Esegue il codice in un ambiente sandbox (timeout 60s).
- Loop di Auto-Riparazione: Se l'esecuzione fallisce per errori di sintassi, l'agente analizza il messaggio di errore e tenta di riparare il codice fino a 3 volte.
- Logica: Determina la validità logica basandosi sulla soddisfacibilità (Satisfiability Modulo Theories): se $\bigwedge \phi_i \land \neg \phi$ è insoddisfacibile, la conclusione è TRUE; se $\bigwedge \phi_i \land \phi$ è insoddisfacibile, è FALSE; altrimenti UNCERTAIN.

3. Risultati Chiave

Gli esperimenti sono stati condotti sul set di validazione pulito di FOLIO (203 esempi), utilizzando il modello LLM Gemini 2.5 Flash come backbone per entrambi gli agenti.

Accuratezza Complessiva:
- Chain-of-Thought (Baseline): 73.89% (150/203).
- Agente di Auto-Formalizzazione: 86.70% (176/203).
Analisi per Categoria:
- FALSE (Contraddizioni): Il miglioramento è drastico, passando dal 44.26% al 77.05%. Questo dimostra la superiorità dei solver nel rilevare contraddizioni logiche rispetto al ragionamento puramente testuale.
- TRUE (Entailment): Prestazioni simili e alte per entrambi (89.04% vs 90.41%).
- UNCERTAIN (Indeterminato): L'agente di auto-formalizzazione supera la baseline (91.30% vs 84.06%), evidenziando la capacità dei solver di gestire l'indeterminatezza logica.

4. Contributi Principali

Framework AAA: Introduzione di un paradigma di valutazione in cui la logica di assessment è un agente autonomo, riducendo i costi di integrazione e migliorando la tracciabilità dei fallimenti.
Dataset FOLIO Ripulito: Creazione e rilascio di una versione di FOLIO verificata e riparata, che elimina errori sistematici di etichettatura e disallineamenti NL-FOL.
Validazione dell'Auto-Formalizzazione: Dimostrazione empirica che tradurre problemi logici in codice eseguibile per solver SMT (Z3) supera significativamente i metodi basati su Chain-of-Thought, specialmente nei casi di contraddizione e indeterminazione.
Infrastruttura Riproducibile: Sviluppo di una leaderboard logica che registra artefatti di valutazione dettagliati (accuratezza, latenza, tipi di errore) per confronti riproducibili.

5. Significato e Implicazioni

Questo lavoro segna un passo importante verso la valutazione robusta e scalabile degli agenti AI.

Affidabilità: Spostando la logica di valutazione in un agente separato e utilizzando solver formali per la verifica, si ottengono metriche più affidabili e meno soggette a rumore operativo.
Scalabilità: Il modello AAA permette di testare nuovi agenti su molteplici benchmark con uno sforzo di integrazione minimo, facilitando l'evoluzione dell'ecosistema degli agenti.
Direzione Futura: I risultati suggeriscono che l'integrazione di strumenti formali (come i solver SMT) è cruciale per il ragionamento logico avanzato, superando i limiti dei modelli linguistici puri. Il lavoro apre la strada all'applicazione di questo framework di valutazione ad ambienti più complessi con uso di strumenti multipli.