DeepConfig：一个基于大语言模型（LLMs）的、可用于MAN覆盖层（MAN overlays）的可验证配置生成框架

《Computer Networks》：DeepConfig: A verifiable configuration generation framework for MAN overlays using LLMs

针对大都市覆盖网络（MAN overlay）配置复杂性和易错性问题，提出DeepConfig框架，包含知识增强的配置生成器DeepGen和分层依赖验证器DeepValidator。DeepGen通过结构化JSONet模板与领域知识库引导LLM生成高精度配置，解决多协议异构性问题；DeepValidator采用模块化分层验证策略与混合SMT/仿真方法，有效缓解状态空间爆炸问题。实验表明，DeepConfig的配置生成准确率达90%以上（基线<30%），验证效率提升100倍以上，显著降低人工干预需求。

　　

传林|朱龙龙|刘洪燕|张东|余嘉硕|廖丽达

福建福州大学计算机与数据科学学院，中国福州，350108

摘要

在现代城域网（MANs）中，基于覆盖层的架构被广泛采用，多种服务和协议层堆叠在一起，使得网络配置变得极其复杂且容易出错。有前景的方法包括形式化配置合成和人工智能辅助生成，并结合形式化验证。然而，当前的工具对于MAN覆盖层的复杂性来说还不够完善：现有的形式化合成方法通常只关注单一协议，难以捕捉复杂的跨协议交互。基于人工智能的配置生成器由于领域知识的不完整和供应商配置的异构性而不够准确，而针对这些复杂覆盖层的有效形式化验证工具仍然很少。为了解决这个问题，我们提出了DeepConfig框架，该框架包括一个精确的生成器DeepGen和一个高效的验证器DeepValidator，旨在最小化人工干预。为了实现高精度，DeepGen利用专家知识库来指导大型语言模型（LLM）。这个知识库基于一个结构化的、与供应商无关的配置规范，作为中间表示。通过向LLM提供从该知识库中检索到的精确的基于规范的配置模板和约束，我们简化了其任务，同时解决了多供应商异构性问题。反过来，DeepValidator利用专家知识进行模块化分解，构建层次化依赖图，并采用混合SMT/仿真策略将全局验证任务分解为可管理的局部问题，从而避免了状态空间爆炸。实验表明，DeepConfig的生成精度超过90%（而基线方法的精度低于30%），在100节点网络上，其验证速度比单体方法快100倍以上。

引言

城域网（MANs）承载着各种关键服务，包括移动基站回传、企业VPN、住宅宽带和IPTV，通常通过在基于MPLS [2]/SRv6的传输网络上部署L2/L3 VPN和EVPN [1]覆盖层服务来实现。在本文中，我们将构建在城域传输网络之上的此类虚拟化逻辑网络统称为MAN覆盖层。虽然MAN覆盖层通过将逻辑拓扑与物理基础设施解耦提供了高灵活性 [3]，但它们也引入了显著的复杂性：多个协议（例如EVPN [1]覆盖在SRv6 [4]上）的深度嵌套和紧密耦合使得配置管理变得非常困难。至关重要的是，覆盖层配置通常应用于提供商边缘（PE）设备——这些设备是服务聚合和隧道的枢纽。因此，即使在这些点上的微小配置错误也往往会导致连锁故障，从而导致广泛的服务中断 [5]、[6]、[7]。

为了解决网络配置任务的高复杂性和易出错性问题，现有研究主要遵循两个方向。第一个方向是形式化配置合成 [8]、[9]、[10]、[11]、[12]，它将高级网络意图和低级协议行为建模为一个统一的形式化约束问题，然后使用自动化求解器来合成满足这些约束的低级配置参数。第二个方向采用生成式AI和形式化验证相结合的两阶段范式 [13]、[14]。这种方法首先利用人工智能辅助生成 [14]、[15]、[16]、[17]、[18]、[19]、[20]、[21] 来提高效率并减少误配置，然后通过严格的形式化验证 [22]、[23] 来确保生成的配置满足所需的属性。然而，当这两种方法应用于复杂的MAN覆盖层场景时，它们仍然存在显著的限制。

