Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

Dit artikel introduceert een nieuw raamwerk dat natuurlijke taal specificaties automatisch vertaalt naar formele verificatievragen, waardoor bestaande tools voor neurale netwerken toepasbaar worden op complexere, semantische eisen met hoge nauwkeurigheid en lage rekentijd.

De kern

Titel: Vertalers voor Neuronale Netwerken: Hoe we AI laten praten in mensentaal

Stel je voor dat je een zeer slimme, maar erg specifieke robot hebt. Deze robot is een Deep Neural Network (een soort super-AI) die bijvoorbeeld medische diagnoses stelt of auto's bestuurt. We willen zeker weten dat deze robot veilig is.

Helaas is deze robot een beetje als een oude, strenge ingenieur die alleen wiskundige formules en cijferrijen begrijpt. Als je hem vraagt: "Zorg dat de auto niet remt als er een kind op de fiets zit," kijkt hij je raar aan. Hij vraagt zich af: "Welke coördinaten? Welke pixel? Wat is de exacte snelheid in meters per seconde?"

Deze robot kan geen menselijke taal begrijpen. Hij werkt alleen met strakke, lage niveaus van data (zoals "pixel 102 is donkerder dan pixel 103"). Dit maakt het heel moeilijk om te controleren of de AI veilig is voor echte, complexe situaties.

Het Probleem: De Vertaalbarrière

In dit paper beschrijven onderzoekers een groot probleem: Hoe vertaal je wat een mens wil, naar wat een computer kan controleren?

Vroeger moest een mens (een expert) die wiskundige formules zelf schrijven. Dat was:

1. Moeilijk: Je moest een expert zijn in zowel AI als wiskunde.
2. Gevaarlijk: Als je één getal verkeerd schreef, was de hele controle waardeloos.
3. Beperkt: Je kon alleen simpele dingen controleren, niet complexe ideeën zoals "als de vogel zijn snavel verbergt, moet hij nog steeds herkend worden."

De Oplossing: Een Slimme Vertaler

De onderzoekers hebben een nieuwe "tussenpersoon" bedacht. Ze noemen dit een automatische vertaalservice.

Stel je dit voor als een tolk op een drukke luchthaven:

1. Jij (de gebruiker) spreekt gewoon Nederlands: "Controleer of de vogel nog steeds herkend wordt als zijn snavel bedekt is."
2. De Vertaler (onze nieuwe tool) pakt deze zin op. Hij gebruikt twee soorten slimme hulpmiddelen:
   • Een Taal-expert (LLM): Deze begrijpt wat je bedoelt. Hij denkt: "Ah, de gebruiker wil weten of het model robuust is tegen verstoring van het 'snavel'-gedeelte."
   • Een Oog-expert (Perceptie-model): Deze kijkt naar de foto en zegt: "Oké, ik zie de vogel. Hier is de snavel. De coördinaten zijn X, Y, Z."
3. De Vertaler schrijft nu de perfecte wiskundige formule voor de strenge ingenieur-robot: "Check of de uitkomst gelijk blijft als pixels in dit specifieke vakje (de snavel) worden gewijzigd."
4. De Ingenieur-robot doet zijn werk, checkt de formule en zegt: "Veilig!" of "Onveilig, hier is een voorbeeld waar hij faalt."

Hoe werkt het in de praktijk?

De onderzoekers hebben dit systeem getest op drie verschillende gebieden, net als een multitalent dat zich aanpast aan verschillende situaties:

• Tabellen (Bijv. Kredietverlening):
  • Jij zegt: "Mensen onder de 50 jaar mogen geen andere credit-score krijgen."
  • De tool: Zoekt in de tabel naar de kolom "Leeftijd" en maakt een regel: "Als leeftijd < 50, dan moet de uitkomst gelijk blijven."
• Afbeeldingen (Bijv. Vogels herkennen):
  • Jij zegt: "De vogel moet herkend worden, zelfs als zijn snavel bedekt is."
  • De tool: Kijkt naar de foto, vindt de snavel, en zegt tegen de robot: "Verander alleen de pixels van de snavel en kijk of de naam van de vogel nog steeds klopt."
• Geluid (Bijv. Alarmen herkennen):
  • Jij zegt: "Het noodsignaal moet herkend worden, zelfs als er boorgeruis overheen zit."
  • De tool: Zoekt in het geluidsbestand naar het moment dat er geboord wordt en zegt: "Versterk dat stukje geluid en check of het alarm nog steeds klinkt."

Waarom is dit belangrijk?

Vroeger was het controleren van AI-veiligheid als het proberen te lezen van een boek in een taal die je niet spreekt. Je moest eerst een cursus volgen om de taal te leren.

Met deze nieuwe tool is het alsof je een live-tolk krijgt. Je kunt gewoon praten in je eigen taal, en de tool zorgt ervoor dat de strenge AI-veiligheidscontroleurs precies begrijpen wat je bedoelt.

De voordelen:

• Iedereen kan het doen: Je hoeft geen wiskundig genie te zijn.
• Veiliger: We kunnen nu veel complexere en realistischere situaties testen.
• Sneller: Geen handmatig schrijven van duizenden formules meer.

Kortom: De onderzoekers hebben een brug gebouwd tussen menselijke intentie (wat we willen) en machine-logic (wat de computer kan checken). Hierdoor kunnen we AI-systemen veel beter en veiliger maken voor de echte wereld.

Technische samenvatting

Probleemstelling

