Technische Samenvatting: Directed Neuro-Symbolic Stochastic Execution voor de Verificatie van Gedistribueerde Parallelle AI-programma's

1. Probleemstelling

Gedistribueerde parallelle Kunstmatige Intelligentie (AI) systemen kampen met kritieke betrouwbaarheidsgebreken die conventionele testmethoden niet kunnen aanpakken. Deze systemen opereren over heterogene clusters en coördineren duizenden gelijktijdige activiteiten met hoogdimensionale inputs en niet-lineaire operaties (bijv. activaties, tensorcontracties). De verificatieuitdaging komt voort uit de cumulatieve complexiteit van twee factoren:

1. Niet-determinisme: Parallelle executies lijden onder data races, deadlocks en atomiciteitsschendingen die zich alleen manifesteren onder specifieke thread-interleavings.
2. Inputcomplexiteit: AI-workloads omvatten continue, hoogdimensionale inputruimtes die worden bewaakt door niet-lineaire operaties die resistent zijn tegen klassieke analyse.

Bestaande technieken falen bij de intersectie van deze twee dimensies. Symbolische executie kampt met pad-explosie en niet-lineaire aritmetica; fuzzing schaalt goed maar dringt zelden door naar regio's die worden bewaakt door strikte numerieke condities en negeert de scheduling-dimensie; en systematische concurrency-testing controleert de scheduler maar redeneert niet over numerieke inputs. Gevolgelijk blijft de bereikbare toestandsruimte onhandelbaar voor standaardtools.

2. Methodologie: DNSSE

De auteurs stellen Directed Neuro-Symbolic Stochastic Execution (DNSSE) voor, een hybride testframework dat drie engines fuseert tot één gerichte zoektocht over de toestandsruimte van gedistribueerde AI-programma's.

2.1 Formeel Framework

Het systeem modelleert gedistribueerde AI-programma's als niet-deterministische transitiesystemen ($P = \langle T, S, I, O, \Delta, s_0 \rangle$). Correctheid wordt gespecificeerd met behulp van Linear Temporal Logic (LTL) om eigenschappen te definiëren zoals vrijheid van data races, deadlocks en atomiciteitsschendingen. Het verificatiedoel is het vinden van een spoor $\pi$ en een input $x$ die een eigenschap $\phi$ schenden.

2.2 Hybride Constraint Solving

DNSSE deelt pad-constraints $\Phi_\pi$ op in twee fragmenten op basis van een syntactische classifier $\tau$:

• Beslisbaar Fragment ($\Phi_{sym}$): Bevat lineaire aritmetica, array-indexering en synchronisatie-guards. Deze worden opgelost met een SMT-solver (Z3).
• Onhandelbaar Fragment ($\Phi_{stoch}$): Bevat niet-lineaire transcendente termen (bijv. tanh, softmax). Deze worden aangepakt via coverage-guided stochastic mutation (LibFuzzer) waarbij een branch-distance objectief wordt geminimaliseerd.

2.3 LLM-gestuurde Schedule Voorspelling

Een belangrijke innovatie is het gebruik van een Large Language Model (LLM) als een scheduler prior. De LLM analyseert de semantische structuur van de gedistribueerde code (thread program counters, lock states, pending collectives) om de enabled thread-transities te rangschikken.

• Rol: De LLM voorspelt welke interleavings het meest waarschijnlijk concurrency-schendingen blootleggen.
• Veiligheid: De LLM fungeert enkel als een geleerde prior. Haalbaarheid wordt strikt bepaald door de symbolische en stochastic engines. Als de LLM-rangschikking malafide is, valt het systeem terug op een uniforme willekeurige volgorde, waardoor formele garanties niet afhankelijk zijn van de correctheid van de LLM.

2.4 Algoritme Executie

Het kernalgoritme onderhoudt een worklist van toestanden, pad-constraints, schedules en concrete witness inputs. In elke iteratie:

1. Rangschikt de LLM de enabled transities.
2. Worden transities symbolisch uitgevoerd om pad-constraints uit te breiden.
3. Worden constraints opgelost: SMT voor de beslisbare delen, stochastic search voor de niet-lineaire delen.
4. Als een witness input wordt gevonden, wordt de nieuwe staat toegevoegd aan de wachtrij met een prioriteit afgeleid van de LLM-betrouwbaarheid en structurele risico-heuristieken.
5. Het proces gaat door totdat een eigenschapschending wordt gevonden of de dieptegrens wordt bereikt.

