STEP 1: Selective translation (CSTM Module)

Input → Structural filter → selects sentences with explicit 
logical patterns (if-then, and/or, quantifiers, predicates) → 
Semantic verifier → checks that the meaning survives translation → 
if confidence is high: logical formula (FOL) 
if confidence is low: natural-language text → 
Hybrid context: {logical formulas} + {text}

STEP 2: Backward reasoning (HBRM Module)
Runs in a single prompt, but iteratively (up to k steps):

Hypothesis H = "conclusion C is true" → 
Find support: which premises from the hybrid context P' support H? → 
Verify the step: are there logical errors? → 
if it contradicts P' → False
if support is found in P' → True  
if unclear → H = a new sub-hypothesis, repeat
if the step limit is reached → Unknown

Task: You're assessing whether a startup fits the criteria of a small-business innovation grant program (SBIR-style). There are formal requirements (company age, team size, field) and subjective ones (innovativeness, demand) — you need to determine whether it qualifies.

Prompt:

I'll give you the selection criteria for a grant and information about a startup. 
The task is to determine whether the project qualifies.

Use backward reasoning: start from the hypothesis "the project qualifies", 
then check which criteria support or refute it.

When analyzing:
- Translate clear numeric and formal conditions into logical formulas
- Leave subjective wording ("innovativeness", "potential") 
  as text and analyze it semantically
- For each criterion, show whether it's met based on the project data

GRANT CRITERIA:
1. Company is no more than 3 years old
2. Team size between 2 and 10 people
3. Field: technological innovation (AI, biotech, cleantech)
4. Has a prototype or MVP
5. Validated customer demand

PROJECT DATA:
- The company was incorporated in 2022
- The team has 5 people
- Building an AI service that automates bookkeeping
- Has a working MVP with 3 pilot customers
- Positive feedback from customers, but no payments yet

Result:

The model will produce a hybrid analysis: it translates the numeric criteria (age ≤ 3 years, team of 2-10 people) into formulas and checks them precisely, concluding "met"; it matches the field (AI) against the list of technologies; and it leaves the subjective parts ("innovativeness," "validated demand") as text and gives a contextual assessment.

