UFAL-CUNI at SemEval-2026 Task 11: An Efficient Modular Neuro-symbolic Method for Syllogistic Reasoning

想象一下，你正在试图教一位非常聪明但稍有分心的学生（一个大语言模型）如何求解称为三段论的逻辑谜题。这些谜题类似于：

• 前提 1： 所有猫都是动物。
• 前提 2： 有些动物毛茸茸的。
• 结论： 因此，有些猫是毛茸茸的。

问题在于，这位学生有一个坏习惯：他们会让现实世界的知识干扰判断。如果谜题说“所有猫都是毛茸茸的”，学生可能会因为知道猫确实是毛茸茸的而回答“正确”，即使谜题的逻辑实际上并不支持该结论。这被称为**“内容效应”**。学生受到他们认为为真的事物的偏见，而非受到谜题规则的限制。

本文的作者构建了一个特殊的“辅导系统”来解决这个问题。以下是该系统的工作原理，简单解释如下：

1. 翻译器（双语口译员）

首先，如果谜题是用外语（如葡萄牙语或俄语）写的，系统会使用一个大语言模型将其翻译成英语。这就像一位翻译员确保在逻辑游戏开始前，所有人都在使用同一种语言。

2. 符号专家（LaTeX 撰写者）

这是该系统的巧妙之处。系统不是直接让学生求解谜题，而是要求他们将句子重写为一种特定的“代码”，称为一阶逻辑（FOL），并以LaTeX格式书写（看起来像数学公式）。

• 为什么是 LaTeX？ 作者们意识到，要求学生直接用计算机的“母语”（Prover9 语法）书写，就像要求人类直接说二进制代码一样。这会导致过多的错误。
• 类比： 这就像要求学生先用标准符号（$\forall$、$\exists$、$\rightarrow$）在白板上写下数学题，而不是试图直接将其输入到一台只理解某种奇怪、特定代码的计算器中。学生在书写“白板”版本时表现要好得多，因为他们在训练数据中见过这种形式。

3. 翻译器（代码转换器）

一旦学生用“白板”（LaTeX）格式写出逻辑，一个简单的计算机脚本（一个“转译器”）就会充当严格的编辑。它立即将该整洁的 LaTeX 代码转换为计算机运行证明所需的特定、僵化的代码（Prover9 语法）。这一步完全是机械的，不涉及那位“分心”的学生，因此很少出错。

4. 裁判（自动定理证明器）

最后，系统将僵化的代码交给一个定理证明器（一款名为 Prover9 的软件）。这是一个零情感、零现实世界知识的机器人裁判。它不在乎猫是否毛茸茸，也不在乎月亮是否由奶酪制成。它只检查：结论在数学上是否从前提中推导出来？ 如果数学成立，它就说“有效”；否则，就说“无效”。

5. 侦探（寻找关键线索）

对于包含额外无用句子的更难谜题，系统使用一种“贪心算法”。它像一个侦探，尝试一次移除一条线索。如果移除某条特定线索后谜题仍然成立，那么该线索就是无关的；如果谜题因此崩溃，那么该线索就是必要的。这确保系统只关注那些真正重要的事实。

他们发现了什么？

• 小即是美： 他们为“学生”部分使用了一个相对较小的 AI 模型（40 亿参数）。尽管小模型通常在复杂逻辑方面表现不佳，但该系统通过将实际推理工作外包给机器人裁判，使其变得非常擅长逻辑。
• 战胜偏见： 通过强制 AI 先转换为逻辑，然后让机器人裁判结果，他们成功阻止了 AI 受现实世界事实的偏见影响。“内容效应”显著下降。
• 指标问题： 论文还指出了比赛评分方式的一个缺陷。评分系统过于敏感，即使是一个微小的随机错误也可能导致团队得分暴跌，使得很难判断一个系统究竟是真正“优秀”还是仅仅“运气好”。

核心结论

这篇论文表明，你不需要一个巨大的、超级智能的 AI 来解决逻辑谜题。相反，你可以使用一个小 AI 作为翻译器，将人类语言转换为数学，然后让一个愚蠢但完美的机器人进行实际的思考。这种组合阻止了 AI 被它“知道”的世界知识所分散注意力，并迫使它严格遵循逻辑规则。