Logic-Based Verification of Task Allocation for LLM-Enabled Multi-Agent Manufacturing Systems

Titel: Logica-gebaseerde verificatie van taaktoewijzing voor LLM-gestuurde multi-agent productiesystemen

1. Probleemstelling

De maakindustrie staat voor de uitdaging om te voldoen aan de groeiende vraag naar gepersonaliseerde producten, wat leidt tot een toename in productvariabiliteit en dynamische operationele omstandigheden. Traditionele multi-agent systemen (MAS) voor productie zijn flexibel, maar afhankelijk van vooraf gedefinieerde taakmodellen, wat hun aanpassingsvermogen aan nieuwe productvereisten beperkt.

Recentelijk zijn Grote Taalmodellen (LLMs) geïntroduceerd om de flexibiliteit te vergroten door adaptieve taakplanning en coördinatie mogelijk te maken. Echter, LLMs hebben een inherente onbetrouwbaarheid wat betreft veiligheidsbeperkingen (zoals botsingsvermijding en volgorde-eisen). Een LLM kan een logisch plausibel plan genereren dat veiligheidsregels schendt, wat in een fabrieksomgeving tot gevaarlijke situaties kan leiden. Er is een behoefte aan een architectuur die de flexibiliteit van LLMs benut, maar tegelijkertijd de veiligheid van de uitvoering op de vloer garandeert via formele verificatie.

2. Methodologie

Het paper stelt een controle-architectuur voor die LLM-genereren taakplannen verifieert voordat ze worden uitgevoerd. De aanpak combineert LLMs met formele methoden uit de Discrete Event Systems (DES) en Temporele Logica.

Kerncomponenten van de architectuur:

• Product Agent (PA): Een LLM-gestuurde agent die natuurlijke taal (NL) productvereisten interpreteert en vertaalt naar een taakplan, weergegeven als een Gerichte Acyclische Grafiek (DAG). Deze DAG wordt gecompileerd tot een Finite State Automaton (FSA) dat het gezamenlijke gedrag van alle hulpbronnen (robots) modelleert.
• Centrale Controller Agent (CCA): Deze agent fungeert als een veiligheidsbewaker.
  • Veiligheidsspecificatie: NL-veiligheidsregels worden door de CCA (met hulp van een LLM) omgezet in gestructureerde elementen en vervolgens vertaald naar Linear Temporal Logic on Finite Traces (LTLf).
  • Automata-transformatie: Elke LTLf-formule wordt omgezet in een veiligheidsautomaton ($A_s$) met specifieke "schendingsstaten" ($Q_{v,s}$).
  • Verificatie: De CCA voert een bereikbaarheidsanalyse uit (gebaseerd op een diepte-zoekalgoritme, DFS) op het product van het uitvoeringsautomaton van het plan ($A_{plan}$) en de veiligheidsautomata ($A_{safety}$).
• Feedback en Herplanning: Als een veiligheidschending wordt gedetecteerd (een staat in $Q_{v,s}$ wordt bereikt), wordt dit niet als een definitief falen gezien. In plaats daarvan fungeert de schending als gestructureerde feedback (inclusief een "witness trace" die toont hoe de fout ontstond). Deze feedback wordt teruggegeven aan de PA, die het plan opnieuw genereert (replanning) om de fout te corrigeren. Dit proces herhaalt zich totdat een veilig plan wordt gevonden of een maximum aantal pogingen wordt bereikt.

Formele Basis:

• FSA: Gebruikt voor het modelleren van de uitvoeringslogica van hulpbronnen en het totale plan.
• LTLf: Gebruikt om temporale beperkingen (zoals "taak A moet voor taak B plaatsvinden" of "taak C en D mogen niet gelijktijdig plaatsvinden") formeel te specificeren.
• CEGIS-geïnspireerd: De cyclus van genereren, verifiëren en corrigeren is geïnspireerd op Counterexample Guided Inductive Synthesis.

3. Belangrijkste Bijdragen

1. Controle-architectuur: Een nieuw raamwerk dat verificatie van LLM-genereren taakplannen in multi-agent systemen mogelijk maakt zonder de flexibiliteit van de LLM te beperken.
2. Verificatieproces: Een methode om taakplannen te evalueren waarbij temporale logica (LTLf) wordt vertaald naar automata voor uitvoeringsniveau-validatie.
3. Feedback-mechanisme: Een gesloten lus waarbij verificatieresultaten worden gebruikt als gestructureerde input om LLM's te sturen bij het verfijnen van onveilige plannen, in plaats van alleen te vertrouwen op vooraf gedefinieerde modellen.

4. Resultaten (Case Study)

De auteurs hebben hun framework getest in een multi-robot assemblage-scenario met drie verschillende complexiteitsniveaus (S1, S2, S3), variërend in het aantal robots, onderdelen en veiligheidsregels.

• Vergelijking: Een "Pure LLM" baseline (zonder formele verificatie) werd vergeleken met het voorgestelde framework.
• Veiligheidsconformiteit:
  • S1 (2 robots, 3 delen, 2 regels): Verbetering van 50% naar 92,5% regelconformiteit.
  • S2 (3 robots, 4 delen, 3 regels): Verbetering van 75,93% naar 91,67%.
  • S3 (4 robots, 6 delen, 4 regels): Verbetering van 50% naar 86,25%.
• Kosten: De verificatietijd en het aantal reparatiepogingen namen toe met de schaal van het probleem (van 0,1s in S1 naar 25,46s in S3), wat wijst op een toename in de complexiteit van de state-space.
• Conclusie uit data: Hoewel de pure LLM vaak onveilige plannen genereerde, kon het voorgestelde framework deze fouten detecteren en corrigeren, waardoor de veiligheid aanzienlijk werd verhoogd, zij het niet altijd tot 100% (vanwege de interpretatiecapaciteit van de LLM bij het herplannen).

5. Betekenis en Toekomstperspectief

Dit werk is significant omdat het een brug slaat tussen de onvoorspelbaarheid van generatieve AI (LLMs) en de strikte veiligheidsvereisten van de industriële automatisering. Het bewijst dat het mogelijk is om LLMs in te zetten voor adaptieve planning in dynamische omgevingen, zolang er een formele "veiligheidsnet" (verificatie) aanwezig is die schendingen detecteert en corrigeert voordat ze gebeuren.

Toekomstige uitdagingen:

• Schaalbaarheid: De huidige centrale controller (CCA) kan een bottleneck worden bij zeer grote fabrieken. De auteurs suggereren een overgang naar hiërarchische of subsystem-level verificatie.
• Online verificatie: Uitbreiding naar runtime-verificatie om onvoorziene gebeurtenissen tijdens de uitvoering te hanteren.
• Convergentie: Verdere onderzoek naar methoden om de betrouwbaarheid en snelheid van convergentie tijdens het herplanningsproces te verbeteren.

Samenvattend biedt dit paper een robuust raamwerk om de "black box" van LLMs in de productie te openen en te controleren, waardoor veilige, flexibele en adaptieve productiesystemen haalbaar worden.