Installation
Il y a deux façons d'utiliser ACT.
| Vous voulez | Utilisez | Il vous faut |
|---|---|---|
| Essayer tout de suite | L'atelier en ligne | Un navigateur |
| Exécuter ACT vous-même | Une installation locale | Linux, Miniconda, git (GPU CUDA facultatif) |
Atelier en ligne
Ouvrez app.act-online.au. L'atelier exécute ACT sur son serveur ; vous n'avez rien à installer.
Installation locale
1. Créer l'environnement
Installez Miniconda, puis clonez ACT avec ses sous-modules et créez l'environnement act-py312 (Python 3.12 et PyTorch) :
git clone --recursive https://github.com/SVF-tools/ACT.git
cd ACT
conda env create -f environment.yml
conda activate act-py312Lancez toutes les commandes ACT depuis la racine du dépôt.
2. Gurobi (facultatif)
Gurobi n'est nécessaire que pour le solveur gurobi (MILP/LP). Obtenez une licence Gurobi et placez-la ici :
cp /path/to/gurobi.lic ./modules/gurobi/gurobi.licSans licence, ACT affiche un avertissement et utilise ses autres solveurs.
3. Vérifier l'installation
python -m act.back_end --generate --device cpu --dtype float64 # génère les réseaux d'exemple
python -m act.back_end --list-examples # les liste
python -m act.back_end --verify --network act/back_end/examples/nets/mlp_plain_3x8_64x64_3962224133.json --device cpuChaque niveau a sa propre ligne de commande ; --help liste toutes les options :
python -m act.front_end --help # jeux de données, benchmarks et spécifications
python -m act.back_end --help # vérification et réseaux d'exemple
python -m act.pipeline --help # fuzzing, validation et tests de conversion4. Benchmarks et jeux de données
ACT télécharge les benchmarks dans son répertoire data/ à la demande.
python -m act.front_end --list # jeux de données TorchVision et catégories VNN-LIB
python -m act.front_end --search acas # recherche par nom
python -m act.front_end --download acasxu_2023 # modèles ONNX et propriétés VNN-LIB
python -m act.front_end --download MNIST # jeu de données et ses modèles recommandés
python -m act.front_end --list-downloads # ce qui est déjà téléchargé5. Notebooks
Le répertoire ipynb/ contient de petites démonstrations, dont un exemple de fuzzer et un exemple de vérificateur.
Suite : Fonctionnement.