用大语言模型合成正确的路由配置需要什么？

本文研究了大型语言模型（例如 GPT-4）是否能够在减少人工工作量的情况下合成正确的路由器配置。作者团队发现单独的 GPT-4 表现非常糟糕，它可以生成有一定可行性的粗略配置，但在拓扑、语法和语义方面存在严重错误。本文提出的策略，称为“验证提示编程（Verified Prompt Programming）”，是将 GPT-4 与验证器结合使用，并利用验证器的局部反馈来自动纠错。本文展示了两个用例的结果：在单个路由器上将 Cisco 配置翻译为 Juniper 配置，以及在多个路由器上实施非过境策略。虽然仍然需要人工输入，但如果我们将 leverage 定义为自动提示数量与人工提示数量的比例，本文的实验结果显示在 Juniper 翻译方面有 10 倍的 leverage，而在实施非过境策略方面有 6 倍的 leverage，最终得到已验证的配置。

来源：HotNets ’23
题目：What do LLMs need to Synthesize Correct Router Configurations
作者：Rajdeep Mondal, Alan Tang,Ryan Beckett,Todd Millstein,George Varghese
原文链接：https://conferences.sigcomm.org/hotnets/2023/papers/hotnets23_mondal.pdf
内容整理：李雨航

引言

本文试图探讨 LLMs 在一个不同领域进行代码生成的能力，具体到文中是指 GPT-4 是否能够编写由人类传统编写的路由器配置文件。这些文件有助于调整路由和转发决策，对网络运营至关重要。我们在合成配置之外的更进一步目标是看看 LLMs 是否可以与其他程序（通过 API）融合，以模拟一个可以理解程序语义的 LLM。

引入语义的一种可行方法是将 LLM 与自动验证器（例如 SAT 求解器或模型检查器）配对。但使用了验证器并不能高枕无忧。首先，验证器无法在没有规范的情况下证明正确性。在实践中，规范是不完整的，因此并非所有解决方案都可接受。其次，为了使验证器能够自动（最小人工干预地）与 LLM 交互，验证器必须提供可行的反馈。本文发现 LLM 使用来自网络组件的模块化验证器（单个路由器甚至是路由器内的路由映射）的反馈更容易自我纠正，而不是整个网络的反馈。

图1显示了配对编程（PP）的传统方法，体现在 GitHub CoPilot 等系统中，即人类和人工智能共同编写程序。在配对编程中，人工智能和人类形成一个元组（A，H），人类 H 手动检查人工智能 A 的输出的正确性，然后手动向 A 发出校正提示，如图所示。这种手动初始提示和随后的手动校正通常称为提示工程。

图 2 显示了本文的替代愿景。在本文称之为验证提示编程（Verified Prompt Programming，VPP）的系统中，人工智能、人类和验证器 V 形成一个三元组（A，H，V）。验证器检查正确性并自动发出校正指令。V 在一定数量的尝试后可能放弃自动更正，人类仍然必须手动更正。此处，我们的假设是随着输出越来越接近正确的程序，人类工作量会减少。

请注意，在 V 和 A 之间有一个快速的内循环，其中验证器的结果自动反馈给 GPT-4。由于验证器的反馈通常难以理解，我们使用一个简单的称为“人性化器”的程序，将反馈转换为 GPT-4 能理解的自然语言提示。当 V 确定最终配置是正确的或者经过一定时间后，V 的输出将作为慢速手动循环的一部分发送回用户。本文检验了“工作量减少假设”：图 2 中手动循环中的工作量显著少于图 1 中的手动工作量。

为了量化减少的工作量，我们引入了一个简单的度量。定义 leverage 为图 2 中自动提示数量与人工提示数量的比率 L 。leverage 在保持语言模型 A 和人类 H 不变的情况下，衡量验证器的效果，即从（A，H）到（A，V，H）的潜在改进。

系统组织

图 3 是图 2 更一般的 VPP 愿景的一个细化版本，本文称之为 COSYNTH。本文强调他们并未构建 COSYNTH。因为虽然他们使用了 GPT-4，但无法访问其 API，只能通过手动模拟 API 调用并使用提示来与 ChatGPT 进行交互。本文的目标不是展示一个可运行的系统，而是探索 GPT-4 在配置撰写方面的能力。

