Agentified Assessment of Logical Reasoning Agents

Dit artikel introduceert een reproduceerbaar en auditabel framework voor het beoordelen van logische redeneeragenten, waarbij een 'assessor-agent' wordt gebruikt om taken te beheren en fouten te registreren, en demonstreert dat een auto-formalisatie-agent voor eerste-orde logica op een gerepareerde FOLIO-dataset een significant hogere nauwkeurigheid bereikt dan een chain-of-thought-baseline.

De kern

Stel je voor dat je een groep slimme robots wilt testen op hun logisch denkvermogen. Vroeger was dat testen een rommelige zaak: als een robot vastliep in de software, een foutje maakte in de code of gewoon te lang deed, werd dat vaak verward met een "domme" fout in het denken. Alsof je een student een wiskundetoets geeft, maar als hij zijn pen laat vallen, zeggen we dat hij de wiskunde niet begrijpt.

Dit paper introduceert een nieuwe, slimmere manier om die robots te testen, genaamd "Agentified Assessment" (ofwel: "Robots die andere robots testen"). Hier is de uitleg in simpele taal, met een paar leuke vergelijkingen:

1. De Nieuwe Testmethode: De Onpartijdige Examinator

In de oude wereld was de test een statisch computerprogramma dat alles vastlegde. In deze nieuwe wereld hebben ze een Assessor-agent (een testrobot) bedacht.

• De Vergelijking: Denk aan een oude schooltest waar de leraar (de computer) alles zelf regelt. Als de leraar een fout maakt in het nakijken, is je cijfer verkeerd.
• De Nieuwe Aanpak: Nu hebben ze een onafhankelijke examinator (de Assessor-agent). Deze robot is de "scheidsrechter". Hij geeft de opdracht, kijkt of de andere robot (de "proefpersoon") binnen de tijd werkt, en controleert of het antwoord correct is.
• Het Voordeel: Als de proefpersoon robot vastloopt of een foutje maakt in zijn antwoord, schrijft de examinator niet direct "Fout" op. Hij noteert precies wat er misging: "Tijd verlopen", "Programma crashte" of "Antwoord onleesbaar". Zo weten we zeker dat we de robot testen op zijn denkvermogen, niet op zijn technische pech.

2. De Opdracht: Logisch Redeneren (Het "Duits" van de Robots)

De robots kregen een specifieke opdracht: Eerste-orde logica.

• De Vergelijking: Stel je voor dat je een verhaal leest in gewone taal (bijv. "Alle vogels kunnen vliegen. Pinguïns zijn vogels. Dus pinguïns kunnen vliegen"). Je moet dan bepalen of de conclusie waar is, onwaar is, of dat je het niet weet.
• Het Probleem: De originele dataset (FOLIO) waar deze tests op gebaseerd waren, zat vol met fouten. Het was alsof de testvragen zelf slecht waren opgesteld.
• De Oplossing: De auteurs hebben een schoonmaakteam ingezet. Ze gebruikten een supersterke wiskundige machine (een "theorema-bewijzer") om elke vraag te controleren. Als de vraag niet klopte, werd hij gerepareerd.
  • Voorbeeld: Als er in de vraag stond "Alle A's zijn B's", maar de wiskundige machine zei "Nee, dat klopt niet", dan werd de vraag aangepast. Zo ontstond een "gezuiverde" testset, waar je echt op kunt vertrouwen.

3. De Twee Robots in de Arena

Op deze schone testset werden twee soorten robots tegen elkaar getest:

• Robot A: De "Ketting-Redenerer" (Chain-of-Thought)

  • Hoe werkt hij? Hij denkt hardop na, stap voor stap, net als een mens die een probleem oplost. Hij probeert het antwoord te "voelen" door te redeneren.
  • Resultaat: Hij deed het redelijk goed (73,9% correct), maar hij maakte veel fouten bij moeilijke, tegenstrijdige situaties.

