Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework¶

会议: ACL 2025
arXiv: 2412.16953
代码: http://llm-symbol.github.io/Aristotle
领域: LLM推理
关键词: 逻辑推理, 符号推理, 反证法, Decompose-Search-Resolve, 符号表达式

一句话总结¶

提出 Aristotle 逻辑推理框架，将符号表达式和逻辑规则全面融入 Decompose-Search-Resolve 的每个阶段，通过逻辑分解器、搜索路由器和消解器三大组件实现逻辑完备的推理，在多个逻辑推理基准上以 GPT-4 平均提升 4.5%、GPT-4o 平均提升 5.4% 超越 SOTA。

研究背景与动机¶

领域现状: - CoT、ToT、GoT 等推理方法已在一般推理任务上取得显著进展 - SymbCoT 将符号表达式引入 CoT 推理，达到了逻辑推理的 SOTA - 然而，逻辑推理要求最严格的证据和逻辑严谨性，是 LLM 推理中最具挑战的任务之一

现有痛点: - 分解阶段: LLM 依赖语言 token 关系而非逻辑结构分解问题，导致子问题断裂 - 搜索阶段: 现有路径搜索依赖不可靠的评估器选择节点，导致错误传播（搜索错误率 15.0%） - 消解阶段: 用简单文本提示引导 LLM 解子问题，频繁产生逻辑错误（推理错误率 28.4%） - 效率问题: 错误节点浪费计算资源，不可靠的评估器导致不必要的节点探索

核心矛盾: - 通用推理方法（如 ToT）忽视逻辑任务的内在结构，未将逻辑规则有效融入 Decompose-Search-Resolve 框架 - 结果是既不高效也不准确

本文目标 - 如何在逻辑推理的分解、搜索、消解每个阶段都充分利用逻辑结构和符号规则 - 如何减少搜索错误和推理错误，同时提高效率

切入角度: - 形式化逻辑方法论：用 Prolog 语法翻译、CNF 范式分解、反证法搜索、消解原理消解 - 将经典逻辑推理的整套方法论系统性地嵌入 LLM 推理框架

核心 idea: - 将符号逻辑表达式和规则（翻译→CNF分解→反证法搜索→消解原理）完全集成到 LLM 推理的每个阶段

方法详解¶

整体框架¶

Aristotle 由四个模块组成： 1. Translator（翻译器）: 将自然语言前提和问题翻译为 Prolog 符号格式 2. Decomposer（分解器）: 将符号表达式规范化为 CNF（合取范式），消除量词 3. Search Router（搜索路由器）: 基于反证法搜索互补子句 4. Resolver（消解器）: 基于消解原理消除互补项，生成新子句

推理过程分三步：初始化 → 迭代搜索消解 → 得出结论

关键设计¶

Logical Decomposer（逻辑分解器）:
- 做什么: 将前提和查询通过规范化（Normalization）和 Skolemization 转换为 CNF 形式
- 核心思路: 例如 \(\forall x (P(x) \rightarrow Q(x))\) 被分解为 \(\neg P(x) \vee Q(x)\)
- 设计动机: CNF 简化了推理过程，使其更容易应用形式化消解规则
Logical Search Router（逻辑搜索路由器）:
- 做什么: 采用反证法（proof by contradiction），搜索与当前子句互补的前提子句
- 核心思路: 如当前子句含 \(P(x, \text{True})\)，则搜索含 \(P(x, \text{False})\) 的前提子句
- 设计动机: 反证法直接搜索逻辑冲突，避免了依赖不可靠评估器的搜索错误；这是一个基于规则而非 LLM 的模块
Logical Resolver（逻辑消解器）:
- 做什么: 基于 Robinson 消解原理消除互补项，连接剩余项生成新子句
- 核心思路: \(C_{\text{current}} = P(x,T) \vee A\)，\(C_{\text{complement}} = P(x,F) \vee B\) → \(C_{\text{resolved}} = A \vee B\)
- 设计动机: 消解原理提供清晰简洁的指令，最小化推理错误
双路径推理（Dual-Path Reasoning）:
- 做什么: 同时从 \(S_n\) 和 \(\neg S_n\) 两条路径进行反证法推理
- 核心思路: 根据四种组合确定答案：True/False/Unknown/Self-Contradictory
- 设计动机: 单路径无法区分所有四种逻辑状态

损失函数 / 训练策略¶

本文是 prompting 方法，不需要训练
搜索路由器是基于规则的模块（非 LLM），其他模块通过 LLM in-context learning 实现
最大迭代次数 \(I_{\text{max}}\) 控制推理深度

实验关键数据¶

主实验¶

在三个逻辑推理数据集上测试，使用 GPT-4 和 GPT-4o：

方法	ProntoQA	ProofWriter	LogicNLI	平均 (GPT-4)
CoT	98.9	68.1	51.0	72.6
CoT-SC	93.4	69.3	57.3	73.3
ToT	97.6	70.3	52.7	73.5
SymbCoT	99.6	82.5	59.0	80.4
Aristotle	99.6	86.8	68.3	84.9

GPT-4o 结果：

方法	ProntoQA	ProofWriter	LogicNLI	平均
SymbCoT	99.4	82.3	58.7	80.1
Aristotle	99.6	88.5	70.7	86.3

GPT-4 上平均提升 4.5%（vs SymbCoT），GPT-4o 上提升 5.4%（+6.2 on ProofWriter, +12.0 on LogicNLI）

跨模型泛化性（Claude-3.5-Sonnet / Llama-3.1-405B）：

模型	ProntoQA	ProofWriter	LogicNLI	平均
Claude + Aristotle	99.0	86.5	61.3	82.3 (+5.3)
Llama + Aristotle	98.4	89.5	69.0	85.6 (+12.1)

Llama-3.1-405B 上 ProofWriter 提升 20.0%，LogicNLI 提升 8.7%

关键发现¶

越复杂的逻辑场景，提升越大: ProntoQA 简单场景几乎无提升，LogicNLI 复杂场景提升最显著（6.3-12.0%）
搜索路由器最关键: 消融实验中，去除搜索路由器在 ProofWriter 上下降 50.8%，LogicNLI 下降 31.6%
分解器在复杂场景更重要: LogicNLI 包含 "either...or..." 等复杂逻辑结构，依赖分解器
框架跨模型泛化: 在 GPT-4、GPT-4o、Claude-3.5、Llama-405B 上均有效

亮点与洞察¶

经典逻辑方法论的现代复兴: 将消解原理、CNF 转换、反证法等经典形式化逻辑方法与 LLM 结合
接近逻辑完备: 覆盖了 True/False/Unknown/Self-Contradictory 四种答案类型
搜索路由器是基于规则的: 非 LLM 生成，避免了 LLM 搜索的不可靠性
双路径反证法设计巧妙: 一条路径无法区分所有四种逻辑状态，双路径+公式 (1) 优雅解决
错误类型分析深刻: 28.4% 推理错误 + 15.0% 搜索错误的定量分析很有说服力

局限与展望¶

依赖 LLM 完成翻译/分解/消解，这些环节仍可能引入错误
仅处理命题逻辑和一阶逻辑的子集，对更复杂的逻辑形式（如模态逻辑、时态逻辑）适用性未知
反证法的最大迭代次数 \(I_{\text{max}}\) 需要预设，可能影响复杂推理链的覆盖
Prolog 翻译步骤需要 LLM 具有较强的符号理解能力，小模型上效果未验证
计算成本未详细报告，双路径推理可能导致 API 调用翻倍

评分¶

维度	分数 (1-10)
创新性	8
技术深度	8
实验充分性	8
写作质量	8
实用价值	7
总分	7.8