Technische Samenvatting: MANTRA – Het Synthetiseren van SMT-gevalideerde Compliance-benchmarks

Probleemstelling

Tool-gebruikende Large Language Model (LLM)-agenten worden steeds vaker ingezet in kritieke domeinen zoals bedrijfsoperaties, gezondheidszorg en reisboekingen, waar hun gedrag moet voldoen aan strikte procedurale handleidingen. Een fundamentele uitdaging bij het evalueren van deze agenten is het "mismatch" tussen de invoer en de uitvoer: procedurale regels worden typisch geschreven als ongestructureerde natuurlijke taal voor menselijke interpretatie, terwijl het gedrag van de agent zich manifesteert als een reeks tool-aanroepen (uitvoeringstraces).

Bestaande evaluatiemethoden lijden aan aanzienlijke beperkingen:

• Handmatige Constructie: Het handmatig maken van benchmarks is van hoge kwaliteit, maar schaalbaar tot grote, complexe handleidingen of nieuwe domeinen.
• LLM-gebaseerde Judges: Hoewel deze judges makkelijker in te zetten zijn, worstelen ze met het betrouwbaar afdwingen van strikte temporele constraints, precondities en verboden acties over lange uitvoeringstraces, wat leidt tot onbetrouwbare evaluaties.
• Alleen Uitkomst-evaluatie: Veel benchmarks controleren alleen de eindtoestand, waardoor ze niet detecteren of een agent via een niet-compliant procedurale weg tot het juiste resultaat is gekomen.

Er ontbreekt een schaalbare, reproduceerbare methode om automatisch trace-niveau compliance-benchmarks te genereren uit natuurlijke taal-handleidingen die deterministische, machine-controleerbare grading bieden.

Methodologie: Het MANTRA Framework

MANTRA (MANual-to-Test-tRAnslation) is een framework ontworpen om automatisch compliance-benchmarks te synthetiseren uit procedurale documenten in natuurlijke taal en toolschema's. Het werkt via een drie-staps proces dat LLM-generatie combineert met formele verificatie:

1. Document Inname en Scenario-generatie

