🤖 machine learning

SMT-Based Active Learning of Weighted Automata

本文提出了一种针对非确定性加权自动机的基于SMT的参数化主动学习算法，该算法保证生成最小结果，确保在半环有限时终止，并在大量实验中展现出优于现有方法的效率和紧凑性。

原作者： Tiago Ferreira, Kevin Batz, Alexandra Silva

发布于 2026-05-11

📖 1 分钟阅读☕ 轻松阅读

原作者： Tiago Ferreira, Kevin Batz, Alexandra Silva

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在教一个机器人如何穿越迷宫，但你并不知道迷宫的布局。你可以向机器人提出两种类型的问题：

“如果我走这条路会发生什么？”（机器人会告诉你结果，例如“我卡住了”或“我找到了价值 5 枚金币的宝藏”。）
“你画的这张地图正确吗？”（机器人会将你的地图与真实迷宫进行比对，并回答“是”或“不，你在这里漏掉了一个转弯”。）

这就是主动学习的核心思想：一种通过向“教师”（即真实系统）提出智能问题来学习模型的算法。

长期以来，这些学习算法在简单的“是/否”迷宫（例如：这扇门是开着的还是关着的？）中表现优异。但现实世界的系统往往更为复杂。它们涉及权重：成本、概率或时间。例如，“到达出口的最便宜路径是什么？”或“发生碰撞的概率是多少？”

本文介绍了一种新颖且强大的方法，用于教会计算机学习这些加权自动机（即路径上附有数字的迷宫）。

旧方法：“表格”法

此前，研究人员使用一种基于巨型表格（称为汉克尔矩阵）的方法。想象一下，试图通过填写一张巨大的电子表格来解谜，其中每个单元格的值都依赖于复杂的代数规则。

问题所在： 当数字不仅仅是简单的整数时，这种电子表格方法会变得非常混乱且难以求解。它往往无法找到最简的地图，或者在试图证明能够完成任务时陷入僵局。这就像试图通过在纸上写下每一步可能的移动来解决魔方；对于小魔方或许可行，但对于大魔方则变得不可能。

新方法："SMT"法

作者提出了一种不同的方法：约束求解。他们不再填写电子表格，而是将学习问题转化为一个巨大的逻辑谜题。

类比：侦探与 SMT 求解器
想象你是一名侦探，试图根据目击者的证词（即教师的回答）来重构犯罪现场（迷宫）。

假设： 你猜测一名嫌疑人和一个时间线（一个包含少量状态的小地图）。
约束： 你列出一系列规则：“如果嫌疑人在银行，他们必须在下午 5 点前离开”，或者“被盗总金额必须等于 100 美元”。
SMT 求解器： 这是一个超级聪明的计算机程序（就像一个逻辑引擎），用于检查你的规则是否合理。它会问：“是否存在任何一种安排嫌疑人移动的方式，使得所有这些规则同时成立？”
- 如果是：求解器会给你一个有效的地图。
- 如果否：它会告诉你你的地图是不可能的。

本文的算法工作流程如下：

它从一个微小、简单的地图开始。
它向教师询问特定路径的答案。
它将这些答案作为一组数学规则输入到SMT 求解器中。
求解器尝试寻找一个符合所有规则的地图。
如果教师说：“不，那张地图是错的，因为它在某个特定路径上失败了”，算法就会将该路径添加到规则中，并让求解器再次尝试。

为什么这更好？

本文声称有三个主要优势，简单解释如下：

1. 它总能找到最小的地图（最小性）
旧方法有时会给出一个拥有 10 个房间的地图，而实际上 3 个房间的地图就足够了。新的 SMT 方法旨在找到符合规则的最小可能地图。这就像寻找最高效的路线，而不仅仅是一条路线。

2. 它能处理“怪异”的数学
旧方法在处理复杂的数系（例如“热带”数学，其中你相加数字但取最小值，或“瓶颈”数学）时显得力不从心。新方法可以通过将这些“怪异”的数学系统转化为计算机求解器能理解的逻辑谜题来处理它们。这就像拥有一个万能翻译器，能将复杂的数学转化为简单的“真/假”问题。

