💻 computer science

Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning

Het artikel introduceert RNN-ProVe, een probabilistisch raamwerk dat de waarschijnlijkheid van ongewenst gedrag schat in op recurrente neurale netwerken gebaseerde beleidsstrategieën voor enkelvoudige en multi-agent versterkingslering door beleidsgestuurd bemonsteren te gebruiken om de beperkingen van bestaande verificatietools in deels waarneembare omgevingen te overwinnen.

Oorspronkelijke auteurs: Luca Marzari, Enrico Marchesini

Gepubliceerd 2026-05-15

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Luca Marzari, Enrico Marchesini

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een robot traint om een doolhof te navigeren. Deze robot heeft een speciale "geheugen" (een Recurrent Neural Network, of RNN) die hem helpt te onthouden waar hij al is geweest, zodat hij niet alleen reageert op wat hij nu ziet, maar beslissingen neemt op basis van zijn hele reis tot nu toe.

Het probleem is: Hoe weten we dat deze robot niet per ongeluk tegen een muur zal botsen?

De Oude Manier: De "Slechtst-Mogelijke" Gissing

Traditionele veiligheidscontroles proberen te bewijzen dat de robot veilig is door naar elk mogelijk ding te kijken dat ooit zou kunnen gebeuren. Ze stellen zich elke mogelijke herinnering voor die de robot zou kunnen hebben, zelfs diegene die in het echte leven onmogelijk zijn (zoals een robot die een muur onthoudt die niet bestaat).

Omdat ze elke enkele mogelijkheid moeten controleren, inclusief de onmogelijke, raken ze vaak vast. Het is als proberen een specifieke naald in een hooiberg te vinden door elk enkel stukje hooi te controleren, zelfs diegene die vanaf het begin niet eens in de schuur zaten. Dit maakt het proces ongelooflijk traag, en vaak geven ze gewoon op en zeggen ze: "We kunnen het niet zeker weten," of ze gaan ervan uit dat de robot onveilig is, enkel om veilig te zijn, wat niet erg behulpzaam is.

De Nieuwe Manier: RNN-ProVe (De "Echt-Leven" Detective)

De auteurs van dit artikel, Luca Marzari en Enrico Marchesini, hebben een nieuw hulpmiddel bedacht genaamd RNN-ProVe. In plaats van elke onmogelijke fantasie te controleren, stellen ze een slimmere vraag: "Welke werkelijke herinneringen heeft deze robot opgebouwd terwijl hij aan het leren was?"

Hier is hoe het werkt, met een eenvoudige analogie:

1. De "Haalbaarheidsorakel" (Het Geheugenfilter)

Stel je voor dat de robot duizenden trainingsrondes heeft doorlopen. Tijdens deze tijd heeft hij een specifieke set van "echte" herinneringen opgebouwd.

Oude tools kijken naar de volledige bibliotheek van alle mogelijke herinneringen (inclusief neppe).
RNN-ProVe traint een speciaal "Geheugenfilter" (een classifier). Dit filter leert onderscheid te maken tussen een echte herinnering (een die de robot daadwerkelijk heeft ervaren) en een nep herinnering (een die nooit zou kunnen gebeuren).

Denk hierbij aan een bouncer bij een club. De bouncer (het filter) controleert je ID. Als je ID aangeeft dat je daadwerkelijk op het feest was (een haalbare geschiedenis), krijg je binnen. Als je ID nep is (een onmogelijke geschiedenis), word je geweigerd. RNN-ProVe controleert alleen de veiligheid van de mensen die echt langs de bouncer zijn gekomen.

2. De "Waarschijnlijkheids"-Controle (De Risicometer)

Zodra het filter de echte herinneringen scheidt van de neppe, probeert RNN-ProVe niet om elke enkele echte herinnering te controleren (wat nog steeds te moeilijk is). In plaats daarvan neemt het een willekeurige steekproef van de echte herinneringen.

Het vraagt: "Van de 1.000 echte herinneringen die we hebben gekozen, hoeveel hebben geleid tot een crash?"

Als 10 van de 1.000 hebben geleid tot een crash, zegt het niet: "De robot is onveilig."
Het zegt: "Er is een 1% kans dat de robot in deze specifieke situatie crasht, en we zijn 99% zeker dat dit getal accuraat is."

Dit is als een weerman. In plaats van te zeggen "Het zal zeker regenen" of "Het zal zeker niet regenen", zeggen ze: "Er is een 30% kans op regen, gebaseerd op de data die we hebben." Dit geeft een veel nuttiger, kwantitatief antwoord.

Waarom Dit Belangrijk Is

Het artikel heeft dit getest op twee soorten spellen:

Single Agent: Eén robot die een rooster navigeert.
Multi-Agent: Twee robots die samenwerken om een doos te duwen.

De Resultaten:

Snelheid: De oude tools deden minuten of uren over het controleren van kleine roosters en gaven het op bij grotere. RNN-ProVe deed dezelfde controles in milliseconden.
Nauwkeurigheid: De oude tools vonden vaak "nep" problemen (vals alarm) omdat ze onmogelijke herinneringen controleerden. RNN-ProVe negeerde de onmogelijke en vond de echte risico's.
Samenwerking: De oude tools konden geen teams van robots aan die samenwerken. RNN-ProVe hanteerde het multi-agent team perfect, en controleerde of een van de teamleden een fout zou kunnen maken.