3. Belangrijkste Bijdragen

Het paper levert vier primaire bijdragen:

1. DNSSE Algoritme: Een nieuw hybride algoritme dat LLM-gestuurde schedule voorspelling combineert met gerichte symbolische en stochastic executie, specifiek voor gedistribueerde parallelle AI-programma's.
2. Formele Garanties: Een framework gebaseerd op transitiesystemen en LTL met bewijzen van:
   • Soundness (Correctheid): Elk gerapporteerd tegenvoorbeeld is een haalbare executie.
   • Bounded Completeness (Begrensde Volledigheid): Het systeem verkent elke haalbare trace tot een dieptegrens $D$.
   • Probabilistic Completeness (Probabilistische Volledigheid): De stochastic solver slaagt met een waarschijnlijkheid die de 1 nadert naarmens het aantal mutatie-rondes toeneemt.
   • Expected-Cost Analysis (Verwachte Kostenanalyse): Een theoretische grens die kwantificeert wanneer geleerde rangschikking superieur is aan uniforme exploratie.
3. Schaalbare Architectuur: Een gedistribueerde implementatie op PyTorch en Ray, waarbij tracing, constraint solving en fuzzing over een cluster worden verdeeld.
4. Empirische Evaluatie: Een uitgebreide evaluatie op vijf realistische gedistribueerde AI-benchmarks.

4. Experimentele Resultaten

De evaluatie werd uitgevoerd op vijf benchmarks die productiewerkbelastingen vertegenwoordigen (bijv. data-parallel training, federated learning, reinforcement learning) met in totaal ~36.900 regels code. DNSSE werd vergeleken met KLEE-AI (symbolic), P-Fuzz (distributed fuzzing) en Random testing.

• Bug Detectie: DNSSE detecteerde 73 bevestigde concurrency bugs, vergeleken met 25 voor de sterkste baseline (P-Fuzz), wat een 2,9× verbetering betekent.
• Coverage (Dekking): De gemiddelde branch coverage steeg van 68,6% (P-Fuzz) naar 91,6% met DNSSE.
• Efficiëntie: DNSesse voltooide de exploratie in gemiddeld 2.134 seconden, terwijl KLEE-AI op alle benchmarks binnen 24 uur een timeout kreeg, en P-Fuzz/Random de volledige 1-uur budget nodig hadden zonder dezelfde dekking te bereiken.
• Component Analyse:
  • De LLM scheduler was verantwoordelijk voor ~14,3% van de runtime maar was cruciaal; het uitschakelen ervan verminderde de bug detectie met 58%.
  • De stochastic solver domineerde de tijd op benchmarks met hoge niet-lineariteit (bijv. 51,2% op Graph-GNN), terwijl de SMT solver domineerde op taken met veel lineaire elementen.
  • Ablatie-studies bevestigden dat het verwijderen van een enkele component (LLM, SMT of Fuzz) de prestaties aanzienlijk verslechterde, wat hun complementaire aard aantoont.

5. Betekenis en Claims

Het paper claimt dat DNSSE erin slaagt de kloof in de verificatie van gedistribueerde parallelle AI-programma's te dichten door semantische schedule voorspelling te integreren met rigoureuze constraint solving.

• Nieuwigheid: Het is het eerste framework dat een LLM gebruikt om de schedule ruimte van gedistribueerde AI-programma's te navigeren, terwijl dit geïntegreerd wordt met een hybride symbolic-stochastic solver.
• Betrouwbaarheid: De aanpak behoudt formele soundness; de LLM beïnvloedt de efficiëntie (prioritering) maar niet de correctheid, aangezien haalbaarheid altijd wordt geverifieerd door solvers.
• Praktische Impact: Door 2,9× meer bugs te detecteren en bijna volledige branch coverage (91,6%) te bereiken op realistische benchmarks, biedt DNSSE een levensvatbaar pad naar het waarborgen van de betrouwbaarheid van veiligheidskritische gedistribueerde AI-systemen waar traditionele methoden falen.

De auteurs merken beperkingen op, waaronder de afhankelijkheid van gecureerde benchmarks en het probabilistische karakter van de stochastic solver binnen real-world budgetten, maar stellen dat het framework een robuuste fundering biedt voor toekomstige verificatie van autonome en gedistribueerde AI-systemen.