Verified algorithm design supports intent-based transport network control
From Intents to Algorithms: Verified Algorithm Discovery for Transport Networks
Networking and Internet ArchitectureMultiagent Systems
Summary
Networks need to be set up so traffic flows efficiently, but making software that chooses the best way can be tricky and must be reliable. The authors created a system that uses rules and a small trusted program to check algorithms that decide how to route traffic, instead of relying only on AI-generated code, which can be unpredictable. They tested their approach on realistic network setups and found that their method can reliably produce good routing algorithms, though it didn’t show clear improvement from using AI to create the code. This work helps ensure network algorithms meet strict requirements for correctness and safety.
What this means in practice
- •For network schedulers: Check new routing algorithms for correctness and constraints automatically to ensure network traffic meets latency and capacity limits.
- •For software testers: Use verified, bounded designs to validate network control software without relying on unpredictable AI-generated code outputs.
Authors
Behnam Ojaghi, Ricard Vilalta, Raul Muñoz
Abstract
Intent-based networking decouples desired outcomes from device-level configuration, but most systems still map intents to parameters of an algorithm selected in advance. Large language models (LLMs) create an opportunity to automate algorithm design, yet unrestricted generated code is unsuitable for transport-network control because feasibility, reproducibility, and robustness must be enforced independently of the model. We present VERA-TN, a verification-guided framework that compiles a network intent into a bounded algorithm-design specification. The target architecture uses an LLM as a semantic variation operator over typed request-ordering and path-ranking programs; generated logic remains separated from a trusted allocator that enforces path validity, latency, capacity, and single-path constraints. We prove feasibility preservation under explicit assumptions and establish a sufficient bound for the lexicographic latency tie-break in the exact reference model. The released proof-of-concept instantiates the same interface with a bounded ten-parameter numerical candidate and deterministic replay, rather than a completed live-LLM/AST study. Across 150 certified held-out cases on a 28-node TEFNET24-derived hierarchy, evolutionary search reaches a mean priority-utility ratio of 0.958, compared with 0.952 for equal-budget random search and 0.940 for priority-greedy routing. The gain over random search is small but statistically detectable (Holm- adjusted p = 0.0083). The candidate does not improve congestion relative to MILP-C, and the effect of failure-aware training is inconclusive at the 0.05 level (p = 0.051). Eight discovery runs on the official national topology and replay on 12 unseen metro-regional topologies show no stable intent-specific specialization. These results support the trust-boundary and numerical-evolution claims but do not establish a benefit from LLM generation.