• Robot B: De "Vertaler naar Wiskunde" (Auto-formalization)

  • Hoe werkt hij? Deze robot vertaalt de gewone taal direct naar een strikt wiskundig programma (Z3Py-code). In plaats van te "gokken" of te redeneren als een mens, laat hij een wiskundige computer (een solver) het antwoord berekenen.
  • De Magie: Als de code een fout geeft (bijv. een haakje mist), probeert de robot zichzelf te repareren en het opnieuw te doen.
  • Resultaat: Deze robot won met overmacht (86,7% correct). Vooral bij de moeilijke "Onwaar" (contradictie) gevallen was hij veel beter.

4. Waarom is dit belangrijk?

De kernboodschap van dit paper is tweeledig:

1. Betrouwbaarheid: Door de "Assessor-agent" te gebruiken, weten we precies waarom een robot faalt. Is hij dom, of is zijn software kapot? Dit maakt testen eerlijker en reproduceerbaarder.
2. Kracht van Wiskunde: Het bewijst dat robots die gewone taal omzetten in strikte wiskundige code, veel beter zijn in logisch denken dan robots die alleen maar proberen te "redeneren" zoals mensen.

Samenvattend:
Stel je voor dat je een nieuwe auto wilt testen. De oude manier was: "Laat de auto rijden en kijk of hij aankomt." Als hij stukviel, was het een slechte auto.
De nieuwe manier (zoals in dit paper) is: Je hebt een testpiloot die de auto aanstuurt, een mechanicus die de motor controleert, en een rekenmachine die de route berekent. Als de auto niet aankomt, weten we precies of het aan de motor lag, aan de route, of aan de bestuurder. En in dit geval bleek dat de auto die de route met een rekenmachine uitrekende, veel sneller en veiliger aankwam dan de auto die probeerde de weg te "voelen".

Technische samenvatting

Titel: Agentified Assessment of Logical Reasoning Agents

Conferentie: ICLR 2026 Agents in the Wild (AIWILD) Workshop
Auteurs: Zhiyu Ni, Yifeng Xiao, Zheng Liang (UC Berkeley)

---

1. Het Probleem

Het evalueren en benchmarken van redeneeragenten (AI-agenten) is momenteel problematisch vanwege de complexiteit van fouten die op verschillende lagen kunnen optreden:

• Vermenging van fouten: Traditionele evaluatieharnassen verwarren operationele fouten (zoals time-outs, runtime-fouten of het niet kunnen parsen van output) met daadwerkelijke redeneerfouten. Dit leidt tot een onnauwkeurige weergave van de prestaties.
• Gebrek aan reproduceerbaarheid: De integratie van een nieuwe agent in een bestaande benchmark vereist vaak maatwerk per benchmark, wat de schaalbaarheid beperkt.
• Verborgen failure modes: Traditionele setups presenteren vaak slechts één accuraatheidscijfer, waardoor specifieke faalpatronen (bijv. syntaxfouten in gegenereerde code) onzichtbaar blijven.

2. Methodologie

De auteurs stellen een nieuw raamwerk voor dat twee hoofdcomponenten combineert: een gezuiverde dataset en een agent-gebaseerde evaluatie.

A. Data Cleaning en Validatie (FOLIO Dataset)

De studie gebruikt de FOLIO-dataset (First-Order Logic reasoning), maar erkent dat de originele dataset fouten bevat in de vertaling van natuurlijk taal naar formele logica.

• Validatie-pijplijn: Een systematische pijplijn wordt gebruikt die symbolische verificatie toepast met de Vampire-theorema-prover.
• Stappen:
  1. Consistentiecheck: Controleer of de premissen consistent zijn.
  2. Implicatiecheck: Gebruik Satisfiability Modulo Theories (SMT) om te bepalen of een conclusie logisch volgt (TRUE), in tegenspraak is (FALSE), of onbepaald is (UNCERTAIN).
  3. Reparatie: Als de verificatieresultaten afwijken van de originele labels, worden twee LLM-agenten ingezet: een critique-agent die vertaalfouten identificeert en een refiner-agent die deze corrigeert.
  4. Resultaat: Een "gezuiverde" split van FOLIO met geverifieerde labels, waarbij onoplosbare gevallen handmatig worden beoordeeld.