Huidige tools voor de formele verificatie van diepe neurale netwerken (DNN's) kampen met een significant gebruiksgemak-probleem. Hoewel deze tools wiskundig bewijzen kunnen leveren dat een model voldoet aan bepaalde correctheidseisen, kunnen ze momenteel alleen lage-niveau specificaties verwerken. Deze specificaties moeten worden uitgedrukt als numerieke constraints over vaste invoerdimensies (bijv. "als pixel 100-200 wordt verstoord, mag de output niet veranderen").

Dit creëert een kloof tussen:

1. Hoge semantische intentie: Wat gebruikers werkelijk willen garanderen (bijv. "De classificatie van een vogel moet correct blijven, zelfs als de snavel wordt afgedekt" of "De kredietbeslissing mag niet veranderen voor mensen jonger dan 50").
2. Lage technische implementatie: De noodzaak om deze intenties handmatig te vertalen naar complexe numerieke formules.

Deze vertaalslag is foutgevoelig, vereist specialistische kennis en is niet schaalbaar, vooral bij ongestructureerde data (zoals afbeeldingen of audio) waar de relevante regio's (bijv. de snavel van een vogel) variëren per input en niet vastliggen in de invoerstructuur.

Methodologie

Het paper introduceert een nieuw kader dat de kloof overbrugt door een automatische generatie van specificaties te implementeren. In plaats van nieuwe verificatie-algoritmen te ontwikkelen, fungeert het systeem als een integratielaag die natuurlijke taal specificaties omzet in standaard numerieke verificatiequeries die bestaande verifiers kunnen verwerken.

De pipeline bestaat uit drie fasen (gevisualiseerd in Algorithm 1):

1. Parsing (Ontleding):

   • Een Large Language Model (LLM) analyseert de natuurlijke taal specificatie van de gebruiker.
   • Het extrahert twee componenten: een set van semantische objecten die gelokaliseerd moeten worden (bijv. "vogelsnavel", "drillgeluid") en een operatie die op deze objecten moet worden toegepast (bijv. "occluderen", "versterken").

2. Detectie (Grounding):

   • Een perceptiemodel (zoals een Vision-Language Model of Audio-Language Model) lokaliseert de geëxtraheerde objecten in de concrete inputdata.
   • Voor afbeeldingen wordt gebruik gemaakt van Open-Vocabulary Object Detection (bijv. Grounding DINO) om de coördinaten van het object te vinden.
   • Voor audio wordt gebruik gemaakt van Sound Event Localization om tijdsintervallen te identificeren.
   • Bij gestructureerde tabulaire data (bijv. kredietdata) wordt de "detectie" gereduceerd tot een directe mapping van feature-namen naar invoerindices.

3. Specificatiegeneratie:

   • Op basis van de input, de gedetecteerde coördinaten/tijdsintervallen en de geëxtraherde operatie, wordt een gegroundeerde formele specificatie ($P_x$) gegenereerd.
   • Deze specificatie is een standaard lokale robustheidseis (bijv. "voor alle variaties binnen het gedetecteerde gebied, moet de output gelijk blijven").
   • Deze query wordt vervolgens naar een bestaande DNN-verifier gestuurd om te controleren of het model veilig is ($SAFE$) of een tegenvoorbeeld te genereren ($UNSAFE$).

Belangrijkste Bijdragen

1. Identificatie van de gebruiksgemak-kloof: Het paper benadrukt dat de moeilijkheid om hoge-level intenties om te zetten in lage-level constraints een grote belemmering is voor de adoptie van formele verificatie in de praktijk.
2. Geautomatiseerd vertaalmechanisme: Een end-to-end pipeline die natuurlijke taal specificaties omzet in formele queries zonder de onderliggende verifier te hoeven aanpassen. Dit werkt voor gestructureerde (tabellen), ongestructureerde (afbeeldingen) en audio-data.
3. Empirische validatie: Het paper demonstreert de haalbaarheid door de pipeline toe te passen op diverse case studies, waaronder credit scoring modellen en vogelclassificatie (CUB-200-2011 dataset).

Resultaten

De evaluatie toont aan dat de aanpak robuust en effectief is:

• Parsing: Moderne LLM's (zoals GPT-5 Mini en Gemini 3 Flash) halen een hoge nauwkeurigheid (85% - 100%) bij het correct identificeren van objecten en acties uit natuurlijke taal.
• Grounding (Detectie): Hoewel open-vocabulary detectie complex is, bereikt het systeem een gezamenlijke succesrate van 83% wanneer meerdere configuraties worden gecombineerd (d.w.z. als ten minste één configuratie het object correct lokaliseert).
• Eindresultaat: De gegenereerde specificaties kunnen direct worden verwerkt door bestaande verifiers. Het systeem slaagt erin complexe semantische specificaties te verifiëren die voorheen onbereikbaar waren, zoals het testen van robustheid tegen verstoringen van specifieke objecten in een afbeelding zonder handmatige coördinatie.

Betekenis en Impact

Deze studie is een doorbraak voor de praktische toepassing van formele verificatie in veiligheidskritieke systemen (zoals autonoom rijden, medische diagnose en industriële monitoring).

• Verlaagde drempel: Gebruikers hoeven geen experts te zijn in formele methoden of numerieke constraints; ze kunnen hun eisen in natuurlijke taal formuleren.
• Herbruikbaarheid: De aanpak vereist geen wijziging van bestaande verifiers, maar maakt gebruik van mature componenten (LLM's en perceptiemodellen).
• Semantische relevantie: Het stelt onderzoekers en ingenieurs in staat om te verifiëren op het niveau van menselijk begrip (bijv. "is het systeem robuust als de snavel wordt bedekt?") in plaats van op het niveau van pixels of array-indices.

Kortom, het paper transformeert DNN-verificatie van een niche-technische discipline naar een toegankelijker hulpmiddel voor het waarborgen van semantische correctheid in real-world AI-systemen.