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 というソフトウェア）に渡します。これは感情も現実世界の知識も持たないロボット審判です。猫がふわふわかどうか、月がチーズでできているかどうかは気にしません。それはただ、結論が数学的に前提から導かれるかをチェックするだけです。数学が成り立てば「妥当（Valid）」と言います。そうでなければ「無効（Invalid）」です。

5. 探偵（重要な手がかりを見つける）

余分で無用の文が混ざっている難しいパズルの場合、システムは「貪欲アルゴリズム」を使用します。これは、一つの手がかりを一つずつ取り除いてみる探偵のように機能します。もし特定の手がかりがなくてもパズルが成り立つなら、その手がかりは無関係です。もしパズルが崩壊するなら、その手がかりは必要でした。これにより、システムは実際に重要な事実だけに焦点を当てることが保証されます。

彼らは何を見つけましたか？

• 小ささは美徳である: 彼らは「生徒」部分に比較的小さな AI モデル（40 億パラメータ）を使用しました。通常、小さなモデルは複雑な論理に苦労しますが、このシステムは実際の推論をロボット審判に任せることで、彼らを非常に優れものに変えました。
• バイアスの克服: AI にまず論理への変換を強制し、その後その結果をロボットに判定させることで、彼らは AI が現実世界の事実によってバイアスされるのを成功裡に防ぎました。「内容効果」は大幅に減少しました。
• 指標の問題: この論文はまた、コンペティションの採点方法における欠陥も指摘しています。採点システムは非常に敏感で、わずかな無作為な間違いさえもチームのスコアを壊滅させる可能性があり、システムが本当に「優れている」のか、それとも単に「運が良かった」のかを判断するのが難しくなっていました。

結論

この論文は、論理パズルを解くために巨大で超知能な AI が必要ではないことを示しています。代わりに、人間の言語を数学に変換する翻訳者として小さな AI を使い、実際の思考を愚かだが完璧なロボットに任せることができます。この組み合わせにより、AI が世界について「知っている」ことに気を取られるのを防ぎ、論理の規則に厳密に従うことを強制します。