Repair Instead of Retraining: A Constraint-Guided Framework for Neural Network Repair

Technische Samenvatting: Reparatie in plaats van hertraining: Een door constraints gestuurd framework voor het repareren van neurale netwerken

Probleemstelling
Diepe neurale netwerken (DNN's) die worden ingezet in veiligheidskritische toepassingen blijven kwetsbaar voor adversariële perturbaties en backdoor-aanvallen. Hoewel hertraining of fine-tuning deze problemen kan mitigeren, zijn dergelijke benaderingen computationeel duur, moeilijk selectief toe te passen op reeds uitgerolde modellen, en lopen ze het risico op oncontroleerbare gedragsdrift buiten de specifieke geobserveerde fouten. Bestaande reparatiemethoden vertrouwen vaak op heuristische zoekopdrachten (grey-box) met beperkte interpreteerbaarheid, of vereisen formele architecturale transformaties en handmatig gespecificeerde polytope-constraints (bewijsbare methoden) die moeite hebben met schaalbaarheid. Er is behoefte aan een post-hoc reparatiebenadering die een balans vindt tussen interpreteerbaarheid, gedragsgetrouwheid en computationele kosten zonder volledige hertraining.

Methodologie
De auteurs stellen een configureerbaar, door constraints gestuurd framework voor dat neurale netwerkreparatie behandelt als een logica-bewust optimalisatieprobleem over een ijle set gelokaliseerde parameters. Het framework werkt in vier gekoppelde stadia:

1. Foutlokalisatie: Het systeem gebruikt DeepSHAP om neuron-niveau attributie-masks te berekenen voor zowel benigne als adversariële inputs. Het identificeert "attack-only" neuronen—die met een hoge attributie onder adversariële inputs maar een lage attributie onder benigne inputs. Deze contrastieve attributie dient als het signaal om de ijle set fout-relevante gewichten te lokaliseren.
2. Selectie van de reparatie-targets: Een ijle binaire mask ($\Theta_S$) wordt gegenereerd over de netwerkparameters op basis van de gelokaliseerde neuronen. Het framework verkent een ontwerpplan dat wordt gedefinieerd door:
   • Gewichtsdirectie: Het wijzigen van inkomende gewichten, uitgaande gewichten of biases van de kritieke neuronen.
   • Selectiebeleid: Het selecteren van gewichten via percentiel-drempels (bijv. top 5% magnitude) of willekeurige vaste budgetten ($k$).
3. Pad-constraint specificatie: De reparatie-intentie wordt gecodeerd als pad-niveau constraints met behulp van concolic execution (via PyCT).
   • Hard Constraints: Afgeleid van benigne sporen om de correcte interne vertakkingslogica te behouden.
   • Soft Constraints: Afgeleid van adversariële sporen om het model te dwingen de executie weg te leiden van de geobserveerde foutieve paden.
   • Surrogaatnetwerken: Om de onhandelbaarheid van het coderen van volledige schaal netwerken in Max-SMT solvers aan te pakken, introduceert het framework twee analyse-surrogaten:
     • $N^\Delta_w$ (Ternaire Surrogaat): Brengt niet-reparatie gewichten in kaart naar $\{-1, 0, +1\}$ op basis van magnitude, wat de formulecomplexiteit vermindert.
     • $N^\Delta_i$ (Activatie-gestuurde Surrogaat): Snijdt niet-reparatie randen weg op basis van de input-activatie magnitude.
   • Cruciaal is dat reparatie-gewichten ($\Theta_S$) exacte symbolische onbekenden blijven in alle formuleringen, terwijl niet-reparatie componenten vereenvoudigd of afgeschermd zijn.
4. Constraint-gestuurde Reparatie & Validatie: Het systeem lost een Top-K Max-SMT probleem op (met behulp van Z3) om kandidaat gewicht-updates te synthetiseren. Kandidaten worden gerangschikt op basis van een gebalanceerde score die wordt berekend via getrouwe validatie op het originele deployment netwerk $N$ (met behulp van exacte affine operaties), wat ervoor zorgt dat gerapporteerde metrieken de werkelijke runtime-gedragingen reflecteren in plaats van surrogaat-artefacten.

Belangrijkste Bijdragen

• Configureerbaar Logica-bewust Framework: Een verenigde pipeline die DeepSHAP lokalisatie, concolic path-constraint extractie, ternaire/activatie-gestuurde surrogaten en Max-SMT optimalisatie combineert.
• Formaliseerde Reparatie Ontwerpplan: De auteurs karakteriseren expliciet de interactie tussen neuron bron (attack-only vs. intersectie), gewichtsdirectie (inkomend, uitgaand, bias) en kolom-gewijze selectiebeleid, waarmee zij aantonen dat geen enkele enkele "recept" universeel optimaal is.
• Encoding-tijd Vereenvoudigingen: Technieken zoals common subexpression elimination, negation normalization en expression pruning worden geïntroduceerd om concolic constraints handelbaar te houden voor Max-SMT zonder de reparatie-semantiek te veranderen.
• Surrogaat Formuleringen: De introductie van $N^\Delta_w$ en $N^\Delta_i$ maakt het mogelijk om pad-constraints te verzamelen op vereenvoudigde modellen, terwijl de exacte symbolische representatie voor de reparatie-variabelen behouden blijft.
• Getrouwe Validatie Protocol: Een rigoureuze evaluatiemethode waarbij alle gerapporteerde nauwkeurigheid en attack success rates (ASR) worden gemeten op het originele netwerk $N$, waardoor de constraint-verzameling wordt ontkoppeld van de uiteindelijke prestatiebeoordeling.

Experimentele Resultaten
Het framework werd geëvalueerd over 4.737 runs op zes benchmarks (Fashion-MNIST, MNIST-BD, CIFAR-10, GTSRB, MNIST-6, en ResNet18). Belangrijkste bevindingen zijn:

• Backdoor Benchmarks: Op Fashion-MNIST en MNIST-BD bereikte het framework bijna volledige backdoor verwijdering. Specifiek daalde de ASR van >98% naar <8% (bijv. 99,77% $\to$ 6,66% op Fashion-MNIST) terwijl de clean accuracy behouden bleef of zelfs licht verbeterde. De meest effectieve configuratie gebruikte uitgaande gewicht modificatie met de activatie-gestuurde surrogaat ($N^\Delta_i$).
• Adversariële Benchmarks: Een cruciale bevinding was de effectiviteit van bias-only reparatie. Op MNIST-6 reduceerde bias-richting reparatie de ASR van 100% naar 5,81% met 100% behoud van clean accuracy. Op ResNet18 reduceerde het de ASR van 85,51% naar 40,42%. Deze richting was eerder onderbelicht en zou gemist zijn door methoden die zich uitsluitend richten op inkomende of uitgaande gewichten.
• Schaalbaarheidslimieten: CIFAR-10 en GTSRB bleken uitdagend onder single-layer reparatie. Hoewel er gedeeltelijke verbeteringen zichtbaar waren, toonde GTSRB minimale ASR reductie, wat wijst op een tractabiliteit-getrouwheid trade-off waarbij single-layer constraints onvoldoende zijn voor complexe, gedistribueerde fouten.
• Vergelijking met CARE: Vergeleken met de grey-box CARE methode (causaliteit-gebaseerde lokalisatie + PSO), bereikte het voorgestelde framework over het algemeen een lagere ASR en een betere behoud van clean accuracy op Fashion-MNIST en MNIST-BD, met aanzienlijk lagere wall-clock tijden (bijv. 74,4s vs. 8.745s op MNIST-BD). Echter, CARE bereikte volledige backdoor verwijdering op GTSRB, wat suggereert dat de single-layer scope van de voorgestelde methode een beperkende factor is voor bepaalde architecturen.

Betekenis en Claims
Het artikel claimt dat systematische exploratie van de reparatie ontwerpplan essentieel is voor het ontdekken van effectieve configuraties, aangezien geen enkele heuristiek universeel domineert in alle scenario's. De auteurs benadrukken dat bias-richting reparatie een kritische, eerder onderbelichte optie is voor adversariële correctie, die alleen ontdekt kan worden via deze systematische aanpak.

Het werk positioneert zich als een middenweg tussen heuristische zoekopdrachten en formele verificatie: het biedt meer interpreteerbaarheid en logische controle dan grey-box methoden, zonder de noodzaak voor de architecturale transformaties of handmatig gespecificeerde polytopes van bewijsbare reparatiesystemen. De auteurs erkennen bescheiden dat hun framework constraint-gestuurd maar niet formeel gecertificeerd is; hoewel het Max-SMT gebruikt voor synthese, zijn de uiteindelijke garanties empirisch, leunend op getrouwe validatie op het deployment netwerk in plaats van formele bewijzen over de gehele inputruimte. De resultaten benadrukken een fundamentele tractabiliteit-getrouwheid trade-off: sterkere vereenvoudigingen (grotere $\Delta$ in surrogaten) verminderen de solver tijd, maar kunnen de reparatie-begeleiding verstoren als ze niet correct gekalibreerd zijn.