想象一下，你正试图预测一台复杂机器的未来，比如一辆自动驾驶汽车或一个采摘水果的机器人。为了做到这一点，工程师们使用一种被称为**马尔可夫模型（Markov model）**的概率“地图”。你可以把这张地图想象成一个巨大的棋盘游戏，每一个方格都是机器可能处于的一种状态，而掷骰子的结果决定了它如何从一个方格移动到下一个方格。问题在于，要正确玩这个游戏，你需要准确知道掷出的每个数字出现的概率。在现实世界中，这些“骰子”就是转移概率——比如机器人手臂打滑或服务器崩溃的可能性。

传统上，为了填补这些数字，专家必须猜测机器可能进行的每一个微小动作的确切概率。这就像是要求一位厨师在知道晚餐是否准备好之前，先猜出锅里每一粒米的确切温度。这极其困难，而且如果猜测哪怕只有一点点偏差，关于机器可靠性或速度的整个预测都可能会出错。这就是**贝叶斯学习（Bayesian learning）**发挥作用的地方。这是一种随着获得新信息来更新猜测的数学方法，但它仍然需要一个起点，或者说一个“先验（prior）”。如果最初的猜测很糟糕，最终的答案也会很糟糕。

于是有了 EPIK，这是由 Simos Gerasimou 和 Xingyu Zhao 提出的一种新方法。EPIK 不再强迫专家去猜测机器内部那些微小的、不可见的骰子滚动情况，而是要求他们描述他们能看到的宏观、可观测的结果。这就像是问厨师：“米通常需要煮多久？”或者“锅通常多久会溢出来？”而不是询问每一粒米的温度。研究人员发现，通过使用这些高层级的、现实世界的观测结果，他们可以反向推导出隐藏的骰子滚动情况，且准确度更高。他们在采摘水果的机器人和外汇交易系统上测试了这种方法，结果表明该方法不仅有效，还能帮助预测那些难以测量、难以获取数据的棘手事物，例如能耗或罕见的故障。

核心理念：通过观察游戏来猜测骰子

这篇论文解决了一个软件工程中的难题：我们如何确保我们对复杂系统的计算机模型是准确的？当我们构建一个机器人或云服务的模型时，我们会使用数学来预测诸如“它会崩溃吗？”或“它完成任务需要多快？”之类的问题。但这些预测的质量取决于我们输入其中的数据。通常，这些数据是系统从一个状态转移到另一个状态的概率。

作者认为，要求人类专家去猜测这些具体的、低层级的概率，就像是要求一个人在预测风筝能否飞起来之前，先猜出树上每一片叶子的精确风速一样。这过于细节化了，专家往往无法掌握这些细节，或者会猜错。如果初始数值是错误的，整个验证过程就会失败，从而导致错误的工程决策。

EPIK：“逆向侦探”

论文介绍了一种名为 EPIK（Eliciting Prior Knowledge，即“诱导先验知识”）的巧妙工具，它颠覆了传统的逻辑。与其询问专家：“机器人采摘水果失败的概率是多少？”，EPIK 问的是：“根据您的经验，机器人完成任务的成功率通常是多少，以及通常需要多长时间？”

这些被称为系统级属性（system-level properties）。它们是专家真正理解并拥有数据的宏观结果。EPIK 将这些已知的输出视为线索。它利用一种称为贝叶斯学习的数学过程，从这些宏观线索出发，反向推导出导致这些结果的隐藏的、微小的概率。

以下是该过程的具体步骤：

1. 设定阶段： 想象一个正在采摘水果的机器人。它有一个“定位”状态，一个“采摘”状态，以及一个“决定重试或放弃”的状态。它采摘失败的确切概率是未知的（我们可以称之为“隐藏的骰子”）。
2. 线索阶段： 专家告诉 EPIK：“根据过去 200 次任务的经验，我们知道机器人的成功率为 80%，平均耗时约 4.75 秒。”这些是 PK-informed properties（基于先验知识的属性）。
3. 逆向工程阶段： EPIK 运行一个复杂的搜索过程（使用进化算法，类似于自然选择的数字版本），以寻找一组最能产生 80% 成功率和 4.75 秒结果的“隐藏骰子”组合。它不仅仅是找到一个答案，而是找到一整组符合线索的可能答案。
4. 回报阶段： 一旦 EPIK 根据已知线索推断出了隐藏的骰子滚动情况，它就可以用来预测我们尚不知道的事情。这些被称为难以捉摸的属性（elusive properties）。例如，没有人测量过机器人在执行此特定任务时的电池消耗量。但现在既然 EPIK 知道了机器人的运动方式，它就可以计算出可能的电池消耗量，即使此前从未有人记录过。

实验结果表明

研究人员在两个现实场景中测试了 EPIK：采摘水果的机器人和外汇交易系统。他们创建了不同复杂度及未知变量的系统版本。

• 准确性： 当他们将 EPIK 的预测与“地面真值”（Ground Truth，即数学上的真实值）进行对比时，结果非常接近。EPIK 的猜测与真实答案之间的差异极小（在测试用例中小于 0.00389）。这表明 EPIK 可以仅通过观察宏观图景，就可靠地逆向工程出系统的隐藏机制。
• “冲突”测试： 团队还测试了当专家给出相互矛盾的建议时（例如，一位专家说机器人非常可靠，而另一位说它很慢）会发生什么。他们发现，当线索存在矛盾时，EPIK 很难找到完美的匹配，并且其猜测的“误差”会上升。这其实是一件好事，因为它起到了警示灯的作用：如果线索不匹配，模型就会知道输入数据有问题。
• “难以捉摸”的胜利： 最令人兴奋的部分是验证“难以捉摸的属性”。在采摘水果机器人的测试中，他们拥有成功率和时间的数据，但却没有能耗的数据。EPIK 利用已知数据估算了能量消耗。由此得出的能量消耗分布是一个合理且有据可依的推测，决策者可以实际使用它；而如果没有 EPIK，他们只能进行盲目的猜测，或者干脆忽略这个问题。

为什么这很重要

这篇论文并不声称已经解决了所有的软件验证问题，但它提供了一种开启对话的强大新方式。它表明，我们不需要成为系统微观细节方面的专家才能建立一个好的模型；我们只需要成为系统产出结果方面的专家即可。

通过将重点从“猜测骰子”转向“观察游戏”，EPIK 使构建复杂系统（如自动驾驶汽车、医疗设备和云服务）的可信模型变得更加容易。它将定义每一个微小概率的艰巨任务，转变为一个更易于处理的任务——即描述我们已经了解的系统行为。而对于那些我们尚未知晓的事物，它为我们提供了一种基于数学逻辑的理性推测，而非盲目猜测。