You'll see the backward flow of reasoning: "if the project qualifies → criteria 1, 2, 3, 4 must hold → the check shows they're met → but criterion 5 is debatable (there's interest, but no payments) → a final decision with an explanation of the risk area." Instead of going through every fact in order, the model moves purposefully from the conclusion to the confirmations it needs.

LLMs are bad at goal-directed search across many premises — they go through everything in turn, generating redundant steps. In forward reasoning the model doesn't "keep the end goal in mind" and can wander off, especially when there are lots of irrelevant facts. Backward reasoning sets a clear anchor: the conclusion is known, and you only need to find what supports it — that narrows the search space and cuts the noise.

LLMs are good at generating from a pattern and checking for a match. The format "if X is true, what must support it?" creates a directed filter: the model picks the relevant facts instead of going through all of them. Plus the hybrid format (logic + text) removes translation errors where the meaning is fuzzy — the model doesn't break the semantics by trying to cram everything into formulas.

The method uses double verification: semantic (during translation) and logical (during reasoning). Every translation into a formula is checked to make sure the meaning survives; every reasoning step is checked for logical errors. This blocks errors from compounding: if a translation is uncertain → the text stays; if a step is wrong → it gets rebuilt.

Prompt control knobs:

• The condition for translating into logic — you can tighten it ("only explicit if-then and numbers") or loosen it ("translate more patterns") → a balance between precision and flexibility. For math and code, formalize more; for business context, leave more as text.

• Depth of the backward search — how many iterations back from the conclusion are allowed (the parameter k in the algorithm). For simple tasks 2-3 is enough; for complex multi-step ones you can go to 5-7. Fewer steps = saved tokens, but a risk of "Unknown" on deep logic.

• Exit criteria — "support found / contradiction / unclear" can be extended with a confidence threshold or a requirement for several independent confirmations → stricter for critical decisions.

• Typing the conditions — instead of an abstract "translate the clear parts," give the model a list of types (numeric → inequalities, logical connectives → implications, contextual → text) → more precise control over which parts get formalized.

Task: {description of a task with logical conditions}

Use backward reasoning:
1. Start from the hypothesis: {desired conclusion}
2. Determine which premises must be true for the hypothesis to hold
3. Check each premise against the data: {data to analyze}

Rules for translating into logic:
- Numeric and clear-cut conditions (age, quantity, if-then) → formalize as 
  logical formulas or inequalities
- Subjective and contextual criteria (innovativeness, potential, 
  quality) → leave as text and analyze semantically
- Check every translation into logic: is the meaning preserved? If unsure → leave it as text

Conditions:
{list of conditions/criteria}

Data:
{source information}

For each condition, show:
- The formalized form (if applicable) or the text form
- Whether it holds based on the data
- Whether it supports or refutes the hypothesis

Final conclusion: the hypothesis is {true / false / unclear} + justification.

Placeholders: - {task description} — what needs to be determined or proven - {desired conclusion} — the statement being tested (e.g., "the project meets the criteria") - {data to analyze} — facts, conditions, inputs - {list of conditions/criteria} — formal requirements or logical rules - {source information} — specific data about the situation/subject

🚀 Quick start — paste this into the chat:

Here's a template for backward logical reasoning (HBLR). Adapt it to my task: 
[your task]. Ask me questions to fill in the fields.

[paste the template above]

The LLM will ask which conclusion you want to test and what conditions and data you have — because backward reasoning is built from the goal to the premises, and it needs to understand the structure of the task. It will take the "hypothesis → find support → hybrid analysis" pattern and adapt it to your context.

⚠️ Simple tasks: If the conclusion follows directly from a single premise, backward reasoning is overkill. The method is built for multi-step logic; for a simple "A → B," regular CoT is faster and simpler.

⚠️ Subjective criteria: The method works best where there's a clear logical structure — at least partially. If the whole task is about judging creative work or emotional tone with no formal criteria, formalization won't help, and the backward flow won't beat ordinary reasoning.

⚠️ Weaker models: On GPT-3.5-Turbo the method sometimes loses to Logic-LM with an external solver (e.g., on LogicalDeduction) — the model handles the translation but gets stuck on complex reasoning. For reliable results you need a GPT-4-class model or better, capable of multi-step hypothesis checking.

The team tested the method on five logical reasoning datasets: from synthetic ones (ProntoQA, ProofWriter with clear templates) to hard human-written ones (FOLIO, AR-LSAT with implicit logic and varied language). They tested on four models of different strength — from GPT-3.5 to DeepSeek-R1. They compared against four baselines: Direct (a direct answer without reasoning), CoT (step-by-step forward reasoning), Logic-LM (full translation into logic + an external solver), SymbCoT (full translation + LLM reasoning).

First they checked translation accuracy into logic: models handle templated datasets well (90%+ on ProntoQA) but make mistakes on natural text (73-74% on FOLIO and AR-LSAT) — which is exactly what motivated the selective strategy. Then they analyzed the redundancy of forward reasoning: they took GPT-4's correct answers and removed all unnecessary steps, leaving only the essential logical chain — it turned out most of the tokens go to sifting through irrelevant premises.

HBLR beat every baseline on accuracy: on GPT-4 the gain was up to +36.74% vs Direct and up to +10% vs the closest competitors (Logic-LM, SymbCoT). The trend held across all models except one case: GPT-3.5 on LogicalDeduction lost to Logic-LM — the weaker model can't handle complex reasoning, and the solver takes over that work. A surprising result: on the strongest model (DeepSeek-R1), CoT outperforms the symbolic methods Logic-LM and SymbCoT — apparently powerful models suffer from the noise of full formalization, and their built-in reasoning is more effective than crudely translating the whole text into logic. HBLR minimizes that noise with its selective approach.

The final check: they compared selective translation (HBLR) against two extremes — full translation into logic (All-FOL) and no formalization at all (All-NL). Selective translation won by 7.2% over text and by 4.7% over full logic — confirming that the hybrid works better. In practice HBLR leaves an average of 15.74% of the input as text, but on FOLIO and AR-LSAT that figure is higher (21-37%) — exactly where translation proved especially unreliable in the first experiment.

🔧 Technique: Controlling the depth of the backward search → savings on simple tasks

If the task isn't hard, limit the number of iterations back from the conclusion. Add to the prompt:

At most {N} steps back from the hypothesis. If after {N} iterations you haven't found 
support or a contradiction, answer "unclear" and state what's missing.

For simple tasks set N=2-3; for complex multi-step ones, 5-7. This saves tokens and speeds up the answer where a deep chain isn't needed.

🔧 Technique: Explicitly typing the conditions → tighter control of the hybrid

Instead of an abstract "only translate the clear parts," give the model a list of condition types:

Condition types:
- Numeric (age, quantity, dates) → formalize as inequalities or ranges
- Logical connectives (if-then, and, or, not) → formalize as implications and conjunctions  
- Predicates with clear parameters → formalize as functions
- Contextual (innovativeness, quality, fit with the spirit of the rules) → leave as text

For each condition, state its type and the form of analysis (formula or text).

This gives you more control: you explicitly decide what to formalize and what not to. Useful for mixed tasks (business + law, engineering + ethics).

🔧 Technique: Combining with Tree-of-Thought at forks → checking alternatives

If at some step of the backward search several possible premises could support the hypothesis, branch out:

At step {i} there are two possible branches supporting the hypothesis:
- Branch A: {premise_1}  
- Branch B: {premise_2}

Check both in parallel:
- If either one leads to a contradiction → that branch is false
- If both are confirmed → the hypothesis is proven by two independent paths (stronger)  
- If both are unclear → the final conclusion is "unclear"

Show the result for each branch separately, then the overall conclusion.

This is Tree-of-Thought inside backward reasoning — useful for tasks with ambiguous logic or several possible justifications.

"From Hypothesis to Premises: LLM-based Backward Logical Reasoning with Selective Symbolic Translation" — references Chain-of-Thought (Wei et al. 2022), Tree of Thoughts (Yao et al. 2023), Logic-LM (Pan et al. 2023), SymbCoT (Xu et al. 2024), the Prover9 prover, the Z3 solver, and the PyKE constraint solver.

Code: https://github.com/wufeiwuwoshihua/HBLR

Authors: Qingchuan Li, Mingyue Cheng, Zirui Liu, Daoyu Wang, Yuting Zeng, Tongxuan Liu — University of Science and Technology of China, JD.com.