Animation, Verification and Visualisation of Prolog Transition Systems with ProB

想象一下你是一名正在试图破解谜题的侦探，但你的“犯罪现场”不是一个犯罪现场，而是一段可能隐藏着漏洞（bug）的计算机代码。在计算机科学领域，这被称为形式验证（formal verification）。这就像是在构建一张关于程序“应该”如何运行的完美数学地图，然后检查每一个步骤，以确保程序不会迷路或崩溃。通常，这涉及只有专家才能读懂的复杂数学。但如果能将那些枯燥的数学变成一个栩栩如生的视频游戏呢？这就是 Prolog 的魔力——它是一种思维方式更倾向于逻辑谜题而非标准指令的编程语言。当你将 Prolog 与一个名为 PROB 的工具结合在一起时，你就得到了一个“模型检查器”——一个超级聪明的机器人，它可以观察你的逻辑谜题如何展开，发现错误，甚至让你一步步地回顾整个故事，看看问题到底在哪里。

这篇论文介绍的是如何为这个机器人进行一次重大升级。作者们来自杜塞尔多夫海因里希·海涅大学（Heinrich Heine University Düsseldorf），他们对现有的能够理解 Prolog 的工具 PROB 进行了升级，为其添加了一整套全新的“超能力”。你可以把它想象成将一本黑白素描本变成了一部高清、互动的电影制片厂。他们改进了可视化效果，增加了一种可以模拟数千场游戏以测试策略的方法，甚至创建了一个系统，让你可以在动作暂停时给计算机一个特定的指令，并观察它的反应。他们通过将经典游戏**四子棋（Connect Four）**转化为一个逻辑谜题，让不同的计算机“大脑”相互对战来测试这些新功能。结果表明，这是一个功能强大的工具包，它让检查复杂的计算机逻辑感觉更像是玩游戏，而不是在做作业。

“活生生”逻辑地图的魔力

其核心在于如何将用 Prolog（一种看起来像“如果……那么……”语句列表的语言）编写的一组规则转化为一个转换系统（transition system）。想象一个棋盘游戏，每个方格都是一个“状态”（例如“行人灯是红灯”），而每一次移动都是一次“转换”（例如“切换到绿灯”）。在过去，PROB 可以加载这些规则，并让你点击按钮从一个方格移动到下一个方格，从而展示路径。但那时它有点笨拙。

作者们显著提升了这种体验。首先，他们优化了视觉效果。以前，你可能只能看到显示“状态：红色”的文本列表。现在，他们集成了可以绘制实际图像的工具。如果你在建模交通灯，工具现在可以在屏幕上显示一个真实的、发光的红圈。如果你在建模国际象棋，它可以显示带有棋子精确位置的棋盘。更酷的是，他们增加了交互式可视化功能：你可以右键点击图片中的一个部件，工具就会显示出你可以进行的合法移动，就像玩真正的视频游戏一样。他们还创建了一个导出视觉故事为 HTML 文件的功能，这样你就可以与任何人分享你的逻辑谜题“电影”，即使他们没有安装特殊的软件。

“暂停并询问”功能

其中一个最令人兴奋的新技巧是他们称之为**符号转换（symbolic transitions）**的功能。想象你正在和计算机对弈，但计算机卡住了，因为它不知道你下一步想做什么。在过去，计算机可能会直接猜测或停止。现在，工具可以暂停并说：“嘿，我需要人类来决定这个部分！”它会等待你输入一个特定的值（比如“将骑士移动到 F3”），然后继续故事。这对于测试复杂的逻辑（比如证明一个数学定理）至关重要，因为人类可能需要做出计算机无法自行预测的选择。

他们还改进了追踪回放（trace replay）。把这想象成一个“存档游戏”功能。如果你找到了解决问题的完美移动序列，你可以保存它。稍后，你可以加载那个存档文件，工具会一步步重新播放完全相同的移动。这对于确保如果你今天修复了一个漏洞，明天不会意外将其再次破坏，是非常关键的。新版本使用一种智能格式（JSON）来保存这些回放，它能记住你当时所处的精确状态，因此回放每次都是完美的。

“百万场游戏”模拟器

或许是最强大的新增功能是运行 蒙特卡洛模拟（Monte Carlo simulations） 的能力。这是一种高级说法，意思是“让我们玩一百万次游戏来看看会发生什么”。作者将 PROB 连接到了一个名为 SIMB 的模拟器。你不再仅仅是观看一场游戏，而是可以告诉计算机连续进行 10,000 场四子棋，让不同的策略相互对抗。

他们利用这一点测试了三个用于四子棋的“大脑”：

1. 随机（Random）： 一个不加思考、随机选择移动的玩家。
2. 极大极小算法（Minimax）： 一种经典的 AI，它会通过查看后续几步来寻找最佳路径。
3. 蒙特卡洛树搜索（MCTS）： 一种更聪明的 AI，它通过模拟许多可能的未来来做出决策。

结果非常有趣。当随机玩家对抗 Minimax 时，如果随机玩家先走，他大约有 55.7% 的胜率；但当 Minimax 先走时，这个数字降到了 7.3%。然而，当 Minimax 对抗 MCTS 时，MCTS 玩家彻底碾压了对手，胜率约为 99%。作者指出，他们的 Minimax 玩家之所以显得较弱，是因为它只向后看两步（搜索深度较浅），这解释了为什么它在面对更先进的 MCTS 时输得如此惨烈。

他们还测量了这些游戏的耗时。随机和 Minimax 玩家速度很快，在不到 20 分钟内完成了 10,000 场游戏。但 MCTS 玩家稍慢一些，运行同样数量的游戏需要几个小时，因为它在进行大量的重度思考。有趣的是，他们发现 MCTS 玩家平均只需要 9.7 步 就能击败随机玩家，而 Minimax 则需要 18.0 步。

为什么这很重要

这不仅仅是为了玩游戏。作者展示了这些工具在教学方面的完美用途。想象一个正在学习编写代码的学生；与其只是盯着屏幕上的文本，他们可以看着自己的代码化为生动的动画。如果他们犯了错，他们可以看到“交通灯”变红或“棋子”消失，这使得理解出错的原因变得容易得多。

论文还强调，该系统非常适合构建解释器（interpreters）。解释器就像是一个翻译官，让一种编程语言能与另一种语言对话。通过使用 PROB 的新功能，学生和研究人员可以轻松构建其他语言（如 Java 或 WebAssembly）的翻译器，并通过观察它们运行的视觉过程来立即进行测试。

最后，作者并不是声称他们已经解决了所有的计算机科学问题。他们是在建议，通过使这些逻辑工具更加可视化、互动化并具备运行大规模模拟的能力，我们可以更早地发现漏洞，更好地教导学生，并更深入地理解复杂的系统。他们甚至暗示了一个未来的前景，即这些工具可以用于通过强化学习训练 AI 智能体，让计算机通过试错（就像人类一样）来学习玩游戏（或解决逻辑谜题）。但就目前而言，主要的胜利在于将枯燥、抽象的逻辑证明转变成了一个你可以观察、触摸并与规则共舞的游乐场。