想象一下，你正试图教一个机器人如何使用一本全新的、神秘的食谱来烘焙一个非常复杂的蛋糕。这本书（深度学习库）非常庞大，但说明书却很模糊。它只说“加入面粉”，却没告诉你在面粉和糖的比例方面应该如何配合，或者如果你尝试用一把小勺子去搅拌一大碗面糊会发生什么。如果你猜错了，机器人可能会搞砸整个厨房，或者更糟——烤出的蛋糕看起来很完美，吃起来却很难吃。

这正是研究人员在面对深度学习库（如 PyTorch 和 TensorFlow）时所面临的问题。这些是驱动现代人工智能的“食谱”。它们功能强大，但也充满了隐藏的陷仍然（Bug）。问题的在于，这些库的使用手册往往不完整、零散，或者语言晦涩难懂。

于是有了 Centaur，一种由研究人员开发的用于测试这些库的新工具。你可以把 Centaur 想象成一个超级聪明的侦探，它结合了两种不同的思维方式：人类的创造性直觉和计算机的严密逻辑。

Centaur 的两个大脑

Centaur 是“神经符号化”（neurosymbolic）的，这意味着它有两个协同工作的脑子：

1. “神经”大脑（创意侦探）： 这个部分使用的是大语言模型（LLM）。你可以把它想象成一位博学多才的大厨，读过数百万篇烹饪博客和食谱。当 Centaur 查看一个特定的函数（例如“将两个数字相加”）时，LLM 会利用其知识来推测规则。“嘿，”LLM 可能会说，“通常情况下，如果你把两个列表相加，它们的尺寸必须相同，或者其中一个必须是可以在空间中进行复制的单个数值。”

   • 代价： LLM 很有创意，但也可能犯错。它可能会猜出一个听起来不错但实际上并不成立的规则。

2. “符号”大脑（严谨的数学教授）： 这个部分使用的是 SMT Solver（一种逻辑引擎）。你可以把它想象成一位严厉的数学老师，负责检查大厨提出的每一个假设。如果大厨说，“你可以将 5 杯面粉与 2 杯糖混合”，数学教授会运行计算，以检查这是否符合物理定律（或者在这种情况下，符合软件的运行规则）。

   • 力量所在： 数学教授不仅仅是回答“是”或“否”。它可以生成成千上万个具体的、有效的示例（例如“3 杯面粉，1 杯糖”）来证明该规则是行得通的。

Centaur 是如何运作的（配方步骤）

以下是 Centaur 使用的逐步流程，解释起来非常简单：

第一步：猜谜游戏（规则生成）
Centaur 要求“大厨”（LLM）写下关于一个特定函数应该如何运作的规则。为了防止大厨“放飞自我”，Centaur 会给它一个特殊的模板（语法），强制要求规则以特定的、逻辑化的格式编写。大厨可能会猜：“两个张量（tensors）的形状必须相同。”

第二步：事实核查（约束学习）
Centender 随后会将这些猜测与一小组已知的“良好”输入（有效数据）进行对比测试。

• 如果规则对所有良好输入都成立，Centaur 就会保留它。
• 如果规则失败，Centaur 就会将其丢弃。
• 优化： 有时，大厨会猜出两个意思完全相同的规则。Centaur 有一个特殊的技巧来识别这些重复项并删除多余的部分，这样它就不会感到困惑。

第三步：大规模生产（模糊测试/Fuzzing）
现在 Centaur 有了一系列经过验证的规则，它会利用“数学教授”（SMT Solver）来生成数百万个新的测试用例。因为这些规则在数学上是经过证明的，所以 Centaur 知道它创建的几乎每一个输入都是有效的。这就像拥有一台只生产完美蛋糕糊、绝不会生产出烧焦或生面糊的机器。

第四步：碰撞测试
Centaur 将这些数百万个完美的输入喂给深度学习库。如果库发生崩溃、冻结或给出奇怪的答案，Centaur 就会将其标记为一个 Bug。

为什么这很重要？

之前的工具尝试通过两种方式寻找 Bug：

• “随机投掷者”： 它们向库中投掷随机数据。这就像蒙着眼睛扔飞镖。大多数飞镖都会偏离目标（无效输入），因此浪费了大量时间。
• “代码阅读者”： 它们试图通过阅读库的源代码来弄清规则。这就像是在房子建造的过程中试图阅读它的蓝图。这很慢，而且如果蓝图本身很混乱，他们就会迷失方向。

Centaur 则不同。 它通过观察库的行为来学习规则（使用 LLM），然后利用数学来验证这些规则并生成数百万个完美的测试用例。

结果（论文声称的内容）

研究人员在 PyTorch 和 TensorFlow（这两个最流行的 AI 库）上测试了 Centaur。以下是他们的发现：

• 准确性： Centaur 的规则准确率达到了 94%。它很少猜错，也极少遗漏实际存在的规则。
• 效率： 其他工具生成的输入大多是无效的（对测试毫无用处），而 Centaur 生成的输入中 98% 是有效的。这意味着它几乎把所有时间都花在了测试真实的场景上，而不是浪费在不可能的场景上。
• 覆盖率： Centaur 探索了比以往最好的工具更多的代码部分。它找到了“深层”Bug——即软件核心逻辑中的问题——而不仅仅是表面错误。
• 找 Bug 能力： 使用 Centaur，团队在这些库中发现了 26 个新 Bug。其中 18 个得到了开发者的确认。其中一个甚至在论文发表前就被修复了！

关于“深层 Bug”的一个简单类比

想象一座桥。

• 浅层 Bug 就像路边的坑洼。容易看到，也容易修复。
• 深层 Bug 就像主支撑梁上的裂缝。从外面看不出来，但如果一辆重型卡车开过去，整座桥可能会坍塌。

之前的工具大多只能找到坑洼。而 Centaur 通过理解建造这座桥的复杂规则，能够找到支撑梁上的裂缝。

总结

Centaur 是一种全新的测试工具，它利用创造性 AI 来猜测深度学习库的规则，并使用逻辑数学引擎来验证这些规则，从而生成数百万个完美的测试用例。这种结合使得它能够发现其他工具无法发现的隐藏且危险的 Bug，从而让依赖这些 AI 的系统更加安全、更加可靠。