TL;DR

• This is an indirect reasoning template: uses contrapositive and proof-by-contradiction to push the model toward more rigorous reasoning.
• Good for: mathematical proofs, logical derivations, and "proving a conclusion must hold" scenarios.
• The key to making it work: write the steps as an executable checklist, and do a self-check at the end (did it cover all cases? did it introduce unstated premises?).

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

You can use this template as a general scaffold for "proof-type tasks":

1. Break the original proposition into conditions and question
2. Merge conditions into a tighter set (the paper calls this wj)
3. During reasoning, explicitly consider the negation of the question, and use "is the intersection empty?" to check whether a counterexample can be constructed

Its value: it turns the model's freestyling into a "must follow these steps" reasoning flow, reducing step-skipping and concept-swapping.

How to Iterate

1. Structure Step 1's output: require listing Given / To Prove
2. Require listing all cases (e.g., by sign, interval, boundary values)
3. Add verification at the end: check each step for hidden assumptions
4. Have the model output a "failure mode": if it can't prove it, point out where it's stuck and what conditions are missing

Self-check Rubric

• Did it explicitly write the negation and use contradiction reasoning?
• Did it cover all possibilities / cases?
• Did it introduce premises not given in the problem?
• Is the reasoning chain self-consistent (no circular reasoning)?

Practice

Exercise: prove any of the following propositions using the same indirect reasoning template (or explain what conditions are missing):

• If a^2 is even, prove that a is even.
• If x + |x| = 0, prove that x <= 0.
• For any integer n, if n is divisible by 4, then n is even.

Prompt

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)

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)

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)