What do LLMs need to Synthesize Correct Router Configurations?

TL;DR

This paper explores how combining GPT-4 with verification tools can effectively automate the synthesis of correct router configurations, reducing manual effort significantly.

Contribution

Introducing Verified Prompt Programming, a method that integrates GPT-4 with verifiers for accurate router configuration synthesis.

Findings

GPT-4 alone produces configurations with critical errors.

Verification with localized feedback improves correctness.

Achieved 10X and 6X automation leverage in two use cases.

Abstract

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.