Source-linked AI summary
What do LLMs need to Synthesize Correct Router Configurations?
Rajdeep Mondal, Alan Tang, Ryan Beckett, Todd Millstein, George Varghese
TL;DR
The paper examines whether LLMs can synthesize correct router configurations with reduced manual effort, despite GPT-4’s elementary errors. It combines GPT-4 with verifiers that provide localized corrections, and reports verified configurations with leverage of 5X to 10X in simple use cases.
Problem
GPT-4 can make elementary errors when authoring router configurations, which are critical to network operation.
Source: §1 · p. 1Method
Verified Prompt Programming pairs GPT-4 and a human with a verification suite that automatically sends localized corrections to GPT-4.
Source: §1 · pp. 1–2Results
With a verifier and automated corrections, GPT-4 produced reasonable but not completely correct configurations for simple use cases, with reduced-human-effort leverage of 5X to 10X.
Source: §6 · p. 6Takeaways & Limitations
Modular verification seems crucial, and effective verification requires a specification and actionable localized feedback.
Source: §6 · p. 6COSYNTH was not built, and GPT-4 API calls were manually simulated, so the study does not demonstrate a working system.
Source: §2 · p. 2
Abstract
from arXiv · showhide
We investigate whether Large Language Models (e.g., GPT-4) can synthesize correct router configurations with reduced manual effort. We find GPT-4 works very badly by itself, producing promising draft configurations but with egregious errors in topology, syntax, and semantics. Our strategy, that we call Verified Prompt Programming, is to combine GPT-4 with verifiers, and use localized feedback from the verifier to automatically correct errors. Verification requires a specification and actionable localized feedback to be effective. We show results for two use cases: translating from Cisco to Juniper configurations on a single router, and implementing no-transit policy on multiple routers. While human input is still required, if we define the leverage as the number of automated prompts to the number of human prompts, our experiments show a leverage of 10X for Juniper translation, and 6X for implementing no-transit policy, ending with verified configurations.
1 Introduction
The paper asks whether LLMs can produce correct router configurations with less manual effort, given GPT-4’s tendency to make elementary errors. It proposes verified prompt programming, using verifier feedback to correct drafts, and evaluates two configuration tasks.
1 Introduction
- GPT-4 can make elementary configuration errors despite success in other language tasks, motivating checks for syntax, topology, and semantics.The paper describes these errors as potentially serious for network operation.Source: §1 · p. 1
- Verification needs a specification and actionable feedback; modular checks of routers or route maps were easier for GPT-4 to correct than whole-network checks.The authors note that incomplete specifications can leave some solutions unacceptable to users.Source: §1 · p. 1
- Verified Prompt Programming pairs an AI, a human, and a verification suite that checks correctness and issues localized corrections automatically.The verifier-to-AI feedback forms a fast inner loop, while a human can still correct outputs when automation stops.Source: §1 · pp. 1–2
- Leverage is the ratio of automated prompts to human prompts, intended to measure the verifier suite’s effect while holding the AI and human fixed.Its interpretation assumes each automatic correction would otherwise be done by a human; the authors note that leverage may fall if future LLMs need less correction.Source: §1 · p. 2
- Both use cases ended with verified configurations, with reduced manual work as the paper’s hypothesis for adding verifier-driven correction.The use cases are Cisco-to-Juniper translation and no-transit policy implementation.Source: §1 · p. 2
- The broader motivation extends prompt programming beyond configurations, while router configs offer a tractable domain with verifiers that provide localized feedback.The paper distinguishes this use of APIs and automatically generated feedback from prompt engineering.Source: §1 · pp. 1–2
2 System Organization
The proposed COSYNTH design refines verified prompt programming for router configurations, but the authors did not build it and manually simulated GPT-4 API calls. Its proposed workflow combines syntax, semantics, and, for multi-router work, topology checks with modularized prompts.
2 System Organization
- COSYNTH was not built, and GPT-4 API calls were manually simulated, so the work explores configuration authoring rather than a working system.The authors say they could not access the APIs.Source: §2 · p. 2
- The proposed verification suite checks syntax first, then semantics, with a topology verifier added for the multi-router use case.Syntax checking used Batfish; semantic verification varied by use case, and topology checking addressed missed route announcements.Source: §2 · p. 2
- For multiple routers, the Modularizer turns machine-readable topology and local-policy descriptions into router-specific prompts and verifier specifications.A Composer reassembles the resulting configuration pieces.Source: §2 · p. 3
- Initial instruction prompts are loaded from a database to avoid common mistakes, and experts can extend that database over time.The authors also use single-shot prompting and break complex prompts into simpler sub-prompts.Source: §2 · p. 3
3 Cisco to Juniper Translation
The study uses Batfish and Campion feedback to iteratively refine a Cisco-to-Juniper router configuration. The translation reached a point where neither verifier reported errors, with 10X prompt leverage, although some corrections still required human intervention.
3. Cisco to Juniper Translation
- The workflow translates a Cisco configuration into an equivalent Juniper configuration, using Batfish for syntax errors and Campion to detect and localize semantic differences.The experiment focused on routing and forwarding behavior, excluding features such as NTP servers.Source: §3 · p. 3, §3.1 · p. 3
3.1 Method
- The humanizer distinguishes syntax errors, structural mismatches, attribute differences, and policy behavior differences, which require different prompts and an order that avoids earlier errors masking later ones.For policy behavior differences, the prompts use an example prefix because the affected input space can be difficult to describe.Source: §3.1 · p. 3
3.2 Experience and Results
- Automatically generated prompts often fixed issues, but GPT-4 sometimes failed to correct redistribution or produced invalid Juniper syntax when translating a prefix-list length condition.After being told that its prefix-list syntax was invalid, GPT-4 eventually found a correct translation; correction cycles could also introduce new errors.Source: §3.2 · pp. 3–4
- 10X leverage—about 20 automated prompts to 2 human prompts—accompanied a translation that reached a point where Batfish and Campion reported no errors.The automated prompts were manually fed to GPT-4 to simulate API calls.Source: §3.2 · p. 4
- Translation errors included missing BGP local-as attributes or routing policies, differing OSPF link settings, an incorrect BGP MED value, and differing redistribution behavior.Source: §3.2 · p. 4
4 Global Policies via Local Synthesis
The section applies local-policy synthesis to BGP configurations for a no-transit network, using topology and policy checks to refine router configurations. Local policies worked better than a global prompt in this setup, but the process still required a human correction.
4 Global Policies via Local Synthesis
- The BGP workflow checks topology with a dedicated verifier, checks local policies with Batfish, then simulates BGP communication to verify the global policy.The topology verifier checks interfaces, BGP neighbors, and announced networks.Source: §4 · p. 4, §4.1 · p. 5
4.1 Method
- Experiments used a star network in which ISP routers connect directly to the first router, with local policies generated from prompts for each router.A network generator turns the topology into both a text prompt and a JSON dictionary for checking generated configurations.Source: §4.1 · p. 5, Figure 4 · p. 5
- Specifying local policies gave better results than a global no-transit prompt because verification errors could be localized to routers and route maps.The global prompt led GPT-4 to oscillate between incorrect strategies after counterexample feedback.Source: §4.1 · p. 5
4.2 Experience and Results
- Initial instructions and syntax rectification eliminated common syntax errors, but GPT-4 sometimes misplaced BGP neighbor commands in ways Batfish could not explain well enough to repair.The prompt also addressed Cisco configuration-file output and common misplaced or unwanted commands.Source: §4.2 · pp. 5–6
- GPT-4’s route-map used AND rather than the intended OR behavior, and neither Batfish’s counterexample nor an IIP example fixed the error without a human prompt.The configuration therefore filtered only routes carrying all specified communities, rather than any one of them.Source: §4.2 · p. 6
- 6X leverage came from 2 human prompts and 12 automated prompts, although the AND/OR error required a final human correction.The AND/OR case persisted despite Batfish feedback and an initial instruction example.Source: §4.2 · p. 6
5 Previous Work
Earlier LLM synthesis systems such as Jigsaw and Copilot focused on sequential programs and did not pair synthesis with verifiers. The Kani Rust verifier use case comes closer, but retains manual switching and does not use modularity or local specifications.
5 Previous Work
- Jigsaw and Copilot use language models for sequential program synthesis, but do not pair the synthesizer with verifiers.Jigsaw tests programs and performs some automatic syntax correction; Copilot can suggest invariants but does not attempt an axiomatic proof.Source: §5 · p. 6
- Jigsaw and Copilot do not address how to use a specification or provide localized feedback.Source: §5 · p. 6
- The Kani Rust verifier use case is closest to this vision, but lacks modularity and local specifications and requires users to switch manually between verifier and LLM.Its specification question is handled by treating the source program as the specification for program transformations such as optimization.Source: §5 · p. 6
6 Conclusions
The preliminary experiments find GPT-4 alone makes elementary errors that can bring networks down, while verifier-driven corrections yield reasonable but imperfect configurations with 5X–10X leverage. Modular verification and node-role descriptions matter, and more complex use cases need further testing.
6 Conclusions
- GPT-4 by itself is not ready for configuration use without a verifier; elementary errors can bring networks down.Source: §6 · p. 6
- For simple use cases, using a verifier and automated corrections via a humanizer, GPT-4 can synthesize reasonable but not completely correct configurations, with 5X to 10X leverage in reduced human effort.Modular verification seems crucial.Source: §6 · p. 6
- For global specifications, users need to describe each node’s role because the LLM’s search space is large.The paper presents modular synthesis as the dual of modular verification.Source: §6 · p. 6
- More testing in complex use cases is needed, including whether GPT-4 can add policies without disturbing existing verified policies.Source: §6 · p. 6
- The vision, leverage measure, and lessons may also be useful for synthesizing programs beyond network configurations.Source: §6 · p. 7