LeanReasoner: Boosting Complex Logical Reasoning with Lean
摘要 大型语言模型（LLMs）在处理复杂的逻辑推理任务时经常遇到逻辑不一致性和这种推理的内在困难。我们使用Lean，一个定理证明框架来应对这些挑战。通过将逻辑推理问题形式化为Lean中的定理，我们可以通过证明或反驳相应的定理来解决这些问题。这种方法借助Lean的符号求解器减少了逻辑不一致性的风险。它还利用Lean广泛的定理证明库，提高了我们处理复杂推理任务的能力。我们的方法在FOLIO数据集上达到了最先进的性能，并在ProofWriter上达到了接近这个水平的表现。值得注意的是，这些结果是通过对每个数据集少于100个领域内样本进行微调实现的。
1 引言 逻辑推理是智能的基石，也是人类的核心能力，但长期以来一直是机器学习系统的一个挑战。尽管LLMs在理解和生成自然语言方面表现出色，但在处理复杂逻辑推理任务时常常表现不佳。它们经常出现逻辑不一致性，即模型产生与前提无关的幻觉性陈述，导致虚假的结果（Saparov and He, 2023; Dasgupta et al., 2022）。
最近的AI进展采用了一种结构化的方法，通过将推理问题分为符号形式化和问题解决两个步骤来应对这些问题（He-Yueya et al., 2023; Pan et al., 2023; Ye et al., 2023）。具体来说，形式化步骤通常由大型语言模型处理，而问题解决由现成的符号求解器处理。在这种方法中，符号求解器本质上起到了严格检查点的作用，确保模型输出符合逻辑规则，从而减轻了逻辑不一致性的问题。在这些方法中，求解器可能是完全确定性的，如SymPy（He-Yueya et al., 2023），或依赖于启发式和基本机器学习技术的组合，如Pyke（Pan et al., 2023）和Z3（Ye et al., 2023; de Moura and Bjørner, 2008）。虽然这种方法成功解决了幻觉问题，但在处理更复杂的问题时仍然存在困难。
作为一个强大的定理证明器和通用编程语言，Lean（de Moura et al., 2015）提供了一种将符号求解器与语言资源连接的有力解决方案。与符号求解器类似，Lean有一个严格的检查系统，确保每一步推理都得到验证。然而，它的区别在于它作为一个专门为定理证明开发的编程语言的额外功能。每天都有大量代码用Lean编写，捕捉到对训练LLMs有用的逐步推理“精华”。最近的一些研究已经利用Lean进行数学定理证明任务（Polu et al., 2023; Han et al., 2022a; Lample et al., 2022），显示了其在解决困难推理挑战方面的潜力。
在本文中，我们提出了LeanReasoner，一个基于Lean的框架，用于解决逻辑推理问题。我们使用LLMs将自然语言上下文形式化为Lean，并使用我们自己注释的适量数据对定制模型进行微调。当我们使用LLMs在Lean环境中动态生成解决方案时，我们的方法与LogicLM（Pan et al., 2023）的静态、预定义解决方案方法形成鲜明对比，后者仅依赖于传统技术如前向和后向链推理，和SATLM（Ye et al., 2023），其在Z3环境中使用一套预定的算法和启发式。LLMs作为解决方案工具的适应性使得我们的系统能够不断进化，利用大量的推理数据和信息。
参见图例 图1：我们方法的概述。自然语言上下文首先由“形式化器”处理。然后进入证明搜索阶段，“策略生成器”生成的所有策略（红色部分）用于操作目标。最后，结果由“结果解释器”解释。 我们在本文中的贡献有三方面：
- 据我们所知，这是首次尝试使用传统上与数学定理证明相关的Lean来进行自然语言逻辑推理。这项工作展示了数学定理证明和逻辑推理之间的可能交集。
- 我们的研究发现，与以前的技术相比，结合数学定理证明的预训练数据可以开发出更有效的逻辑推理求解器。此外，这种方法使我们在FOLIO上取得了SOTA结果。
- 我们提供了本研究中积累的训练数据，包括ProofWriter中100个Lean形式化的逻辑推理问题，以及FOLIO中27个类似的形式化问题。相应的Lean证明也包含在内。
2 问题定义和符号 我们要解决的任务是逻辑推理，以自然语言上下文给出的多选题形式。根据上下文，问题的答案可以通过逻辑推导得出。我们用于解决问题的框架是Lean。Lean是一个开源的定理证明编程语言，具有活跃的社区支持。其当前基础包括超过100,000个定理和1,000,000行代码。我们使用Lean作为一个通用的定理证明器，超出数学领域。
任务及其解决方案包括以下组件：
- 上下文，由自然语言语句组成，构成一组规则和事实。例如：Hudson是一只猫，所有的猫都是动物，猫经常喵喵叫。
- 问题，指所提出的问题。例如，Hudson经常喵喵叫吗？
- 选项，是一组可选答案（离散类别），从中可以选择一个答案。例如，真、假或未知。
- 形式化上下文，指在Lean中的上下文表示。例如，我们示例的形式化上下文为：公理A1：is_cat Hudson，公理A2： [ \forall x, \, \text{is_cat} \, x \rightarrow \text{is_animal} \, x ] 和公理A3： [ \forall x, \, \text{is_cat} \, x \rightarrow \text{often_meow} \, x ]
- 形式化问题：鉴于Lean作为一个定理证明器，问题被转化为两个对立的定理：一个主张正面的立场，另一个否定它。对于给定的例子，形式化问题将是：定理hudson_often_meows： [ \text{often_meow} \, \text{Hudson} ] 和定理not_hudson_often_meows： [ \neg \text{often_meow} \, \text{Hudson} ]
- 目标：在Lean中证明定理的上下文中，“目标”是指给定一组公理和规则，需要证明为真的逻辑陈述。当我们使用Lean证明器回答一个问题时，这个问题成为我们的根目标。此时，我们可以在Lean中应用各种指令来简化或分解这个主要目标并生成中间目标。 例如，使用前面的例子，如果根目标是证明定理hudson_often_meows： [ \text{often_meow} \, \text{Hudson} ] 一个中间目标可能是证明Hudson是一只猫。我们旨在使用提供的上下文解决每个中间目标，逐步证明根目标。一旦所有中间目标都解决了，我们就有效地证明了根目标，并成功结束了证明搜索。
- 策略：在Lean定理证明语言中，策略是用于操作目标以获得给定目标的证明的指令。例如，apply A3 Hudson是一个策略，使用于目标often_meow Hudson并将其转化为新目标is_cat Hudson。
这些组件及其相互关系的图示如图1所示。这个过程在Lean定理证明器的语言中被框定为一个目标满足过程。
3 LeanReasoner 我们的框架LeanReasoner由四个主要组件组成：形式化器、策略生成器、证明搜索机制和结果解释器。形式化器将上下文和问题转换为形式化上下文和形式化问题。策略生成器然后基于从形式化上下文中提取的前提生成策略。证明搜索机制监督策略执行和目标扩展。结果解释器分析证明搜索的输出，并在选项中识别正确答案。在本节中，我们详细介绍每个组件。
3.1 形式化器 作为形式化器，我们使用了OpenAI的模型text-davinci-003（GPT-3）和GPT-4（OpenAI, 2023）。对于text-davinci-003，我们遵循与Logic-LM（Pan et al., 2023）相同的提示方法，将任务规范和问题分开，使模型能够通过下一个令牌预测继续形式化任务。对于GPT-4，我们使用了类似的提示，但在系统提示中包含任务规范。
没有自动方法来断言上下文的所有实体、关系和约束都已被形式化结果捕
捉。然而，形式化结果的语法可以通过Lean检查。因为正确的语法是下游定理证明的前提，如果在编译过程中遇到错误，我们提供Lean生成的错误消息以及错误的形式化结果，并要求形式化器重新生成结果。我们进一步在§5中手动检查形式化器。我们采取严格的方法，如果形式化器失败超过一次，则该问题计为未正确解决。
3.2 策略生成器 我们用于策略生成的模型是ReProver（Yang et al., 2023）。该模型包含两部分：一个检索器，使用检索机制在提供当前目标时明确选择前提；一个生成器，使用目标和检索到的前提生成策略。
将问题解决任务划分为前提选择和策略生成简化了过程，便于更容易的故障排除。它隔离了潜在问题的来源，无论是前提选择还是策略生成，从而减少了问题的复杂性。此外，这种责任划分减轻了策略生成器的负担。在众多干扰中选择正确的前提是具有挑战性的，特别是在逻辑推理问题中，当多个选项似乎对当前步骤有吸引力但最终不会导致所需目标时。
我们的过程中的前提检索组件借鉴了Dense Passage Retriever（DPR）（Karpukhin et al., 2020）。提供一个目标 (g) 作为查询和一组候选前提 (P) ，它生成一个 (m) 个前提的排名列表。在DPR中，(g)和(P)都被视为嵌入在向量空间中的原始文本。然后我们检索最大化目标和前提之间余弦相似性的前 (m) 个前提。对于策略生成，我们使用标准的序列到序列模型。目标和前提被串联在一起作为一个字符串生成新的策略。
作为基线，我们还提示GPT-4生成证明。当选择的定理与答案一致时（比如选择的定理是问题的正面立场且答案是“是”），我们将正确的证明作为提示的一部分提供给GPT-4。相反，如果答案与选择的定理不一致或答案未知，形式化的定理是无法证明的。在这些情况下，我们仍然鼓励模型进行逐步推理，即使它最终会遇到障碍。提示GPT-4的一个示例可以在附录A.1中找到。
3.3 证明搜索 证明搜索模块控制选择策略和维护状态的整个搜索过程。本质上，搜索方法的目标是通过策略调用逐步演化目标，构建一个证明树。这个方法最早在GPT-F中引入（Polu and Sutskever, 2020）。LeanDoJo（Yang et al., 2023）是一个最近发布的框架，使得与Lean程序交互变得可能，我们在研究中使用了这一方法的实现。
作为参考，图1的中间部分提供了这一过程的实际示例。从根目标开始，对于每个给定的证明目标，我们探索64种可能的策略。所有目标都保存在一个优先队列中，并基于目标的累计对数概率进行扩展。累计对数概率定义为从根目标到当前目标的策略的对数概率之和。这意味着我们倾向于扩展那些生成模型具有最高全局信心的目标。
为了提高搜索效率并避免潜在的循环，我们引入了一个机制，如果我们已经探索了一个具有前缀 (N) 的状态序列的节点 (M) ，则停止扩展节点 (N) 。本质上，如果当前目标包含所有先前探索过的目标元素，则不应进一步扩展。这是基于这样的观察：如果我们已经评估了特定目标的潜在路径和结果，那么探索该目标的更广泛版本是多余的。这样的机制避免了不必要的重复，简化了搜索过程，提高了整体效率。此外，我们定义有效的证明为没有“作弊”策略（如sorry）的证明，这些策略告诉Lean假设当前目标已完成，尽管它尚未被证明。这意味着包含“作弊”策略的所有路径都被忽略。
搜索过程中的错误通常表现为超时或节点搜索耗尽。我们为每次搜索分配了三分钟的时间窗口，通常足够。我们在实验部分提供了更多关于策略生成器错误的分析。
3.4 结果解释器 如果正确答案是“未知”，我们仅在既不能证明“真”也不能证明“假”的情况下将结果视为正确。本研究中调查的所有数据集只包含唯一正确答案的问题。因此，如果证明系统验证了多个选项，则立即将响应标记为不正确。
4 实验设置 我们现在描述我们的实验设置：用于评估和模型训练的数据集以及模型训练的详细信息。
4.1 评估数据 在我们的评估中，我们使用了两个常见的逻辑推理数据集作为测试平台：
ProofWriter：这个演绎逻辑推理数据集以直观的语言形式呈现问题。我们采用了Pan等人（2023）提出的开放世界假设（OWA）子集，其中每个实例由{问题，目标}配对组成。每对的标签包含真、假或未知。它包括基于所需推理深度的五个部分。我们重点关注最具挑战性的深度5子集。为了公平比较Logic-LM，我们使用了相同的600个样本测试，确保标签分布均匀。
FOLIO：与ProofWriter不同，FOLIO使用一阶逻辑构建。这增加了证明部分的复杂性。该数据集还以更自然的措辞呈现问题，关系也复杂得多。如此结合高级逻辑和丰富的语言结构，使得FOLIO中的形式化任务比ProofWriter难得多。对于我们的分析，我们使用了整个FOLIO测试集，共包含204个示例。
4.2 领域适应的训练数据 关于模型训练的数据，我们收集了ProofWriter的100个定理证明和FOLIO的27个定理证明，其中每个问题的证明要么是手动注释的，要么是从GPT-4生成的成功证明中收集的。数据收集大约花了八天时间。
在数据注释过程中，我们采用了两种不同的方法来构建证明。一种方法模仿了简单的策略，包括所有中间步骤和引理的详细过程，类似于我们在接到定理证明任务时可能采用的方式。相反，第二种方法类似于mathlib中的证明格式。我们通过减少中间引理的数量并将多个策略组合成一个复合策略，生成相同问题的更简洁的证明。为同一问题提供两种注释的目的是检查注释风格对下游逻辑推理的影响。在接下来的实验中，我们使用Intuitive（直观）指代第一种注释风格，Concise（简洁）指代第二种注释风格。附录C中有一个示例。
尽管收集到的数据有限，但逻辑推理的推理模式可能与数学推理中发现的模式相似，这些模式可能在预训练期间学到。数据收集的主要目的是领域适应，从数学推理转移到自然语言逻辑推理。
4.3 模型训练 我们使用与ReProver论文中相同的模型结构进行预训练，即Google的Byte-T5（Xue等，2022）。我们还试验了在mathlib上预训练的LeanDoJo的预训练ReProver（Yang等，2023）。微调我们收集的数据大约花了六个小时，使用了一台A100 40G。超参数与原始LeanDoJo论文中的相同。
5 结果 我们展示了实验结果，包括基于提示的基线的检查、LeanReasoner的实验结果以及我们工作与其他基线的比较。
| 模型 | ProofWriter | FOLIO | ||||
|---|---|---|---|---|---|---|
| Formalize | Prove | Answer | Formalize | Prove | Answer | |
| GPT-4 Base | 94% | 15% | 80% | 60% | 10% | 35% |
| GPT-4 Base Comments | 99% | 15% | 80% | 75% | 15% | 35% |
| GPT-4 Base Separate | 95% | 5% | 75% | 60% | 10% | 40% |
| GPT-3 Base Comments | 77% | 12% | 63% | 45% | 10% | 35% |
| Logic-LM | 98% | 75.5% | 74% | 65% | 69.2% | 55% |
表1：通过OpenAI语言模型API对100个ProofWriter样本和40个FOLIO样本进行形式化、证明和答案选择的准确性，使用手动注释。‘GPT-4 Base’作为我们的基线，其中少样例包括单个提示中的形式化和证明生成。在‘GPT-4 Base Comments’中，我们在Lean代码中逐行添加注释来增强这些样例。对于‘GPT-4 Base Separate’，我们将任务分为两个部分，使用单独的提示进行形式化和证明生成。为了简化，我们在评估Logic-LM时没有使用自我改进技术。
5.1 基于提示的基线 由于没有自动方法来验证形式化的准确性，我们手动检查了形式化的结果，以确定在形式化或证明生成阶段是否发生错误。在此检查中，只有正确捕捉每个事实、公理和规则的形式化才被视为准确。我们手动检查了ProofWriter验证集的100个问题和FOLIO训练集的40个问题。结果总结在表1中。
形式化准确率的比较。 ProofWriter的形式化准确率远高于FOLIO。这可以归因于其语言结构较简单。对于FOLIO，尽管使用LLM进行形式化有助于从自然语言上下文中过滤掉不必要的细节，但仍然存在一些常见的错误模式。我们在附录B中使用从各种错误实例中派生的综合样本，说明了典型的GPT-4错误模式。有趣的是，Lean的形式化准确率与Logic-LM中的Prolog和FOL一致。这种一致性突显了Lean的多功能性，使其能够在单一框架内统一表示不同类型的问题。
添加文本注释可以提高形式化准确率。 我们观察到，当形式化代码与从上下文中提取的描述性文本注释配对时，结果有所改善。这种方法进一步将形式化任务分为两个子任务：1）将文本上下文与形式化代码链接起来；2）基于先前的文本上下文生成形式化代码。这些文本提示作为原始文本和形式化代码之间的桥梁，增强了形式化的性能。
GPT-3在形式化方面的表现不如GPT-4。 GPT-3和GPT-4在表现上的区别显而易见。虽然对较简单问题的形式化是一样的，但GPT-3在处理复杂逻辑和复杂问题时表现不佳。因此，我们选择不在进一步的测试中使用GPT-3。此外，我们还试验了CodeLLAMA模型家族，用于类似任务，但发现其形式化准确率显著低于GPT-3，在ProofWriter上的准确率不足30%。
基于提示的基线的证明准确率非常低。 表中的证明准确率部分由生成的证明是否能在Lean中成功验证决定。如果问题的形式化作为定理是正确的，并且证明可以在没有任何错误或警告的情况下验证，那么我们可以将证明视为有效。然而，生成的证明的准确率非常低。问题可能出在分配给大型语言模型的任务太多，难以在单个提示中解决这两者。尽管我们努力将形式化和证明分开，但结果仍然令人失望，这突显了GPT-3和GPT-4在生成正确Lean证明方面的困难。有趣的是，Logic-LM的证明准确率不如预期高。在复制他们的代码时，我们发现他们选择的求解器Pyke并不理想，在有多个搜索路径时难以找到答案，某些路径可能导致循环。
基于提示的基线的答案准确率出乎意料地高。 尽管GPT-4的大部分证明的准确率较低，但在ProofWriter上它的最终选择的准确率很高（如答案列所示）。我们认为这可能是由于GPT-4在训练中暴露于数据集，可能导致一定程度的记忆。
5.2 LeanReasoner | 方法 | 预训练 | 微调 | ProofWriter | FOLIO | | — | — | — | — | — | | on Math Data | on our Annotation | 前提选择 | 证明 | 前提选择 | 证明 | | GPT-4 | N/A | N/A | N/A | 15% | N/A | 10% | | LeanReasoner | Yes | No | 56.2% | 81.3% | 0% | 23.5% | 38.2% | 0% | | LeanReasoner | No | Intuitive | 62.5% | 100% | 99% | 54.8% | 95.2% | 71.4% | | LeanReasoner | Yes | Intuitive
| 75% | 100% | 99% | 71.4% | 96.8% | 85.7% | |||
| LeanReasoner | Yes | Concise | 75% | 100% | 99% | 83.8% | 97.4% | 85.7% |
表2：99个ProofWriter测试样本和28个FOLIO测试样本中前提选择的Recall@k和整体证明准确率的比较分析。注意这里的证明准确率不同于表1，因为它直接与最终准确率相关。评估LeanReasoner在定理证明数据和直观及简洁注释集上的预训练和微调效果。由于在提示GPT-4时复杂性较高，GPT-4基线未计算前提选择准确率。
在本节中，我们重点训练自己的模型，使用我们注释的训练数据生成策略。为了隔离错误形式化的影响，我们仅使用前一小节中准确的形式化进行测试。这样我们得到了99个ProofWriter测试示例和28个FOLIO测试示例。所有发现详见表2。
在注释数据上微调提高了前提选择准确率。 我们首先使用recall@1和recall@4度量标准比较前提选择的结果。recall@k度量标准定义如下：
| [ \text{recall@k} = \frac{ | \text{GT_Prem} \cap \text{Pred_Prem}[0:k] | }{ | \text{GT_Prem} | }, ] |
其中GT_Prem表示真实前提，Pred_Prem表示顶级预测前提。LeanReasoner仅用数学数据预训练的次优结果可能归因于数学定理证明和逻辑推理之间的领域不匹配。模型经常试图使用在数学定理证明中有用但不适用于逻辑推理的其他无关策略。此外，FOLIO的准确率明显低于ProofWriter。这种差异可能是由于FOLIO的复杂逻辑及其需要更广泛的一阶逻辑策略（如cases、have和contradiction）。相比之下，ProofWriter主要采用apply、exact和split等策略。
在定理证明数据上预训练提高了整体准确率。 关于整体证明结果，LeanReasoner在数学定理证明数据上预训练后，在ProofWriter和FOLIO数据集上的表现始终优于其他方法。这表明我们的模型有效地利用了数学定理证明中的逻辑“黄金”。虽然前提选择器受益于明显的提示和有限的选择范围，但策略生成的领域则要广泛得多。这个广泛的选择使得ReProver基线的证明准确率几乎可以忽略不计。此外，前提选择准确率和整体证明准确率之间存在强相关性。尽管对于像ProofWriter这样较简单的数据集，预训练的LeanReasoner的优势可能不太明显，但在更复杂的数据集如FOLIO上，其价值则更加显著。
简洁注释在前提选择上效果更好。 在这个小测试集上，用不同注释进行微调对前提选择和策略生成有轻微影响。用简洁注释微调时，LeanReasoner也会尝试生成简洁的证明，通常使用提供更多信息的复合策略进行前提选择。然而，在这个小测试集上的最终证明准确率并没有改变。图2展示了我们比较的三种主要方法对同一问题生成的证明。在没有预训练的情况下，模型难以识别适当的解决方法，仅试图应用下一个可用定理，缺乏明确目标。虽然直观数据提供了许多引理，有助于在编写证明时的思考过程，但这些过多的引理并不能有效地帮助LLMs生成策略。
参见图例 图2：由LeanReasoner在没有预训练（左）、在直观数据上微调（中）、在简洁数据上微调（右）生成的样本证明。
5.3 其他基线 | 方法 | 准确率 | | — | — | | 全训练集方法 | | | Abs Biases Gontier et al. (2022) | 80.6% | | MetaInduce Yang et al. (2022) | 98.6% | | RECKONING Chen et al. (2023b) | 99.8% | | 零样本方法 | | | GPT-4 CoT Pan et al. (2023) | 68.1% | | Logic-LM Pan et al. (2023) | 79.3% | | 我们的方法（在100个样本上微调） | | | LeanReasoner without Pretraining | 95.8% | | LeanReasoner fine-tuned on Intuitive | 98.3% | | LeanReasoner fine-tuned on Concise | 98.3% |
表3：在mathlib上预训练的微调LeanReasoner。全训练集方法表示模型在ProofWriter的全训练集上训练。用简洁注释微调在此数据集上并未带来任何优势。
| 方法 | 准确率 |
|---|---|
| 全训练集方法 | |
| Roberta Han et al. (2022b) | 62.1% |
| FOLNet Chen (2023) | 70.6% |
| 零样本方法 | |
| GPT-4 CoT Pan et al. (2023) | 70.6% |
| Logic-LM Pan et al. (2023) | 74.5% |
| Lean Z3 (SATLM) | 77.5% |
| 我们的方法（在27个样本上微调） | |
| LeanReasoner without Pretraining | 66.2% |
| LeanReasoner fine-tuned on Intuitive | 78.4% |
| LeanReasoner fine-tuned on Concise | 82.6% |
表4：从“Lean Z3”的结果来自应用于形式化Lean代码的lean-smt。全训练集方法表示模型在FOLIO的全训练集上训练。我们的方法在FOLIO上实现了最先进的性能。
我们已经证明，在定理证明数据上预训练能带来更好的性能，接下来将我们的结果与ProofWriter和FOLIO的基线进行对比。评估使用与LogicLM相同的600个问题集和整个FOLIO测试集。
我们的方法在ProofWriter上以显著较少的数据取得了近乎完美的准确率。 如表3所示，我们的方法在ProofWriter数据集上取得了近乎完美的准确率。虽然其他方法除了Logic-LM和GPT-4 COT都使用了ProofWriter的整个训练集，我们的方法仅依赖100个示例，突显了我们方法的效率。用简洁注释微调在此数据集上的最终性能没有带来任何优势。
我们的方法在FOLIO上实现了最先进的性能。 表4展示了我们在FOLIO上的表现。为了与使用Z3求解器的SATLM进行公平比较，我们在我们的形式化Lean代码上使用了lean-smt工具。该工具以“sat/unsat”的形式生成结果。在Z3中，“sat”表示“可满足”。当Z3返回“sat”结果时，表示存在一组变量值使得定理为真。另一方面，“unsat”表示“不可满足”。当Z3返回“unsat”时，表示公式本身存在矛盾，在任何情况下都无法满足。我们使用结果解释器将这些结果类似于“找到证明/未找到证明”进行解释。由于FOLIO问题证明的长度较长，我们观察到，当LeanReasoner在直观数据集上微调时，常常花费过多时间进行探索，有时会进入循环。相比之下，生成较短的证明往往更容易发现证明。虽然用简洁数据集微调时生成的策略更具挑战性，FOLIO上LeanReasoner的瓶颈在于搜索过程。
基准测试中的挑战。 需要注意的是，在某些情况下，问题形式化或证明生成可能出错，但最终答案仍被视为正确。一个例子是，当问题的答案是未知时，这些阶段会出现错误。在这种情况下，模型将难以证明正或负定理。然而，使用我们的结果解释器，这些实例尽管在问题处理上存在潜在问题，仍将被归类为正确。