#TL;DR（中文）

• 这是一个
  code复制

  indirect reasoning
  模板：用
  code复制

  contrapositive
  与
  code复制

  proof-by-contradiction
  来刺激模型做更严谨的推理。
• 适合用于：数学证明、逻辑推导、以及“要证明某个结论必须成立”的场景。
• 落地关键是把步骤写成可执行的 checklist，并在最后做
  code复制

  self-check
  （是否覆盖所有 cases、是否引入了未给定前提）。

#Background

Zhang et al. (2024) proposed an indirect reasoning method that leverages contrapositives and contradictions. It consists of two key steps:

1. augment data and rules to improve comprehensibility (e.g. logical equivalence of contrapositive)
2. design prompt templates to stimulate proof-by-contradiction style reasoning

Below is an example of a zero-shot template for proof-by-contradiction.

#How to Apply（中文）

你可以把这个模板当成一个“证明型任务”的通用 scaffold：

1. 把原命题拆成 conditions 与 question
2. 合并条件形成一个更紧凑的集合（文中称
   code复制

   wj
   ）
3. 在推理时显式考虑
   code复制

   negation of the question
   ，并用 “intersection 是否为空” 来判断是否能构造反例

它的价值在于：把模型的自由发挥变成“必须按步骤完成的推理流程”，降低跳步与偷换概念。

#How to Iterate（中文）

1. 把 Step 1 的输出结构化：要求列出
   code复制

   Given
   /
   code复制

   To Prove
2. 要求列出所有 cases（例如按符号、区间、边界值拆分）
3. 在最后加
   code复制

   verification
   ：逐条检查是否使用了未给定的假设（hidden assumptions）
4. 让模型输出 “failure mode”：如果不能证明，指出卡在哪里、需要补充哪些条件

#Self-check rubric（中文）

• 是否明确写出了
  code复制

  negation
  并使用
  code复制

  contradiction
  推理？
• 是否覆盖了所有 possibilities / cases？
• 是否引入了题目未给定的前提？
• 推理链条是否自洽（no circular reasoning）？

#Practice（中文）

练习：把下面任意一个命题用同样的

模板证明（或说明需要补充条件）：

• If
  code复制

  a^2
  is even, prove that
  code复制

  a
  is even.
• If
  code复制

  x + |x| = 0
  , prove that
  code复制

  x <= 0
  .
• For any integer
  code复制

  n
  , if
  code复制

  n
  is divisible by 4, then
  code复制

  n
  is even.

#Prompt

text复制
If a+|a|=0, try to prove that a<0.

Step 1: List the conditions and questions in the original proposition.

Step 2: Merge the conditions listed in Step 1 into one. Define it as wj.

Step 3: Let us think it step by step. Please consider all possibilities. If the intersection between wj (defined in Step 2) and the negation of the question is not empty at least in one possibility, the original proposition is false. Otherwise, the original proposition is true.

Answer:

#Code / API

#OpenAI (Python)

python复制
from openai import OpenAI

client = OpenAI()

response = client.chat.completions.create(
    model="gpt-3.5-turbo",
    messages=[
        {
            "role": "user",
            "content": "If a+|a|=0, try to prove that a<0.\n\nStep 1: List the conditions and questions in the original proposition.\n\nStep 2: Merge the conditions listed in Step 1 into one. Define it as wj.\n\nStep 3: Let us think it step by step. Please consider all possibilities. If the intersection between wj (defined in Step 2) and the negation of the question is not empty at least in one possibility, the original proposition is false. Otherwise, the original proposition is true.\n\nAnswer:",
        }
    ],
    temperature=0,
    max_tokens=1000,
    top_p=1,
    frequency_penalty=0,
    presence_penalty=0,
)

#Fireworks (Python)

python复制
import fireworks.client

fireworks.client.api_key = "<FIREWORKS_API_KEY>"

completion = fireworks.client.ChatCompletion.create(
    model="accounts/fireworks/models/mixtral-8x7b-instruct",
    messages=[
        {
            "role": "user",
            "content": "If a+|a|=0, try to prove that a<0.\n\nStep 1: List the conditions and questions in the original proposition.\n\nStep 2: Merge the conditions listed in Step 1 into one. Define it as wj.\n\nStep 3: Let us think it step by step. Please consider all possibilities. If the intersection between wj (defined in Step 2) and the negation of the question is not empty at least in one possibility, the original proposition is false. Otherwise, the original proposition is true.\n\nAnswer:",
        }
    ],
    stop=["<|im_start|>", "<|im_end|>", "<|endoftext|>"],
    stream=True,
    n=1,
    top_p=1,
    top_k=40,
    presence_penalty=0,
    frequency_penalty=0,
    prompt_truncate_len=1024,
    context_length_exceeded_behavior="truncate",
    temperature=0.9,
    max_tokens=4000,
)

#Reference

• Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning (06 February 2024)