Technische Samenvatting: Verificatie van Neurale Netwerken met Zwevend Komma op Softwareniveau
Probleemstelling
Hoewel de verificatie van neurale netwerken aanzienlijk is gevorderd in het bieden van formele garanties voor geïdealiseerde, reële modellen, schieten deze benaderingen vaak tekort omdat ze geen rekening houden met de specifieke implementatiedetails van uitgerolde systemen. In veiligheidskritische toepassingen (bijv. CPS, IoT) worden neurale netwerken geïmplementeerd met behulp van eindige-precisie zwevend kommagetalsaritmetiek (meestal 32-bit IEEE 754) en vertrouwen ze op standaard wiskundige bibliotheken (bijv. math.h). Deze laag-niveau details introduceren afrondingsfouten en niet-associatieve gedragingen die de veiligheidsbewijzen afgeleid van oneindige-precisie modellen ongeldig kunnen maken. Zo laat het artikel zien dat de SoftSign activatiefunctie, die monotoon stijgend is in reële rekenkunde, niet langer monotoon stijgend is wanneer deze wordt geïmplementeerd in 32-bit zwevend kommagetalsarithmetiek.
Bestaande pogingen om neurale netwerkcode op softwareniveau te verifiëren, hebben gemengde resultaten opgeleverd. Softwareverifieerders hebben vaak moeite om te schalen naar grote instanties van neurale netwerken, waardoor praktijkgebruikers worden gedwongen terug te vallen op onveilige oneindige-precisie modellen of verificatie op te geven ten gunste van testen. Bovendien is bij bestaande tools geobserveerd dat ze in bepaalde omgevingen onjuiste resultaten produceren, wat twijfel zaait over hun betrouwbaarheid als veiligheidsorakels voor zwevend kommagetalsimplementaties. Er is een gebrek aan rigoureuze, gestandaardiseerde evaluatie van geautomatiseerde softwareverifieerders specifiek op neurale netwerkcode.
Methodologie
Om deze hiaten aan te pakken, hebben de auteurs een rigoureuze evaluatie uitgevoerd van acht state-of-the-art geautomatiseerde softwareverifieerders op neurale netwerkcode. De methodologie bestond uit drie primaire componenten:
Benchmark Constructie (NeuroCodeBench 2.0): De auteurs hebben een uitgebreide benchmark geconstrueerd bestaande uit 912 verificatievoorbeelden. Deze benchmark omvat:
- Wiskundige Functies: 58 instanties die eigenschappen (bijv. monotoniciteit, periodiciteit, lineaire grenzen) testen van standaard
math.h functies.
- Activatiefuncties: 57 instanties die eigenschappen testen van veelvoorkomende activaties (bijv. ReLU, TanH, SoftSign, GELU).
- Neurale Lagen: 86 instanties die affiene transformaties, normalisatie, pooling en SoftMax-lagen dekken.
- Volledige Neurale Netwerken: 711 instanties inclusief Hopfield-netwerken, SAT-gecodeerde ReLU-netwerken, polynoombenaderingsnetwerken, Lipschitz-begrensde netwerken en netwerken afgeleid van VNN-COMP (Probability Density en Reinforcement Learning taken).
- Grondwaarheid (Ground Truth): Elke instantie is vooraf gelabeld als "veilig" of "onveilig" met technieken zoals brute-force testen, uitputtende constructie of tegenvoorbeeldgeneratie, wat zorgt voor een bekende correcte uitspraak voor evaluatie.
Standaardisatie en Compatibiliteit: Om een eerlijke vergelijking en reproduceerbaarheid te garanderen, hebben de auteurs alle benchmarkinstanties omgezet naar het formaat dat wordt gebruikt door de International Competition on Software Verification (SV-COMP). Dit hield in dat er zelfstandige C-bestanden zijn gemaakt die de modelimplementatie, veiligheidseigenschappen en noodzakelijke afhankelijkheden bevatten. De workflow maakte gebruik van het BenchExec-framework om bronlimieten en uitvoering te beheren, waardoor werd gegarandeerd dat de tools werden uitgevoerd met dezelfde configuraties als gebruikt in de 2024 SV-COMP editie.
Experimentele Evaluatie: De studie evalueerde acht tools (2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer) onder twee condities:
- Baseline: Het draaien van verifieerders op de pure benchmarkinstanties.
- Operationele Modellen: Het verstrekken van expliciete C-implementaties van de
math.h bibliotheek (met gebruik van MUSL en CORE-MATH) om te zien of het leveren van de functiedefinities de verificatieresultaten verbetert.
- Historische Analyse: De auteurs analyseerden ook de historische prestaties van één tool (ESBMC) van 2018 tot 2026 om trends in het veld te observeren.
Belangrijkste Bijdragen
- NeuroCodeBench 2.0: De creatie van een grootschalige, grondwaarheid-gebaseerde benchmark die specifiek is ontworpen voor de softwarematige verificatie van zwevend kommagetals neurale netwerken. Het bevat 912 instanties variërend van eenvoudige functies tot volledige netwerken met tot 170K parameters.
- SV-COMP Integratie: De benchmark is geformatteerd om compatibel te zijn met de SV-COMP-infrastructuur, waardoor het deel uitmaakt van de officiële benchmarkset voor de 2026 editie. Dit maakt geautomatiseerde, reproduceerbare evaluatie mogelijk met standaard toolconfiguraties.
- Rigoureuze Evaluatie: De eerste systematische studie die acht state-of-the-art softwareverifieerders vergelijkt op neurale netwerkcode, waarbij een aanzienlijke variantie in prestaties en correctheid wordt onthuld.
- Operationele Model Analyse: Een onderzoek naar de vraag of het verstrekken van expliciete implementaties van wiskundige bibliotheken (MUSL, CORE-MATH) de prestaties van de verifieerder verbetert, waarbij werd vastgesteld dat de impact tool-afhankelijk is en vaak verwaarloosbaar of negatief is.
Resultaten
De evaluatie leverde verschillende kritische bevindingen op over de huidige staat van softwareverificatie voor neurale netwerken:
- Lage Correctheid en Schaalbaarheid: De resultaten werden beschreven als "vrij teleurstellend". De tools vertoonden een grote variantie over de benchmark; de best presterende tool (CBMC) loste 371 van de 912 instanties correct op, terwijl anderen er aanzienlijk minder oplosten. Het gemiddelde oplossingscijfer per categorie varieerde, waarbij sommige complexe categorieën (bijv. Reinforcement Learning) oplossingscijfers van slechts 3% lieten zien. De meeste tools slaagden er niet in om meer dan een enkele neurale laag tegelijk te verifiëren.
- Onjuiste Uitspraken: Verschillende tools produceerden een hoog percentage onjuiste resultaten. Zo produceerde CBMC bijna 25% onjuiste definitieve uitspraken (voornamelijk false positives), en ook Pinaka en UAutomizer vertoonden significante foutpercentages. Alleen ESBMC produceerde geen onjuiste uitspraken onder de tools die een substantieel aantal instanties oplosten.
- Impact van Operationele Modellen: Het verstrekken van expliciete implementaties van
math.h (MUSL of CORE-MATH) leidde niet tot zichtbare verbeteringen in het algemeen. Voor sommige tools (CBMC, ESBMC, Pinaka) nam de prestatie zelfs af door de toegevoegde complexiteit van het verifiëren van de bibliotheekcode. Voor andere (CPAChecker, PeSCo) nam het aantal opgeloste instanties toe, maar dit ging vaak gepaard met een toename van onjuiste uitspraken.
- Schaalbaarheidslimieten: Tools hadden aanzienlijke problemen met volledige neurale netwerken. Het oplossingscijfer daalde naar enkel cijfers voor complexe categorieën zoals Reinforcement Learning en Probability Density. Zelfs voor synthetische netwerken konden tools zoals ESBMC alleen instanties met zeer kleine breedtes (bijv. breedte 4) oplossen voordat ze in de tijdlimiet liepen.
- Historische Vooruitgang: De analyse van ESBMC van 2018 tot 2026 toonde niet-monotone maar over het algemeen constante verbeteringen. Een opvallende piek in onjuiste uitspraken in 2022-2023 werd toegeschreven aan een implementatiefout in een k-inductie algoritme, die werd gecorrigeerd na de release van de eerdere NeuroCodeBench 1.0. De introductie van NeuroCodeBench 1.0 in 2024 leidde tot een drastische vermindering van onjuiste uitspraken binnen de gemeenschap, hoewel de impact van NeuroCodeBench 2.0 (eind 2025) gematigder was.
Betekenis en Claims
Het artikel beweert dat hoewel het verifiëren van neurale netwerken op softwareniveau conceptueel haalbaar is, bestaande state-of-the-art softwareverifieerders nog niet klaar zijn om deze taak effectief aan te pakken. De studie benadrukt dat huidige tools niet betrouwbaar meer dan een enkele laag kunnen controleren, frequent onjuiste resultaten geven en onvoldoende ondersteuning bieden voor standaard wiskundige bibliotheken.
De auteurs stellen dat hun werk dient als een noodzakelijke "reality check" voor de verificatiegemeenschap. Door een rigoureuze benchmark met bekende grondwaarheid te bieden, demonstreren zij dat de kloof tussen geïdealiseerde verificatie en softwareimplementatie momenteel te groot is voor bestaande tools om zonder significante verbeteringen te overbruggen. De auteurs stellen dat de release van NeuroCodeBench al vooruitgang heeft gestimuleerd, wat blijkt uit de vermindering van onjuiste uitspraken na de initiële release. Echter, de auteurs concluderen dat het certificeren van de volledige implementatie van neurale netwerken tegen worst-case numerieke afwijkingen een langetermijnuitdaging blijft die native ondersteuning voor wiskundige bibliotheken en aangepaste beslissingsprocedures voor zwevend kommagetalsarithmetiek vereist.