Formally-Certified ISS Small-Gain Stability
for Heterogeneous Swarms with Learned Dynamics
A small, honestly-scoped research prototype — not a finished paper.
MIT License
4 heterogeneous agents
from-scratch IBP + branch-and-bound
source on GitHub
Targets a gap identified by a literature check (Aug 2026): no published work formally
certifies Input-to-State Stability (ISS) for a multi-agent swarm where each
agent's dynamics is a trained neural network (not a known analytic model),
agents are heterogeneous, and the interaction topology
switches over time — combining vector-Lyapunov small-gain theory
(Dashkovskiy–Rüffer–Wirth), Lyapunov-equation structure, and from-scratch formal
neural-network verification.
What's actually here
- 4 heterogeneous agents, each a damped nonlinear oscillator with different
physical parameters.
- Each agent's closed-loop controller is a trained MLP, not the
analytic law — verification runs against the actual network, including its
fitting error.
- A from-scratch interval bound propagation + branch-and-bound verifier proves a
local exponential ISS decay rate for each agent's trained network, over a
bounded domain, with no sampling.
- A closed-form Lyapunov candidate derived to give exact cancellation
for the analytic system (confirmed symbolically). A naive diagonal candidate
provably fails for this system class — found and fixed during development,
not assumed away.
- A small-gain matrix assembled via Young's inequality, generalized to
asymmetric/non-reciprocal coupling. For switching topologies, the gain matrix
is entrywise monotone in active edges, so one verification pass on the
complete graph certifies every possible switching sequence.
Results
0.19 – 0.64
verified per-agent ISS decay rates λᵢ
~8.8h
branch-and-bound verification time
Symmetric (consensus-style) coupling is far more forgiving than the
certificate assumes. Certified threshold κ*≈0.0095, but the real system
never diverged even at 800× that threshold. This traces to a real
structural fact: κ·(pⱼ−pᵢ) coupling is close to a graph-Laplacian
force — it redistributes state rather than injecting energy. The certificate is
correct here, just very conservative.
Non-reciprocal coupling is a different story. Motivated by the
non-reciprocal phase-transition literature (Fruchart, Hanai, Littlewood &
Vitelli, Nature 592, 2021), a directed-ring coupling where each agent is
pulled toward the next but not pulled back shows a sharp, real instability:
bounded at κ_fwd=2.0, all 5 seeds diverge to state magnitude >10⁶ at
κ_fwd=5.0. No per-agent isolated stability test would ever reveal this —
each agent alone is individually, provably stable. The generalized certificate
predicts safety only below κ_fwd*≈0.0286 — conservative by ~70–170×, but
sound: it never falsely certifies past the real cliff. This is the
actual payoff case for the whole exercise.
What this is not
- Not a tight/near-optimal small-gain condition — both cases show real
conservatism (up to ~170×).
- Not a delay-based analysis — only non-reciprocal gain asymmetry was
tested, not communication delay.
- Not evaluated beyond 4 agents, 2D per-agent state, or this coupling family.
- Not submitted or claimed as beating any specific prior work — see the
repo's
LITERATURE_CHECK.md for exactly what was and wasn't found.
Run it
pip install -r requirements.txt
python iss_swarm.py # full pipeline: train, formally verify (slow, ~9h), simulate
python stress_test.py # symmetric coupling stress sweep (fast, reuses trained models)
python asymmetric_test.py # non-reciprocal coupling stress test (fast)