• Afhankelijkheidsgraaf Constructie: Het systeem neemt een procedurale handleiding ($D$) in en construeert een afhankelijkheidsgraaf ($G_D$) waarbij knopen inhoudsblokken (bijv. alinea's) vertegenwoordigen en randen hiërarchische en referentierelaties.
• Dekking-gedreven Sampling: Om taakcomplexiteit te beheersen en brede dekking te garanderen, samplet MANTRA subgrafieken ($G_{DS}$) uit $G_D$. Kleine, dichte subgrafieken leveren eenvoudige scenario's op; grotere of losjes verbonden subgrafieken induceren complexe scenario's die meerdere regels betrekken.
• Tool Relevantie & Scenario-synthese: Voor elke sample identificeert een LLM relevante tools ($T_S$) en genereert concrete scenario's ($\lambda$). Elk scenario bevat een prompt in natuurlijke taal ($p_\lambda$) en een waardering van variabelen, inclusief interne statusvariabelen (bijv. "verzoek is in behandeling") die in de prompt expliciet worden gemaakt om de agent te sturen.

2. Check-generatie en Wereldmodel Creatie

Om compliance deterministisch te evalueren, genereert MANTRA twee onafhankelijke artefacten voor elk scenario:

• Trace-niveau Checks ($C_\lambda$): Een LLM genereert een reeks boolean checks die vereiste tool-aanroepen, verboden aanroepen en temporele volgorde specificeren (bijv. check_inventory moet voorafgaan aan assign_warehouse_picker). Deze checks zijn verankerd met concrete argumentwaarden.
• Symbolisch Wereldmodel ($W_S$): Onafhankelijk genereert een LLM een wereldmodel dat de procedurale regels voorstelt als een statetoestandsysteem. Dit model is uitgedrukt in een getypeerde Domain Specific Language (DSL) die statusvariabelen, tool-precondities en postcondities definieert. Deze abstractie maakt een compacte representatie van complexe procedurale logica mogelijk.

3. Cross-validatie via SMT-oplossing

De kerninnovatie van MANTRA is het gebruik van Satisfiability Modulo Theories (SMT)-oplossers (specifiek Z3) om de gegenereerde checks en het wereldmodel cross-te valideren.

• Gebonden Model Checking: Zowel $C_\lambda$ als $W_S$ worden gecompileerd naar gebonden SMT-encoderingen ($b\Phi_h$) over een trace-horizon $h$.
• Conflict Zoeken: Het systeem zoekt naar twee soorten inconsistenties:
  1. Voorwaartse Conflict: Traces die aan de checks voldoen maar het wereldmodel schenden (wat aangeeft dat de checks te zwak zijn of het model te restrictief).
  2. Achterwaartse Conflict: Traces die voldoen aan het wereldmodel maar een specifieke check schenden (wat aangeeft dat de check te restrictief is).
• Gestructureerde Reparatielus: Wanneer conflicten worden gevonden, hanteert MANTRA een reparatielus:
  • Wereldmodel Resolutie: Als meerdere scenario's uit dezelfde sample een conflict delen, stelt een LLM een gedeelde reparatie voor het wereldmodel voor (bijv. het toevoegen van een ontbrekende preconditie).
  • Check Resolutie: Als conflicten aanhouden, identificeert en repareert het systeem specifieke checks voor individuele scenario's.
  • Deterministische Edities: Reparaties worden toegepast via een getypeerde edit-taal om correctheid te waarborgen, gevolgd door recompilatie en hervalidatie.
• Mens-in-de-Lus: Als geautomatiseerde reparaties na een vastgesteld aantal iteraties falen, markeert het systeem het scenario voor gestructureerde menselijke review, waarbij een reviewer ambiguïteiten handmatig kan oplossen.

Belangrijkste Bijdragen

1. Geautomatiseerde Pipeline: Een volledig geautomatiseerde pipeline voor het converteren van handleidingen in natuurlijke taal en toolschema's naar machine-controleerbare benchmarks met beheersbare taakmoeilijkheid en deterministische grading.
2. Twee-artefact Formulering: De scheiding van trace-niveau checks en symbolische wereldmodellen, die via SMT-oplossing cross-gevalideerd worden. Dit maakt automatische identificatie en reparatie van inconsistenties mogelijk voordat benchmarks worden geaccepteerd, waardoor menselijke tussenkomst wordt geminimaliseerd.
3. Benchmarksuite: De creatie van een nieuwe benchmarksuite met 285 diverse taken over 6 domeinen (Operations, Sneaky Sasquatch, Cabin Safety, Retail, Airline, Telecom). Deze taken schalen tot procedurale handleidingen van tot ~16.000 woorden en 148 tools, met minimale menselijke inspanning.
4. Gedetailleerde Foutanalyse: Het framework biedt trace-niveau checks die gedetailleerde debugging van agent-foutmodi mogelijk maken, en onderscheid maken tussen ontbrekende aanroepen, volgorde-overtredingen en verboden acties.

Resultaten en Evaluatie

De auteurs evalueerden het MANTRA-framework en de resulterende benchmarks met behulp van 6 verschillende LLM-agenten.

• Validatie-efficiëntie: De SMT-gebaseerde cross-validatie slaagde erin een significant deel van de gegenereerde testcases automatisch te valideren. Bijvoorbeeld, in het domein "Operations" werden 63 van de 66 gegenereerde gevallen gevalideerd na voorwaartse en achterwaartse verfijningsrondes.
• Agentprestaties: De evaluatie toonde aan dat huidige LLM-agenten worstelen met procedurale compliance. Succespercentages varieerden aanzienlijk per domein, waarbij "Retail" en "Airline" (van $\tau$-Bench) bijzonder moeilijk bleken vanwege complexe tool-gebruik in plaats van documentlengte.
• Foutmodi-analyse: Analyse van 10.895 mislukte checks toonde aan dat 76% van de fouten te wijten was aan "Missing-Required-Call" (een verplichte tool overslaan) of "Missing-Anchor" (het niet uitvoeren van de prerequisiet voor een volgordebepaling).
  • Een dominante foutpatroon was "premature writing", waarbij agenten schrijftools aanriepen voordat noodzakelijke leestools-lookup's werden uitgevoerd.
  • Het model Qwen3.6:36B toonde superieure prestaties, met name in de Airline- en Retail-domeinen, door een strikte "lezen-voor-schrijven"-gewoonte te handhaven, wat resulteerde in een 0% premature-write rate in deze domeinen.
• Vergelijking met Bestaande Benchmarks: In tegenstelling tot bestaande benchmarks die vertrouwen op handmatige constructie of LLM-judges, biedt MANTRA deterministische, trace-niveau evaluatie die schaalbaar is tot grote, ongestructureerde documenten en nieuwe domeinen met minimale menselijke inspanning.

Betekenis en Claims

Het artikel claimt dat MANTRA de levensvatbaarheid demonstreert van het combineren van geautomatiseerde benchmark-generatie met formeel onderbouwde validatiemethoden om schaalbare en betrouwbare benchmarks te creëren voor tool-gebruikende agenten.

• Betrouwbaarheid: Door SMT-oplossers te gebruiken om checks te cross-valideren tegen een wereldmodel, zorgt MANTRA ervoor dat benchmarks vrij zijn van logische inconsistenties die kunnen voortvloeien uit LLM-hallucinaties, waardoor een hoger niveau van vertrouwen in de evaluatieresultaten wordt geboden in vergelijking met LLM-as-a-judge-benaderingen.
• Schaalbaarheid: Het framework adresseert de schaalbaarheidsbottleneck van handmatige benchmark-creatie, waardoor evaluatie van agenten tegen complexe, real-world procedurale handleidingen (tot 50+ pagina's) mogelijk wordt over willekeurige domeinen.
• Debugging-capaciteit: De granulariteit van de trace-niveau checks stelt onderzoekers in staat verder te gaan dan simpele pass/fail-metrics om specifieke structurele fouten in agent-redenering te begrijpen, zoals de neiging om prerequisiet-lookup's over te slaan.

De auteurs positioneren MANTRA niet als een op zichzelf staande garantie voor veilig gedrag, maar als een kritiek onderdeel voor het ontwikkelen van betrouwbaardere AI-systemen in compliance-kritieke settings, waarbij de kloof tussen machine learning en formele verificatie wordt overbrugd.