3. 它更快且需要更少的问题
在实验中，新方法学习复杂地图的速度远快于旧的“表格”方法。它还需要向教师提出更少的问题才能获得正确答案。

“朴素”基线： 他们将这种方法与一种只是随机猜测的“愚蠢”版本进行了比较。新方法的表现 vastly superior（远超）。
“最先进”竞争对手： 他们将其与现有的最佳方法进行了比较。新方法生成的地图显著更小（有时小 10 倍！），并且仍然能在合理的时间内完成。

“魔法”成分：SMT 求解器

秘诀在于SMT 求解（模理论可满足性）。将 SMT 求解器想象成一个超级强大的逻辑检查器。它不仅仅检查一个句子是否为真，而是检查一组复杂的数学规则是否能同时为真。

作者证明了对于许多类型的数学系统（包括有限系统和某些无限系统），这个逻辑谜题是可解的。
他们表明，如果数学系统是有限的（例如有限的一组数字），该算法保证会终止。

总结

本文提出了一种新方法，用于教会计算机理解复杂的加权系统。他们不再使用旧式、笨拙的电子表格方法，而是将问题转化为一个现代计算机求解器可以破解的逻辑谜题。

结果： 它找到了最简单的可能模型。
结果： 它适用于比以往更广泛的数学系统。
结果： 它比以前的方法更快，且提出的问题更少。

作者在数千个示例上测试了该方法，发现它是学习这些复杂系统的稳健且实用的工具，为过去十年使用的方法提供了一个强有力的替代方案。

技术摘要：基于 SMT 的加权自动机主动学习

问题陈述

主动自动机学习由 Angluin 的 $L^\star$ 算法开创，已成为形式化验证中推断未知组件模型的标准技术。虽然 $L^\star$ 风格的方法在布尔自动机（确定性和非确定性）方面已相当成熟，但将其扩展到加权有限自动机（WFAs）却 proved 显著更具挑战性。WFAs 通过将来自半环的权重分配给转移，对布尔自动机进行了推广，从而能够对成本、概率和资源消耗等定量属性进行建模。

现有的 WFAs 学习方法依赖于 Hankel 矩阵或观察表的推广（例如 $WL^\star$ ）。这些方法需要对底层半环的代数结构进行推理。因此，证明终止性和最小性十分微妙，且通常仅限于特定的代数类（例如域、主理想整环）。对于许多实际相关的半环，如 Tropical 半环或 Bottleneck 半环，终止性保证要么未知，要么无法确保生成最小自动机。此外，现有算法往往产生非最小模型，或在无限半环上无法有效扩展。

方法论

作者提出了一种新颖的基于约束的主动学习算法，将学习问题直接表述为可由SMT（可满足性模理论）求解器解决的满足性问题。

核心方法

该算法不是细化观察表，而是增量地构建给定半环 $S$ 上的方程组。该方程组的解恰好对应于在所有观测查询上与“教师”（目标语言）一致的非确定性 WFAs。

学习过程遵循标准的主动学习循环（算法 1）：

假设生成：算法尝试找到一个与当前观测集 $O$ 一致的 $n$ 状态 WFA。这被委托给子程序 getAutomaton 处理。
等价性查询：如果找到一致假设 $H$ ，则向教师查询以验证 $H$ 是否识别目标语言 $L$ 。
反例处理：如果教师提供反例 $w$ （其中 $H(w) \neq L(w)$ ），则将 $w$ 添加到 $O$ 中，并在约束加强的情况下重复循环。

`getAutomaton` 子程序

论文提出了 getAutomaton 的两种实现：