形式化配置合成的局限性。现有的形式化配置合成方法通常只在预定义的配置框架上填充部分参数，且其用户界面不便于操作员使用，难以直接从高级意图推导出完整的网络范围配置。此外，这些工具通常针对单一协议或特定场景（例如仅BGP或仅SRv6）进行定制，缺乏多协议交互的统一模型，这使它们不适合MAN覆盖层，在这些场景中IGP、BGP、MPLS和SRv6必须紧密协作。

人工智能生成的MAN覆盖层配置的不准确性。在生成方面，两种主要方法都有关键瓶颈。基于图神经网络的方法 [15]、[16]、[24] 可以建模网络结构，但难以捕捉高级操作意图，且通常针对单一协议进行优化，因此在具有多样化、堆叠协议的MAN覆盖层环境中效果不佳。基于LLM的方法 [14]、[17]、[18]、[19]、[20]、[21] 可以将自然语言意图转换为配置，但由于缺乏专门的网络知识库、高质量微调数据集的稀缺以及不同供应商配置命令的异构性，其准确性在复杂的MAN覆盖层中会大幅下降。

MAN覆盖层形式化验证的性能瓶颈MAN覆盖层的固有复杂性导致在形式化编码过程中约束的组合爆炸，从而严重限制了求解器的性能。尽管研究人员提出了增量验证、算法优化和模块化分解等技术来减少问题规模和提高求解器效率，但在MAN覆盖层的背景下，这些方法仍有显著局限性。增量验证 [25] 难以处理网络需求的基本变化；算法优化 [26]、[27]、[28]、[29]、[30]、[31] 过度依赖于简化假设，而这些假设在复杂环境中往往不成立；模块化分解 [3]、[32]、[33]、[34] 受到定义大量所需模块间接口的挑战的阻碍。

为了填补这一空白，我们提出了DeepConfig框架，用于MAN覆盖层的配置生成和验证。该框架包括两个核心组件：专为MAN覆盖层设计的精确生成器DeepGen和专为MAN覆盖层设计的高效验证器DeepValidator。其工作流程如下：DeepGen首先生成网络配置，然后由DeepValidator进行验证。只有在验证失败时才需要人工干预。为了实现最小化人工干预的最终目标，DeepConfig必须克服以下挑战。

•

配置精度受到多供应商命令异构性和缺乏针对MAN覆盖层场景的专家知识库及高质量微调数据集的影响。

•

MAN覆盖层的复杂性导致形式化约束的爆炸，严重影响了验证工具的可扩展性和性能。

为了解决上述挑战，我们的方法如下。

DeepGen。我们首先采用一个结构化的、基于JSON的配置规范（称为JSONet），以统一供应商特定的配置语法，并充分利用LLM处理结构化数据的能力。然后我们构建一个涵盖各种覆盖层配置场景的知识库。对于每个场景，我们提供一个相应的JSONet配置模板、一组参数约束和参数列表。当接收到用户意图时，DeepGen使用索引机制将意图与最合适的场景匹配。然后将配置模板输入LLM，参数约束指导LLM填充模板，从而实现准确的配置生成。

DeepValidator。与以往的工作类似，我们的方法将网络规则、配置和验证属性编码为数学约束，并使用SMT求解器进行验证。同时，我们引入专家知识来优化验证过程，并采用模块化和分层策略来提高效率和可扩展性。具体来说，我们将网络分解为多个逻辑模块（例如接口、IGP、BGP、VPN），并基于这些模块之间的功能依赖关系执行自下而上的验证路径。在BGP模块中，我们对对等会话进行细粒度分析；对于IGP路径计算，我们引入了一个带有策略约束的优化模型。这些设计选择显著减少了验证问题的规模并提高了其效率。

贡献总结来说，本文做出了以下关键贡献：

•

