Signal Temporal Logic guided Neural Architecture Search for safe edge AI systems
Khurram Khalil and Khaza Anuarul Hoque
Department of Electrical Engineering and Computer Science, University of Missouri, Columbia, MO 65211 USA
Corresponding author hoquek@missouri.edu
VeriNAIS is a Neural Architecture Search framework that places a Signal Temporal Logic runtime monitor inside the search loop. The framework treats each search trajectory as a discrete-time signal and checks candidate populations against deployment-facing resource limits, search-dynamics rules, and temporal interaction properties before accepting them.
VeriNAIS combines three implementation components.
- STL search signal and property library over accuracy, energy, parameter count, convolutional diversity, hypervolume, latency, and power.
- Online gatekeeper that wraps NAS oracles and rejects candidates whose hypothetical trajectory violates the monitored specification.
- Hardware profile interface and Jetson measurement harness for latency, power, and energy-aware search evaluation.
The accompanying TCAD manuscript evaluates VeriNAIS on the full NAS-Bench-201 search space across CIFAR-10, CIFAR-100, and ImageNet-16-120, with Jetson Thor telemetry and a complete TransNAS-Bench-101 hardware-profile external validity check. This public repository contains the reference implementation and human-readable result summaries. It does not package raw hardware traces, generated JSON files, generated CSV files, benchmark archives, or manuscript build files.
VeriNAIS/
|-- stl_nas/
| |-- signal.py Search signal construction
| |-- properties.py Eight-property STL specification
| |-- monitor.py Online robustness monitor
| |-- gatekeeper.py Admission gate for NAS candidates
| `-- algorithms/ NSGA-II, ENAS, LaMOO, and random search wrappers
|-- data/
| |-- nasbench201.py NAS-Bench-201 and NATS-Bench loader utilities
| |-- cifar10.py CIFAR-10 loader utility
| |-- cifar100.py CIFAR-100 loader utility
| `-- imagenet16.py ImageNet-16-120 loader utility
|-- hardware/
| |-- hw_table.py Target-device profile lookup interface
| `-- measure_harness.py Jetson measurement harness
|-- experiments/
| |-- run_nas.py Main NAS experiment entry point
| |-- ablation.py Property-subset ablation entry point
| `-- hw_deploy.py Deployment measurement entry point
|-- examples/
| `-- smoke_reference.py Synthetic smoke test
|-- pyproject.toml
`-- requirements.txt
results/
|-- reported-results.md
|-- hardware-and-generalization.md
`-- reproduction-notes.md
The implementation depends on Python, NumPy, SciPy, and optional benchmark or monitoring packages listed in VeriNAIS/requirements.txt. A minimal editable environment is below.
cd VeriNAIS
python -m venv .venv
source .venv/bin/activate
pip install -e .A dependency-light smoke test is below.
python examples/smoke_reference.pyExpected terminal ending.
smoke test passed
stl_nas/signal.py maps each accepted architecture population to a seven-dimensional signal. The monitored dimensions are top accuracy, normalized energy, parameter count, convolutional diversity, hypervolume proxy, measured latency, and measured power.
stl_nas/properties.py implements the eight-property specification used by the reference implementation. The properties cover resource bounds, monotone search progress, diversity, post-violation recovery, and stagnation-triggered complexity reduction.
stl_nas/monitor.py evaluates hypothetical trajectory extensions before commitment. stl_nas/gatekeeper.py exposes the admission decision that wraps NAS candidate generators. The monitor includes a pure NumPy robustness path for reference execution and an optional RTAMT-backed path when the dependency is available.
stl_nas/algorithms/ provides reference wrappers for NSGA-II, ENAS, LaMOO, and random search. The wrappers are deliberately lightweight so that the STL gate remains separated from any single NAS algorithm.
hardware/hw_table.py loads a measured target-device profile when supplied through VERINAIS_HW_PROFILE. The expected profile columns are arch_id, latency_mean_ms, and power_mean_w. hardware/measure_harness.py provides the Jetson measurement harness used as a reference for on-device latency and power collection.
The public results/ folder gives Markdown summaries synchronized with the manuscript-level values used during package preparation.
- Full NAS-Bench-201 coverage with 15,625 architectures.
- Evaluation across CIFAR-10, CIFAR-100, and ImageNet-16-120.
- Four NAS paradigms, NSGA-II, ENAS, LaMOO, and random search.
- Zero gated constraint violations across the reported settings.
- Hypervolume improvement in 11 of 12 paradigm and dataset settings.
- Lower measured mJ per inference in 10 of 12 settings.
- Monitoring overhead of 0.070 to 0.072 ms per candidate.
- Complete TransNAS-Bench-101 hardware-profile check over 7,352 networks.
See results/reported-results.md and results/hardware-and-generalization.md for the public summaries.
After installing dependencies and placing the NATS-Bench TSS file at VeriNAIS/data/nasbench201/NATS-tss-v1_0-3ffb9.pickle.pbz2, run an example gated search from inside VeriNAIS.
python experiments/run_nas.py \
--paradigm nsga2 \
--dataset cifar10 \
--gated \
--trials 1 \
--T 50 \
--output results/Generated outputs are written under ignored local output directories.
To evaluate against a measured device profile, set the environment variables below before running experiments.
export VERINAIS_HW_PROFILE=/path/to/device_profile.csv
export VERINAIS_HW_STRICT=1Without a supplied profile, the lookup table falls back to a small built-in calibration set intended only for code-level testing.
- This repository is a reference implementation and public result-summary package.
- Raw Jetson Thor traces and generated result ledgers are not included.
- NAS-Bench and NATS-Bench archives are not included.
- Generated JSON and CSV outputs are not included.
- Full reproduction requires the benchmark tables and a measured target-device profile.