B. Agentified Assessment Framework (AAA)

In plaats van een statisch script, wordt de evaluatie zelf uitgevoerd door een Assessor-agent.

• A2A-interface: De "agent onder test" communiceert via een gestandaardiseerde Agent-to-Agent (A2A) interface met de assessor.
• Rol van de Assessor:
  • Deelt taken uit.
  • Handhaaft uitvoeringsbudgetten (time-outs, retry-limieten).
  • Parseert output en valideert het resultaat.
  • Gestructureerde foutregistratie: In plaats van een evaluatie te verwerpen bij een runtime-fout, registreert de assessor het type fout (bijv. TIMEOUT, RUNTIMEERROR, PARSEERROR).
• Voordeel: Dit ontkoppelt de evaluatielogica van de agent-implementatie. Een agent hoeft maar één keer een A2A-interface te implementeren om deel te nemen aan vele verschillende benchmarks (O(1) integratiekost in plaats van O(n)).

C. Geteste Agenten

Twee agenten worden vergeleken onder dezelfde assessor:

1. Chain-of-Thought (CoT) Baseline: De agent redeneert stap-voor-stap in natuurlijke taal en geeft een label als laatste zin.
2. Auto-Formalization Agent: Deze agent vertaalt natuurlijke taal-premissen naar uitvoerbare Z3Py-code (Python met de Z3 SMT-solver).
   • Proces: Generatie van code -> Executie in een sandbox (60s timeout) -> Logische validatie via de solver.
   • Self-Repair: Bij syntaxfouten of mislukte uitvoering probeert de agent de code automatisch te repareren (max. 3 pogingen).

3. Belangrijkste Resultaten

De experimenten zijn uitgevoerd op de gezuiverde validatieset van FOLIO (203 voorbeelden).

• Totale Accuraatheid:
  • Auto-Formalization Agent: 86,70% (176/203 correct).
  • Chain-of-Thought Baseline: 73,89% (150/203 correct).
• Gedetailleerde Prestaties per Categorie:
  • FALSE (Tegenstrijdigheid): De grootste verbetering, van 44,26% (CoT) naar 77,05% (Auto-Formalization). Dit toont aan dat solvers beter zijn in het detecteren van logische tegenstrijdigheden dan pure taalredenering.
  • TRUE (Logisch gevolg): Beide methoden presteren hoog en vergelijkbaar (89-90%).
  • UNCERTAIN (Onbepaald): De solver-gebaseerde agent presteert significant beter (91,30% vs 84,06%), wat aantoont dat formele verificatie beter omgaat met logische onbepaaldheid.

4. Bijdragen en Significantie

• Nieuwe Evaluatiestandaard: Het paper introduceert "Agentified Assessment" als een reproduceerbaar, auditabel en robuust raamwerk voor het testen van agenten, waarbij operationele fouten expliciet worden gelogd in plaats van verdoezeld.
• Betrouwbare Benchmark: Door het toepassen van een geautomatiseerde verificatie- en reparatiepijplijn op FOLIO, bieden de auteurs een betrouwbaardere dataset voor logisch redeneren dan de originele versie.
• Superioriteit van Formele Methoden: De resultaten tonen aan dat het vertalen van natuurlijke taal naar formele logica (Z3Py) en het gebruik van SMT-solvers superieur is aan pure Chain-of-Thought prompting voor complexe logische taken, vooral bij het detecteren van tegenstrijdigheden.
• Schaalbaarheid: Het A2A-protocol maakt "plug-and-play" evaluatie mogelijk, wat de integratie van nieuwe agenten in bestaande benchmarks aanzienlijk vereenvoudigt.

Conclusie:
Het werk demonstreert dat het combineren van data-cleaning met formele verificatie, gekoppeld aan een agent-gebaseerde evaluatiestructuur, leidt tot robuustere en nauwkeurigere benchmarks voor logisch redenerende AI-systemen. De auto-formalizing agent overtreft de traditionele CoT-benadering aanzienlijk, wat wijst op de noodzaak van hybride systemen die natuurlijke taal combineren met formele tooling.