形式验证证书的循环一致性神经解释

# 形式验证证书的循环一致神经解释 来源：https://arxiv.org/html/2606.24414 ###### 摘要 形式验证会产生机器可核查的证书，证明时序属性的满足或违反，但这些证书对于非专业利益相关者来说仍然晦涩难懂。我们提出了一种循环一致的神经架构，能够生成验证证书的忠实自然语言解释。前向网络NN1将证书映射为解释，逆向网络NN2从解释重建证书；符号验证器构成闭环，提供可微分的忠实度代理。指针生成机制通过直接从证书中复制状态名称来确保词汇基础。我们在420个测试证书上进行评估，这些证书涵盖六种验证方法（有界证明、k归纳、归纳不变量、拉索、可达性、见证对），包括YES和NO两种裁决变体，来自一个包含207个命名状态的金融合规领域。我们的训练架构结合混合推理时路由策略，实现了90.0%的循环验证可靠性——超越了多LLM少样本基线（四种前沿模型的16种LLM组合中最佳为76.1%）13.9个百分点。神经模型在12个裁决/类型类别中赢得了10个，其中三个类别达到100%的可靠性。该架构提供约860倍的推理速度（每个证书约185毫秒，而完整的多LLM基线约160秒），支持离线运行、确定性输出，且每次推理成本为零。这些结果表明，针对结构化证书解释，经过专业训练的小模型优于通用LLM提示方法，同时消除了基于云推理的部署限制。 ## 1 引言 形式验证会产生机器可核查的证书[11,24,6]——套索形状的反例、可达性见证、归纳不变量、有界证明——为系统行为提供数学保证。在金融合规等受监管领域，这些证书是监管保证的证据基础，但对于必须据此采取行动的审计师和合规官员来说，它们仍然晦涩难懂。生成同时保持忠实（无幻觉事实）和流畅（非专业人员可理解）的自然语言解释是一项开放挑战：现有的神经方法优先考虑流畅性而牺牲了基础性，而模板系统则僵化且特定于领域。我们观察到，忠实度有一个可测试的表述：证书C的解释E是忠实的，当且仅当仅凭E就能重建C。这激发了一种循环一致架构：前向指针生成网络NN1将C映射为E，直接从证书中复制状态名称以消除实体幻觉；逆向Transformer NN2将E重建为C′；符号验证器比较C与C′，通过替代重建损失（第3.2节）提供可微分的忠实度代理，无需人工标注。此外，混合推理时路由器根据示例选择多种解码配置，利用证书类型之间的结构差异。我们在来自金融合规工作流的12个裁决/类型类别的420个测试证书上进行评估。混合路由器实现了90.0%的循环验证可靠性——这是真实忠实度的下限，因为NN2的3.6%假阴性率意味着一些真正忠实的解释会被保守地标记。这超越了最佳的前沿LLM对配置（76.1%）13.9个百分点（95%置信区间不重叠），在12个类别中赢得10个，其中三个达到100%且无失败。这个参数低于1M的模型离线运行，延迟降低约860倍，具有确定性输出、零每次推理成本，且不会将数据暴露给外部服务——这些属性对受监管行业至关重要。我们的贡献： 1. 1. 循环一致解释。一种神经架构，结合了指针生成前向模型、逆向Transformer和符号验证器，通过循环一致性强制执行忠实度，无需人工标注（第3节）。 2. 2. 混合推理时路由。一种测试时策略，实现90.0%的可靠性，而最佳单一配置为61.7%，无需额外训练（第4.3节）。 3. 3. 超越LLM提示。一个参数低于1M的模型在循环验证可靠性上超越了16种前沿LLM配置（90.0% vs. 76.1%），证明当忠实度标准可形式验证时，经过专业训练的小模型优于通用提示方法（第4.4节）。 4. 4. 可投入部署的架构。离线运行、确定性输出、零边际成本、无数据暴露——具有固定的计算图，缺少提示注入攻击可利用的自由文本输入通道（第4节）。 ## 2 相关工作 我们的方法处于四个研究领域的交叉点，我们逐一讨论，然后将我们的贡献与先前工作进行定位（表1）。 #### 循环一致学习。循环一致性作为训练目标因CycleGAN而流行，用于无配对图像到图像翻译，强制映射G:X→Y与其逆映射F:Y→X的组合接近恒等映射。在自然语言处理中，反向翻译应用了类似原理：将句子翻译成中间语言再翻译回来，然后惩罚与原句的差异。后续工作将循环一致性扩展到风格迁移、数据增强和无监督机器翻译。我们的工作有一个根本区别：循环遍历两种不同模态——结构化符号证书和自然语言文本——而不是同一模态的两个实例（例如两个图像域或两种语言）。此外，循环终点的忠实度标准不是近似重建，而是符号语义等价，由形式验证器评估状态集、路径结构和成员关系。 #### LLM奖励信号与评判。使用大语言模型提供训练时信号通过RLAIF、LLM-as-Judge和Constitutional AI等方法获得了关注。在这些框架中，LLM通常评判整体质量——一个单一信号混合了正确性、流畅性、帮助性和安全性。我们的架构引入了一个关键分离：LLM仅评判流畅性，而忠实度由完全独立的机制（具有符号验证的循环一致性）强制执行，确保流畅性优化不会引入幻觉。我们的混合路由器也与测试时计算扩展有关，其中生成并重排序多个候选者可以提高输出质量；我们的不同之处在于，重排序的裁判是精确的符号验证器，而不是学习到的奖励模型，并且参数低于1M的模型使得对每个证书评估数十个候选者在计算上微不足道。 #### 从结构化数据生成神经文本。数据到文本生成将结构化输入映射为自然语言。早期的神经方法使用带注意力的序列到序列模型，后来增加了复制机制。最近的工作包括结构化数据口头化、使用预训练模型的表格到文本生成，以及基于知识的生成。我们将指针生成网络应用于证书到解释的生成；我们的设置特点是形式可验证的忠实度，以及一个小型训练模型超越LLM少样本提示（90.0% vs. 76.1%）。另一条并行的工作线事后测量生成忠实度，使用学习到的代理：基于蕴含的事实一致性分类器、基于问答的一致性指标，以及Ji等人调查的更广泛幻觉分类。这些指标使用训练或提示的打分器近似忠实度，因此自身存在误差。我们的标准根本不同：忠实度不是估计，而是精确验证，因为符号验证器检查原始证书与重建证书之间的集合和序列级别等价。这种精确性之所以可能，只是因为证书是具有明确定义事实集的结构化对象。 #### 形式验证中的可解释性。反例解释已通过模拟、抽象细化追踪和故障定位来解决。一般来说，基于模板的系统天生忠实但根本上不灵活——每种新的证书类型或领域都需要手动模板创作。我们的神经方法通过学习生成来解决这些限制，同时通过循环一致性而不是模板僵化来维持忠实度强制执行。在反应系统的最新工作中，通过溯因形式推理生成具有形式保证的反应神经网络解释，并生成简单的反例（类似于我们使用的轨迹）来评估系统不可实现。这两种方法都不产生其形式化通过循环一致架构双重检查的自然语言解释。 #### 神经符号与验证器在环生成。越来越多的研究将神经生成器与符号或程序化检查器耦合，以约束或验证输出，涵盖验证器引导解码、工具和检查器增强生成，以及神经符号NLG——对生成文本强制执行逻辑约束。一个密切相关但相反的任务是自动形式化，将自然语言映射为形式语句——例如，将非正式数学或规范翻译成证明助手或时序逻辑。我们的前向任务是相反方向：我们进行去形式化，将形式证书映射为自然语言。联系在于，我们的逆向网络NN2执行一种受限的、特定领域的自动形式化（解释→证书），因此整个循环组合了口头化与再形式化，并经过符号验证器。然而，与自动形式化系统不同，这里的忠实度不是单一NL→形式翻译的正确性，而是原始证书与重建证书的往返等价。更广泛地说，我们的架构在强意义上是验证器在环：符号验证器不仅是事后过滤器，而是闭合可微训练循环，并且在推理时作为路由选择裁判。与检查器验证表面形式的系统不同，我们的验证器评估重建证书的语义等价性，使忠实度成为架构优化的属性，而不是事后审计的属性。 #### 定位。新颖性不在于任何单一组件，而在于它们在一个忠实度可形式验证的领域中的原则性集成。流畅性与忠实度的分离提供了先前神经解释系统所没有的结构属性：忠实度约束由符号验证器强制执行，而不是由学习或提示模型执行。表1总结了我们的方法在忠实度、流畅性、监督需求和形式基础维度上与先前工作的比较。 表1：与相关方法的比较。我们的工作独特地结合了循环一致忠实度、LLM流畅性评分和指针生成复制，用于形式验证证书。 ## 3 方法 我们提出了一种循环一致神经架构，用于生成形式验证证书的自然语言解释。该系统包括两个联合训练的神经网络、一个符号验证器和一种混合推理时路由策略（图1）。 ### 3.1 问题形式化 令C表示验证证书空间，E表示自然语言解释空间。证书C∈C是一个结构化对象，包含裁决（YES/NO）、类型（可达性、套索、见证对、归纳不变量、有界证明、k归纳）以及类型特定内容（状态序列、路径结构、不变集）。解释E∈E是一个描述证书含义的自然语言句子或段落。底层时序属性使用标准逻辑如LTL和CTL指定；我们的方法处理结果证书，并与源逻辑无关。我们寻求一个映射f:C→E，产生满足两个属性的解释： - • 可靠性（无幻觉）。E中的每个事实主张都有C支持。如果解释提到状态s，则s必须出现在证书中。如果声称存在路径，则该路径必须存在于C中。可靠性是一个硬约束：任何违反都构成可能误导人类决策者的幻觉。 - • 流畅性。解释读起来像自然英语，能让非形式方法专家的领域专家理解。 我们还定义了一个期望但依赖证书类型的属性： - • 完整性（覆盖）。解释提及了证书关键内容的足够比例。与可靠性不同，完整性不是二值正确性标准，而是一种编辑质量：适当的完整程度因证书类型和预期受众而异。穷举列表的