图 3 中显示的验证器组至少包括两个验证器，一个语法验证器（本文使用了 Batfish）和一个语义验证器（根据用例的不同，本文使用了不同的语义验证器）。对于第二个用例，使用了第三个验证器，拓扑验证器（用 Python 编写），因为我们发现 GPT-4 有时会遗漏向相邻节点告知路由。用户提供了上下文（拓扑、路由器、接口）和所需任务的精确自然语言描述（例如 Cisco 配置和将其翻译为 Juniper 的请求）。GPT-4 的输出首先经过 Batfish 检查语法错误。COSYNTH 向 GPT-4 发送有关错误行的反馈，以自然语言“人性化”（请参阅表 1 中的示例）。图 3 中标有H的方框对应图 2 中的人性化器，它充当错误解析器和自然语言转换器。

如果所有语法错误都得到纠正，则输出传递给语义验证器，而如果发生太多语法纠正尝试，COSYNTH 将会把任务交给人类处理。对于本文的第一个用例，本文使用 Campion 作为验证器。对于本文的第二个用例，本文使用 Batfish 的符号路由映射分析作为验证器，要求其验证共同确保所需全局策略的本地策略，语义验证器的反馈在“人性化”处理后被传递回 GPT-4。

当 COSYNTH 与多个路由器一起工作时，本文使用了另一个称为“模块化器”的模块（图 3）。对于网络配置，我们的想法是从精确的机器可读描述（我们使用 JSON）开始，描述“模块”，在本文的情况下是拓扑和连接。模块化器输出一系列自然语言提示，将拓扑描述给 GPT-4（例如，Router 𝑅1 通过接口 𝐼1 连接到 Router 𝑅2 上的接口 𝐼2）。

实验

Cisco 到 Juniper 的翻译

本文使用 VPP 将 Cisco 配置翻译成等效的 Juniper 配置。使用 Batfish 来识别语法错误。使用 Campion 来检测和定位用于完善结果的语义差异。

实验方法

首先，本文提供 Cisco 配置和提示：“将配置翻译成等效的 Juniper 配置”。GPT-4 将产生一个翻译成 Junos 格式的翻译，通常包含几个错误和差异。然后，我们尝试迭代地纠正这些错误，使用来自验证器的“人性化”反馈。我们在每次迭代中重新验证整个配置。在本文的实验中，我们专注于与路由和转发相关的行为。

为了设计人性化器，本文区分了四类配置错误：

1.语法错误：Batfish 生成解析警告，标识不使用有效 Juniper 语法的相关行。

2.结构不匹配/冲突：当原始配置中存在但在翻译中不存在（或在翻译中存在但在原始配置中不存在）的组件、连接或命名策略时。

3.属性差异：这是两个配置之间的数字属性具有不同值的情况。

4.策略行为差异：当路由映射或访问控制列表存在语义差异时，就会发生这种情况。

对错误进行区分有两个原因。首先，语法错误和结构不匹配必须在早期处理，因为它们可能掩盖属性差异和策略行为差异。其次，不同类型的错误需要不同的人性化提示，而相同类型的错误可以重用类似的提示。每种类型的错误都可以用一个公式提示进行总结，根据 Batfish 或 Campion 报告的错误插入一些字段。

表 1 显示了生成的提示的公式和示例。Batfish 的解析错误和警告可以重复用作语法错误的提示。从相关组件和属性轻松生成结构不匹配和属性差异的提示。策略行为差异更难处理，因为不总是清楚如何描述受影响的输入空间，这些输入空间被不同地处理。本文选择采用给出一个具体示例的方法。

实验结果

本文尝试将一份来自 Batfish 示例的 Cisco 配置翻译成 Juniper 格式。这个配置足够短，可以适应 GPT-4 文本输入的限制，但使用了包括 BGP、OSPF、前缀列表和路由映射在内的非平凡特性。进展并非单调：GPT-4 可以修复一个错误，但可能引入之前不存在的新错误。有时甚至会重新引入之前修复过的错误！然而，最终我们成功完成了翻译任务，采用了自动和手动提示的组合。

leverage：在一次此类测试运行中，整个提示循环包括 2 个人工提示和 20 个自动提示， leverage 为 10 倍。这 20 个自动提示纠正周期中，包括在纠正语义错误后不仅在开始时而且在整个过程中进行的用于语法纠正的小周期。需要明确的是，本文通过手动将自动生成的提示提供给 GPT-4 来“模拟”每个 API 调用。