De Conclusie

RNN-ProVe is een nieuwe manier om AI-veiligheid te verifiëren die stopt met proberen elke onmogelijke scenario te controleren. In plaats daarvan richt het zich op wat er echt gebeurt tijdens het trainen. Door het onmogelijke te filteren en het echte te bemonsteren, geeft het ons een snelle, betrouwbare en wiskundige "risicopercentage" voor hoe vaak een slimme robot een fout zou kunnen maken.

Het verandert een eng, onoplosbaar wiskundig probleem in een beheersbare, statistische schatting die ons precies vertelt hoe veilig onze geschiedenis-afhankelijke AI werkelijk is.

Technische Samenvatting: RNN Probabilistische Verificatie (RNN-ProVe)

Probleemstelling

Recurrente Neurale Netwerken (RNN's) worden veelvuldig ingezet in Versterkend Leren (RL) om gedeeltelijke waarneembaarheid en coördinatie tussen meerdere agenten te hanteren door latente verborgen toestanden bij te houden die interactiegeschiedenis coderen. Het verifiëren van deze beleidsregels is fundamenteel uitdagend omdat het besluitvormingsproces afhankelijk is van de volledige geschiedenis van waarnemingen en acties, en niet slechts van de huidige input.

Bestaande verificatietools voor RNN's richten zich voornamelijk op robuustheidsanalyse tegen begrenste inputverstoringen over een vaste horizon. Deze methoden vertrouwen doorgaans op grove geometrische overbenaderingen (bijvoorbeeld intervallen of hyperrechthoeken) van de ruimte van verborgen toestanden. In de context van RL staat deze benadering spookachtige verborgen toestanden toe—combinaties van neuronwaarden die wiskundig mogelijk zijn binnen de grenzen van het netwerk, maar onhaalbaar zijn gezien het specifieke beleid en de dynamiek van de omgeving. Bijgevolg leveren deze tools vaak te conservatieve resultaten of vals-positieven op.

Bovendien vereist exacte verificatie van op RNN's gebaseerde beleidsregels het enumereren van alle bereikbare configuraties van verborgen toestanden om ongewenst gedrag te controleren. Dit probleem is equivalent aan het berekenen van maatstaven voor pre-images van neurale netwerken, wat #P-hard is vanwege de nonlineariteit en niet-convexiteit van neurale netwerken. Een exacte karakterisering is computationeel onuitvoerbaar voor niet-triviale beleidsregels, en bestaande methoden schalen niet naar multi-agent omgevingen of ruimten met hoge dimensionaliteit.

Methodologie: RNN-ProVe

De auteurs stellen RNN Probabilistische Verificatie (RNN-ProVe) voor, een raamwerk dat verschuift van exacte worst-case verificatie naar probabilistische verificatie over haalbare geschiedenissen. In plaats van te proberen alle mogelijke verborgen toestanden te enumereren, schat RNN-ProVe de waarschijnlijkheid van ongewenst gedrag door het volume van de ruimte van haalbare verborgen toestanden te kwantificeren dat leidt tot schendingen.

Het raamwerk werkt via drie hoofdfasen:

Leren van een Haalbaarheidsorakel:
- Tijdens de RL-trainingsfase verkent de agent de omgeving, waardoor een dataset van paren (toestand, verborgen toestand) $(s, h)$ wordt gegenereerd.
- RNN-ProVe traint een haalbaarheidsclassificator $C: S \times H \to \{0, 1\}$ op deze dataset. Deze classificator leert onderscheid te maken tussen verborgen toestanden die daadwerkelijk bereikbaar zijn onder het getrainde beleid (haalbaar) en die welke dat niet zijn (onhaalbaar).
- Deze stap maakt gebruik van de stelling van universele approximatie om het complexe, lagerdimensionale manifold van haalbare geschiedenissen binnen de hoogdimensionale ruimte van verborgen toestanden te benaderen.
Beleid-gedreven Steekproefneming en Verificatie:
- Voor een specifieke toestand van belang steekproeft de methode kandidaat-geschiedenisvectoren uit het domein van verborgen toestanden.
- De getrainde classificator $C$ fungeert als een orakel, filtert onhaalbare steekproeven eruit en behoudt alleen die verborgen toestanden $h^*$ die corresponderen met geldige interactiegeschiedenissen die leiden tot de huidige toestand.
- Het beleid wordt vervolgens geëvalueerd op deze gevalideerde geschiedenissen om te bepalen of ze leiden tot een schending (bijvoorbeeld het selecteren van een onveilige actie).
Statistische Schatting met Foutmarges:
- Het raamwerk berekent de verhouding van schendende gevalideerde geschiedenissen tot het totale aantal gevalideerde geschiedenissen om het volume van schendingen te schatten.
- Cruciaal leidt RNN-ProVe statistische betrouwbaarheidsintervallen af met behulp van de ongelijkheid van Hoeffding. Het splitst de totale fouttolerantie $\epsilon$ $ϵ$ en de betrouwbaarheidsparameter $\delta$ $δ$ op in twee componenten:
  - Classificatorfout: De nauwkeurigheid van het haalbaarheidsorakel.
  - Steekproefvariatie: De statistische fout uit de Monte Carlo-schatting.
- Hierdoor kan het raamwerk fout-gebonden, hoogbetrouwbare certificaten produceren met betrekking tot de waarschijnlijkheid van gedragsmatige schendingen.

Belangrijkste Bijdragen

Het artikel levert de volgende specifieke bijdragen:

Probleemformulering: Het definieert formeel het probleem van probabilistische verificatie voor recurrente RL-beleidsregels onder gedeeltelijke waarneembaarheid, waarbij expliciet rekening wordt gehouden met de verzameling haalbare verborgen toestanden die worden gegenereerd door een getraind beleid.
RNN-ProVe Raamwerk: Het introduceert een nieuw raamwerk dat haalbaarheidsleren combineert met Monte Carlo-schatting om gedragsmatige schendingen in op RNN's gebaseerde beleidsregels kwantitatief te beoordelen.
Extensie naar Multi-Agent: Het breidt het verificatieprobleem uit naar volledig coöperatief Multi-Agent RL (MARL). Het leidt fout-gebonden, hoogbetrouwbare garanties af voor de identificatie van haalbare geschiedenissen en schattingsfouten in gedecentraliseerde omgevingen, en biedt zo een hanteerbare benadering van een anderszins #P-hard probleem.
Theoretische Garanties: Het biedt een theoretisch bewijs (Stelling 2) dat de geschatte schendingssom voldoet aan specifieke fout- en betrouwbaarheidsmarges, afhankelijk van de steekproefgroottes van de classificatervalidatie en de verificatiesteekproefneming.

Experimentele Resultaten

De auteurs hebben RNN-ProVe geëvalueerd op single-agent navigatietaken en coöperatieve multi-agent "BoxPushing" (BP)-taken met behulp van DRQN-beleidsregels.

Schalbaarheid: RNN-ProVe toonde aanzienlijke schaalvoordelen. Bij navigatietaken vereisten baseline-methoden op basis van linearisatie minuten tot uren voor kleine omgevingen (4x4, 8x8) en liepen ze vast bij grotere omgevingen (16x16). Daarentegen leverde RNN-ProVe kwantitatieve resultaten in milliseconden voor alle geteste rastergroottes.
Nauwkeurigheid versus Baselines:
- In vergelijking met naïeve Monte Carlo (uniforme steekproefneming zonder haalbaarheidsfiltering) leverde RNN-ProVe nauwkeurige schattingen. Naïeve steekproefneming resulteerde in significant opgeblazen schendingspercentages (bijvoorbeeld ~23% versus ~1,6% in 4x4) omdat het onhaalbare verborgen toestanden testte die in de praktijk niet voorkomen.
- In vergelijking met exacte linearisatie-baselines (waar haalbaar) produceerde RNN-ProVe vergelijkbare schendingsindicaties (bijvoorbeeld ~1,42% versus ~1,44% in 4x4), maar dan met probabilistische garanties en een orde van grootte minder rekentijd.
Prestaties Multi-Agent: Het raamwerk slaagde erin coöperatieve beleidsregels te verifiëren in het BP-domein (rasters van 10x10 en 20x20), waarbij gemiddelde schendingspercentages van respectievelijk ongeveer 1,18% en 1,7% werden geïdentificeerd. Bestaande tools konden niet direct worden toegepast op deze coöperatieve omgevingen.
Inzicht: De experimenten onthulden dat zelfs beleidsregels met hoge gemiddelde opbrengsten een niet-uniforme generalisatie vertonen over haalbare verborgen toestanden, met specifieke sensitiviteiten in de buurt van obstakels die standaard empirische evaluaties missen.

Betekenis en Claims

Het artikel betoogt dat exacte worst-case verificatie voor recurrente RL-beleidsregels niet alleen computationeel onbetaalbaar is, maar ook niet in overeenstemming is met de structuur van geschiedenisafhankelijke besluitvorming. De auteurs stellen dat probabilistische verificatie over haalbare geschiedenissen niet slechts een heuristische versoepeling is, maar een principiële reactie op fundamentele computationele barrières.

Door zich te richten op de verzameling verborgen toestanden die daadwerkelijk bereikbaar zijn onder een beleid, biedt RNN-ProVe kwantitatieve, haalbaarheidsbewuste probabilistische garanties. Deze aanpak levert informatiever certificaten op dan binaire "veilig/onveilig" uitkomsten of te conservatieve robuustheidscontroles, waardoor een beter begrip mogelijk wordt van beleidsbetrouwbaarheid en generalisatie in complexe, gedeeltelijk waarneembare en multi-agent omgevingen. Het werk pleit voor dit probabilistische perspectief als een fundamentele aanpak voor redeneren over veiligheid in geschiedenisafhankelijke systemen.