朴素基线：直接编码 WFA 的语义。它将初始权重、转移矩阵和最终权重视为未知变量，并针对所有 $w \in O$ 求解方程 $out(w) = \text{semantics}(w)$ 。
优化版（SWAL）：利用余代数视角和状态语言的概念。它不是直接求解全局语言，而是引入代表从每个状态接受的语言的中间变量。这产生了一个方程组，其中：
- 稳定化约束确保状态语言与转移权重一致。
- 张成约束确保初始权重正确组合状态语言以匹配目标输出。
- 关键洞察：虽然这种编码引入了更多的变量和方程，但它揭示了观测值之间的共享子结构（后缀）。这使得 SMT 求解器能够重用中间结果，与朴素方法相比显著提高了可扩展性。

可判定性与半环

该算法在半环上是参数化的。作者指出，对于可判定半环（其中有限方程组的可满足性是可判定的），getAutomaton 子程序可以被正确且完全地实现。

有限半环：可通过暴力搜索或 SMT 显然地判定。
无限半环：论文提供了将Tropical 半环（ $\min, +$ ）、有界 Tropical 半环和Bottleneck 半环（ $\max, \min$ ）编码到可判定理论（如无量词线性整数算术 QF-LIA 和无量词位向量 QF-BV）的方法。

主要贡献

新颖算法：提出了一种新的基于 SMT 的非确定性 WFA 主动学习算法，该算法在半环上是参数化的。
最小性保证：与通常缺乏特定代数结构之外最小性保证的 $L^\star$ 风格方法不同，该算法保证在终止时生成最小 WFAs，无论半环如何。
终止条件：作者证明了部分正确性并提供了终止的充分条件。具体而言，他们证明了该算法对于所有有限半环均终止。对于无限半环，虽然相同的基数论证无法在理论上保证终止，但实现展示了实际的成功。
基于约束的合成：论文引入了首个 WFAs 的基于约束的生成算法，实现了基于 SMT 的合成。它确定了结果约束系统可判定的特定半环。
实验评估：对提出的方法（SWAL）与朴素基线及最先进的 $WL^\star$ 算法进行了全面的比较评估。

实验结果

作者在 OCaml 中利用 Z3 求解器实现了该算法（SWAL），并在布尔、Tropical、有界 Tropical 和 Bottleneck 半环上对超过 5,000 个随机生成的基准测试进行了评估。

与朴素基线对比：SWAL 在运行时间和可扩展性方面均显著优于朴素编码。虽然朴素方法难以学习超过 2–6 个状态的自动机（取决于半环），但 SWAL 成功学习了多达 8 个状态的最小自动机。优化编码（状态语言）将超时/内存溢出错误减少了数个数量级。
与 $WL^\star$ 对比：与 $WL^\star$ $W L^{⋆}$ （主理想整环的最先进算法）相比：
- 最小性：SWAL 始终生成最小自动机，而 $WL^\star$ 生成的自动机往往大 10 倍。
- 效率：SWAL 需要的输出查询次数（与教师的交互）少于 $WL^\star$ 。
- 运行时间：SWAL 在运行时间上具有竞争力，通常比 $WL^\star$ 更快终止，且资源失败（超时/内存溢出）更少。
增量性：启用增量 SMT 求解大幅减少了学习时间和资源使用，证实了基于约束的方法适用于增量学习。

意义与主张

该论文将基于约束的学习定位为传统 Hankel/ $L^\star$ 风格加权自动机方法的实用且稳健的替代方案，特别是在面向验证的设定中。

稳健性：该方法处理了更广泛的半环（包括像 Tropical 这样的无限半环），而在这些半环上， $L^\star$ 风格方法的代数终止证明往往困难或根本不存在。
最小性：最小性保证是一个关键优势，因为最小模型对于高效验证和抽象至关重要。
可扩展性：实验结果表明，基于 SMT 的合成可以扩展到学习复杂的、最小的加权自动机，而这些是目前现有算法无法触及的。

作者总结道，虽然他们未提供所有无限半环的通用终止证明（这是一个已知的开放问题），但他们的方法提供了一种实用的解决方案，能够在之前的方法失败或产生次优模型的场景中成功学习最小 WFAs。未来的工作包括探索更增量的假设更新，并将该方法扩展到概率自动机。