ACTAbstract Constraint Transformation

Un cadre de test et de vérification pour les réseaux de neurones. Chargez un modèle et une spécification, cherchez des contre-exemples et prouvez des propriétés par interprétation abstraite correcte et séparation-évaluation.

Commencer

Essayer en ligne

GitHub

Une seule représentation pour tous les modèles

Les modèles PyTorch, les réseaux ONNX et les propriétés VNN-LIB deviennent un même ACT Net, dans lequel les spécifications d'entrée et de sortie sont des couches ; chaque moteur vérifie donc le même problème.

Trois domaines abstraits

Propagez des bornes par intervalles, par zonotopes HybridZ ou par bornes duales issues d'une relaxation linéaire, à travers des couches MLP, CNN, RNN et Transformer.

Séparation-évaluation

Raffinez les propriétés non décidées en scindant des neurones ou des entrées, avec des sous-problèmes en lots, plusieurs heuristiques de branchement et des bornes LP, duales ou MILP.

Fuzzing en boîte blanche

ACTFuzzer cherche des violations sur GPU avec des mutations guidées par le gradient, une mise à l'échelle adaptative des perturbations et la couverture des neurones.

Contre-exemples vérifiés

Chaque contre-exemple, issu du fuzzing ou de la vérification, est contrôlé sur le modèle concret avec les mêmes spécifications d'entrée et de sortie avant d'être signalé.

Validation des vérificateurs

Confrontez les verdicts à des contre-exemples concrets et vérifiez, couche par couche, que les bornes abstraites contiennent chaque activation concrète.

Fuzzing ACT dans l'atelier en ligne