表 2 显示了翻译中出现的错误以及 GPT-4 是否能够使用自动生成的提示修复这些错误，具体来说：

缺少 BGP local-as 属性：翻译的 BGP 邻居声明中没有包含本地 AS 属性。我们将其标记为语法错误，因为它产生了解析警告。
缺少/多余的 BGP 路由策略：一个配置中仅为 BGP 邻居使用导入或导出策略。
不同的 OSPF 链路属性：OSPF 链路具有多个属性，而翻译有时包含链接成本或被动接口设置的差异。
设置错误的 BGP MED 值：一个 BGP 路由策略的翻译没有更新 BGP MED 值。这是由于在将原始 Cisco 配置的一个 route map 子句翻译时出现的错误引起的。
进入 BGP 的不同重分发行为：Cisco 和 Juniper 格式以不同的方式处理进入 BGP 的路由重分发。Juniper 通常使用控制导入和导出 BGP 路由的相同路由策略来执行此操作，而 Cisco 配置为为路由重分发设置单独的 route map。在本文的情况下，Campion 检测到 Juniper 配置正在重新分发一些 Cisco 配置未重新分发的路由。这可以通过在策略的多个位置添加“from bgp”条件来修复。与前述错误不同，当给出自动生成的提示时，GPT-4 无法修复此问题。相反，当直接要求它向路由策略添加“from bgp”条件时，它可以解决该问题。
BGP 前缀列表问题：在翻译前缀列表时，出现了另一个微妙的问题。原始的 Cisco 配置包含以下前缀列表：ip prefix-list our-networks seq 5 permit 1.2.3.0/24 ge 24值得注意的部分是“ge 24”，它表示匹配长度为 24 或更长的前缀。在Juniper 中没有这种语法的等效部分，但对于本文的用例，Juniper 有至少两种方法可以使用不同的语法获得类似的行为。当 GPT-4 被要求翻译配置时，它通常会省略“ge 24”部分，因此在翻译中匹配的前缀空间将有所不同。当要求纠正此问题时，它有时会生成具有不正确语法的配置。例如，它可能输出以下内容：prefix-list our-networks { 1.2.3.0/24-32; }而这不是有效的 Juniper 语法。

利用局部合成全局策略

本文使用 GPT-4 基于每个路由器的本地策略生成给定网络拓扑的路由器配置，该方法通过验证本地不变性进行控制平面验证。

为了确保语义正确性，这里采用两个新模块。第一个是“拓扑”验证器，用于检查特定路由器的配置是否符合定义的拓扑。它检查 GPT-4 是否正确设置所有接口，声明 BGP 邻居并正确声明网络。其次，本文运行 Batfish 来检查在提示中定义的本地策略；输出结果用于优化结果。

实验方法

我们首先在初始提示中使用几句话向 GPT 说明任务，目标是使网络遵循无过境策略，在该策略下，没有两个 ISP 能够相互到达。然而，所有 ISP 都能够到达 CUSTOMER，反之亦然。

编写拓扑的自然语言描述是一项容易出现人为错误的任务。我们编写了一个自动化脚本，根据输入的拓扑生成文本。在本文的实验中，我们讨论星形网络，其中一个路由器连接到一个 CUSTOMER IP，而其他路由器连接到不同的 ISP（图 4）。所有ISP路由器都直接连接到第一个路由器。因此，“网络生成器”只需要输入路由器的数量。它有两个输出：1）文本描述和 2）整个网络拓扑的 JSON 字典。文本描述用作提示，而 JSON 字典稍后用于检查生成的配置是否与拓扑匹配。

本地策略提示 vs 全局策略提示：本文尝试一次性向 GPT-4 指定全局无过境策略。GPT-4 生成了两种创新策略：使用 AS 路径正则表达式过滤路由，并阻止从客户路由器向其他路由器广告 ISP 前缀。不幸的是，我们在纠正拓扑和语法错误后发现，当我们以反例数据包的形式提供反馈（就像“全局”网络验证器 Minesweeper 会提供的方式），GPT-4 感到困惑，不断在不正确的策略之间摆动。本文发现指定本地策略会带来更好的结果，因为它允许我们将验证错误局限于特定路由器和这些路由器中的特定路由映射。

我们要求 GPT-4 使用新提示为每个路由器生成配置，每次指定每个路由器的本地策略。具体来说，策略是 𝑅1 应在进入每个 ISP 时添加一个特定的社区，然后在离开每个 ISP 时基于这些社区删除路由。生成的错误可分为三类：

