Technische Samenvatting: Formele Verificatie van Analoge Neuronale Netwerken onder Procesvariaties met Polynoom-Zonotopen

Probleemstelling

Analoog neurale netwerken (ANN's) bieden aanzienlijke voordelen in energieverbruik, verwerkingssnelheid en chipoppervlak ten opzichte van digitale tegenhangers, waardoor ze ideaal zijn voor energie-beperkte Internet of Things (IoT)-toepassingen. Echter, als fysieke schakelingen zijn ANN's zeer vatbaar voor variaties in het fabricageproces (bijvoorbeeld gate-breedte, drempelspanning, oxide-dikte). Deze variaties veroorzaken afwijkingen ten opzichte van het nominale model, wat de veiligheid en nauwkeurigheid van het netwerk in gevaar kan brengen.

Traditionele verificatiemethoden vertrouwen op tijdrovende Monte Carlo-simulaties om de circuitfunctionaliteit onder deze variaties te valideren. Voor complexe netwerken, zoals Convolutional Neural Networks (CNN's), kunnen deze simulaties dagen duren om te voltooien, wat een knelpunt creëert in het ontwerpcyclus. Bovendien falen bestaande modelleringbenaderingen vaak om het volledige systeemgedrag te vangen of missen ze schaalbaarheid over verschillende netwerkarchitecturen.

Methodologie

De auteurs stellen een formele verificatiekader voor dat Monte Carlo-simulaties vervangt door op verzamelingen gebaseerde bereikbaarheidsanalyse met behulp van polynoom-zonotopen. De methodologie bestaat uit drie hoofdfasen:

1. Sensitiviteitsanalyse en Parameterreductie

De auteurs analyseerden een 130 nm CMOS analoog neuroncircuit met het PSP-transistormodel. Door middel van sensitiviteitsanalyse van meer dan 50 procesparameters stelden ze vast dat slechts twee dominante parameters ($\phi_1$ en $\phi_2$), die de oppervlaktepotentiaal van NMOS-transistors beïnvloeden, de circuitprestaties significant beïnvloeden. Andere parameters bleken verwaarloosbare effecten te hebben of werden gemitigeerd door de circuittopologie (bijvoorbeeld stroomspiegels).

2. Polynoomgebaseerde Parametrische Modellering

In plaats van de volledige circuitfysica voor elke variatie te simuleren, hebben de auteurs een polynoommodel afgeleid om het gedrag van het neuron te abstraheren.

• Gewichtsmodellering: De gewichten ($\tilde{W}_k$) worden gemodelleerd als polynomen van de derde orde van de dominante parameters $\phi_1$ en $\phi_2$.
• Bias en Ruis: Bias-termen worden als verwaarloosbaar behandeld, terwijl de resterende kleine variaties worden vastgelegd door een enkel ruisymbool van de derde orde ($d_3$).
• Formulering: Het netwerkgedrag wordt uitgedrukt als een functie van deze parameters, waardoor de gewichten kunnen worden weergegeven als verzamelingen in plaats van vaste waarden. Specifiek worden de gewichten gemodelleerd als:
  $$\tilde{W}_k = \sum_{i=0}^{3} \sum_{j=0}^{3} A_{k,i,j} \phi_1^i \phi_2^j + d_3$$
  waarbij de coëfficiënten worden bepaald via polynoomregressie op Monte Carlo-gegevens voor elke gekwantiseerde gewichtswaarde.

3. Bereikbaarheidsanalyse met Polynoom-Zonotopen

Het verificatieproces propageert invoerverzamelingen door het netwerk met behulp van polynoom-zonotopen, een verzamelingsrepresentatie die afhankelijkheden tussen variabelen kan verwerken.

• Verzamelingspropagatie: De invoerverzameling wordt laag-voor-laag gepropageerd. Lineaire lagen omvatten matrixvermenigvuldiging met de polynoom-gewichtsverzamelingen.
• Omgaan met Non-lineariteit: ReLU-activatiefuncties worden ingesloten met standaardtechnieken voor op verzamelingen gebaseerde berekening.
• Verificatie: De uiteindelijke uitvoerverzameling wordt ingesloten. Als deze insluiting geen snijpunt heeft met de verzameling van "onveilige" uitvoeren (bijvoorbeeld onjuiste classificatiegrenzen), wordt het netwerk formeel geverifieerd als veilig voor het gespecificeerde variatiebereik (bijvoorbeeld $\pm 3\sigma$).

Belangrijkste Bijdragen

1. Geoptimaliseerd Polynoommodel: Een parametrisch model dat analoog neuronprestaties onder procesvariaties nauwkeurig abstraheert met slechts twee dominante parameters en een ruis-term, waardoor de complexiteit wordt verminderd terwijl de nauwkeurigheid behouden blijft.
2. Formele Verificatie op Systeemniveau: De toepassing van bereikbaarheidsanalyse met polynoom-zonotopen om circuitniveaumodellen te verifiëren onder procesvariaties, waardoor de noodzaak voor exhaustieve Monte Carlo-simulaties wordt vermeden.
3. Schaalbaarheid: De aanpak wordt aangetoond schaalbaar te zijn over verschillende architecturen, inclusief volledig verbonden en convolutionele neurale netwerken (CNN's).
4. Efficiëntie: De methode reduceert de verificatietijd drastisch terwijl een hoog percentage variatiesteekproeven wordt ingesloten.

Experimentele Resultaten

De aanpak werd geëvalueerd op drie datasets: Wisconsin Breast Cancer, Iris en MNIST (zowel volledig verbonden als CNN-architecturen).

• Verificatietijd: De voorgestelde methode reduceerde de verificatietijd van dagen naar seconden.
  • MNIST CNN: Cadence Monte Carlo-simulatie duurde ongeveer 29.592 seconden (ongeveer 8,2 uur); de voorgestelde aanpak duurde 3,37 seconden.
  • Iris: Simulatie duurde ongeveer 865 seconden; de voorgestelde aanpak duurde 1,15 seconden.
• Nauwkeurigheid van Insluiting: De polynoom-zonootopische insluiting slaagde erin ongeveer 99% van de Monte Carlo variatiesteekproeven te vangen over alle datasets (variërend van 97,77% tot 99,51%).
• Noodzaak van het Model: Een ablatiestudie die polynoom-zonotopen vergeleek met standaard zonotopen (lineaire relaxaties) toonde aan dat lineaire modellen onvoldoende waren. Standaard zonotopen produceerden insluitingen die beslissingsgrenzen kruisten, waardoor veiligheidsverificatie faalde, terwijl polynoom-zonotopen strakke insluitingen boden die de specificaties succesvol verifieerden.

Betekenis en Claims

Het artikel claimt dat de primaire betekenis ligt in het mogelijk maken van de formele verificatie van analoge neurale netwerken onder procesvariaties in een computatief haalbaar tijdsbestek. Door over te stappen van statistische simulatie (Monte Carlo) naar deterministische op verzamelingen gebaseerde analyse, stellen de auteurs het volgende in staat:

• Snelle Ontwerpcycli: Ontwerpers kunnen snel de robuustheid van analoge schakelingen tegen fabricagevariaties beoordelen zonder dagen te hoeven wachten op simulaties.
• Veiligheidsgaranties: De methode biedt formele garanties dat het netwerk correct zal functioneren binnen een gespecificeerd variatiebereik (bijvoorbeeld 99% van de steekproeven), wat kritiek is voor veiligheidskritieke IoT-toepassingen.
• Robuustheidsbeoordeling: De aanpak maakt kwantificering mogelijk van hoeveel gefabriceerde schakelingen defect zouden kunnen zijn (bijvoorbeeld het identificeren dat schakelingen die meer dan $2\sigma$ afwijken hun nauwkeurigheid kunnen verliezen), wat de behoefte aan robuustere circuitontwerpen stuurt.

De auteurs merken op dat hoewel de huidige modellen relatief klein zijn, dit een beperking is van de fysieke robuustheid van analoge schakelingen en niet van de verificatiemethode zelf. Zij concluderen dat deze aanpak de ontwerpcyclus voor grotere, robuustere analoge inferentieschakelingen aanzienlijk kan versnellen.