DeepConfig，一个基于意图的MAN覆盖层配置生成和验证框架。

•

DeepGen，一个通过提供特定领域知识库的正式约束和配置模板来指导LLM，从而减轻LLM幻觉并确保高保真合成的知识增强生成器。

•

DeepValidator，一个利用层次化依赖图（HDG）和混合SMT/仿真策略将MAN覆盖层控制平面验证分解为可管理的、逐跳子任务的可扩展验证器，有效避免了状态空间爆炸，同时确保了严格的策略合规性。

•

对DeepConfig框架的广泛评估表明，其生成精度超过90%（而基线方法的精度低于30%），在MAN覆盖层场景中的验证性能提高了100倍。

部分摘录

MAN覆盖层配置的复杂性

MAN覆盖层架构。在MAN覆盖层架构中，关键组件包括提供商边缘（PE）路由器、客户边缘（CE）设备和核心提供商（P）路由器。CE设备通常通过eBGP或OSPF等第3层路由协议与PE路由器连接，以与运营商网络交换路由信息。在运营商网络内部，PE和P路由器首先使用OSPF或IS-IS等IGP建立全网络范围的IP可达性，使PE能够建立BGP邻居关系

DeepConfig概述

本节提供了DeepConfig设计的概述。我们首先介绍我们的高级目标和构成我们方法基础的关键思想。然后讨论每个关键思想所解决的挑战以及我们的技术解决方案。最后，我们展示了这些组件是如何集成到一个连贯的工作流程中的。

DeepGen：基于知识的配置合成

DeepGen是DeepConfig的核心模块，负责配置合成。它使用统一的基于JSONet的配置表示将运营商意图映射为与供应商无关的网络配置，并利用专家知识库指导LLM进行基于约束的生成。专家知识库按MAN覆盖层场景组织；每个条目包含一个JSONet配置模板、一组参数约束和一层逻辑拓扑（底层、隧道和覆盖层）

设计概述

为了确保DeepGen生成的配置的正确性，在部署之前，DeepValidator作为核心验证阶段。鉴于MAN覆盖层的规模和复杂性，将整个控制平面作为一个整体进行验证在计算上是不可行的。为此，我们引入了一种两级优化策略，包括架构分解和模块内算法优化。

评估

我们使用Python和模块化架构实现了整个DeepConfig框架。DeepGen利用LlamaIndex（v0.14.8）来管理知识检索和上下文注入。DeepValidator由Z3定理证明器（v4.15.1）驱动进行约束求解。DeepTranslator实现为一个确定性的、基于模板的渲染器：与生成阶段不同，该模块完全通过编程操作，不涉及LLM。这种设计确保了验证结果的精确转换

结论

本文提出了DeepConfig框架，该框架显著提高了LLM生成复杂MAN覆盖层配置的准确性。此外，DeepConfig框架具有高度的可扩展性，能够无缝扩展到新的服务和支持额外的网络设备供应商。通过实验，我们验证了DeepConfig框架在多个LLM上的能力，证明了其在生成复杂MAN覆盖层配置任务中的有效性。

CRediT作者贡献声明

传林：撰写 – 审阅与编辑，撰写 – 原始草稿，可视化，验证，软件，方法论，调查，形式分析，数据策划，概念化。朱龙龙：撰写 – 审阅与编辑。刘洪燕：撰写 – 审阅与编辑。张东：撰写 – 审阅与编辑。余嘉硕：撰写 – 审阅与编辑。廖丽达：撰写 – 审阅与编辑。

利益冲突声明

作者声明以下可能被视为潜在利益冲突的财务利益/个人关系：

朱龙龙报告称获得了浙江大学的写作协助。如果有其他作者，他们声明没有已知的财务利益或个人关系可能影响本文报告的工作。

传林于2008年在中国福州大学获得了计算机科学与技术硕士学位。他之前在瑞杰网络公司工作。他目前正在中国福州大学攻读博士学位。他的研究兴趣包括网络形式化验证和用于网络的大型语言模型。