1. 语法错误：GPT-4 生成具有无效 Cisco 语法的配置。Batfish 生成的解析警告识别这些错误。

2. 拓扑错误：GPT-4 错误地声明或忽略了一些 BGP 邻居或遗漏了声明某些网络。对于这一点，本文使用一个自动化的“拓扑验证器”，其主要目的是系统地解析配置中的所有以太网接口、BGP 邻居和网络声明，并将其与 JSON 字典中列出的网络架构进行匹配。然后，它指出所有缺失的声明和拓扑上的不一致性。

3. 语义错误/策略错误：GPT-4 生成的配置不符合预期的本地策略。本文在此步骤中使用 Batfish 的“搜索路由策略”进行验证。如果存在语义错误，Batfish 将生成一个未遵循本地策略的示例。然后，在新的提示中将此示例提供给 GPT-4。

将其分类为不同的类别使我们能够使用不同的工具来解决每个类别。表 3 列出了纠正提示的示例。一旦所有错误都得到纠正，我们就使用 Batfish 作为最后一步来模拟整个 BGP 通信，以确保满足全局策略。

实验结果

由于某些 GPT-4 错误更为常见，我们提供了一个初始指令提示（IIP，初始指令提示）如下：

CLI 提示：GPT-4 经常生成要输入 Cisco 命令行界面的命令，这是不可取的。因此，我们明确要求它生成 .cfg 文件。
错误关键词：在生成配置时，它经常使用诸如 ‘exit’、’end’、’configure terminal’、 ‘ip routing’、 ‘write’、 ‘hostname’ 和 ‘conf t’ 等关键词，有时放置在错误的位置。因此，我们指示它不要使用这些关键词。
匹配社区：GPT-4 有时尝试直接匹配社区值，这是不正确的。相反，必须声明包含社区值的社区列表，并且路由映射应该在社区列表上匹配。因此，我们添加了另一个 IIP，告诉 GPT-4 定义和匹配社区列表。
添加社区：当要求使用路由映射向路由添加社区时，GPT-4 生成类似以下语法：route-map ADD_COMMUNITY permit 10 set community 100:1上述路由映射错误地用社区 100:1 替换了路由中的所有现有社区。因此，我们添加了一个初始提示，要求它在向路由添加社区时始终使用 “additive” 关键词。

这些初始提示以及表 3 的语法纠正方案能够消除 GPT-4 产生的常见语法错误。尽管如此，我们还是发现了两个需要人工干预的严重情况：

将邻居命令放在错误的位置：在 BGP 的配置文件中，所有邻居命令（将路由映射附加到接口的命令）必须放在 “router bgp” 块下。有时 GPT-4 定义一个路由映射，然后将其与 “router bgp” 块之外的接口关联起来。Batfish 可以捕捉此语法错误，但输出对于 GPT-4 来说不够信息丰富，无法修复该问题。
在 match 语句中的 AND/OR 语义：对于 no-transit，我们要求 GPT-4 生成一个针对 𝑅1 的配置，将特定社区添加到从 𝑅2 进入的每个路由，以及类似地针对 𝑅1 的其他邻居（图 4）。我们还要求它在连接 𝑅1 到 𝑅2 − 𝑅6 的接口的 egress 上过滤包含任何此类社区的路由。GPT-4 在 ingress 处添加了正确的社区，但在 egress 处错误地使用了 AND 语义来过滤路由，如下所示，对于 𝑅1 − 𝑅2 接口的路由映射：

route-map FILTER_COMM_OUT_R2 deny 10
match community 3
match community 4
match community 5
match community 6
route-map FILTER_COMM_OUT_R2 permit 20*

社区列表 3 与从 R3 进入的路由关联，社区列表 4 与从 R4 进入的路由关联，依此类推。我们希望从 𝑅3 − 𝑅6 进入的路由在连接到 𝑅2 的 egress 处被过滤掉。上述配置将仅过滤具有所有四个社区的路由。当我们询问 Batfish 上述路由映射是否过滤与社区列表 3 匹配的所有路由时，它生成了一个反例，但这并没有纠正问题。相反，需要人工提示要求 GPT-4 在单独的路由映射段中声明每个 match 语句。

leverage：在这样的运行中，整个周期需要 2 个人工提示和 12 个自动提示，leverage为 6X。