Challenge: Existing proof generation tasks require reasoning capabilities, but they usually just request for an answer without the reasoning procedure that would make it interpretable.
Approach: They propose an iterative backward reasoning model to solve the proof generation tasks on rule-based Question Answering.
Outcome: The proposed model improves in-domain performance and cross-domain transferability over existing models.

Similar Papers

BC-Prover: Backward Chaining Prover for Formal Theorem Proving (2024.emnlp-main)

Copied to clipboard

Challenge: Existing methods for interactive theorem proving in formal logic lack robustness and robustness.
Approach: They propose a backward chaining framework guided by pseudo steps for proofstep generation that prioritizes pseudo steps.
Outcome: The proposed framework improves on the miniF2F benchmark.
PRover: Proof Generation for Interpretable Reasoning over Rules (2020.emnlp-main)

Copied to clipboard

Challenge: Recent work shows that transformers can act as “soft theorem provers” by answering questions over explicitly provided knowledge in natural language.
Approach: They propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs.
Outcome: The proposed model generates proofs with an accuracy of 87% while maintaining or improving performance on the QA task.
ProofInfer: Generating Proof via Iterative Hierarchical Inference (2022.emnlp-main)

Copied to clipboard

Challenge: Existing proof generation models focus on generating several proof paths instead of a whole tree.
Approach: They propose a method that generates the proof tree via iterative hierarchical inference . they propose coding the proof as plain text without losing structure information .
Outcome: The proposed proof generation model significantly improves performance on widely-used datasets.
Exploring Backward Reasoning in Large Language Models (2025.findings-naacl)

Copied to clipboard

Challenge: Multi-step reasoning through in-context learning strategies have been extensively explored, highlighting the abilities of Large Language Models (LLMs) to solve problems in a step-wise manner.
Approach: They propose to use Large Language Models to generate answers from step-by-step reasoning by re-constructing the original question that led to the final answer.
Outcome: The proposed models show that they are able to reason about the conclusion and reconstruct the original question that led to the final answer.
Forward-Backward Reasoning in Large Language Models for Mathematical Verification (2024.findings-acl)

Copied to clipboard

Challenge: Extensive experiments on six standard mathematical data sets and three LLMs show that FOBAR achieves state-of-the-art performance.
Approach: They propose to combine forward and backward reasoning to verify candidate answers . they propose to use a template to mask a number and ask the LLM to answer a backward question .
Outcome: Experiments on mathematical data show that proposed backward reasoning outperforms Self-Consistency.
LAMBADA: Backward Chaining for Automated Reasoning in Natural Language (2023.acl-long)

Copied to clipboard

Challenge: Recent advances in automated reasoning with natural text suffer from a combinatorial explosion of the search space and high failure rates for problems requiring longer chains of reasoning.
Approach: They propose a Backward Chaining algorithm that decomposes reasoning into four sub-modules and implements it by few-shot prompted LLM inference.
Outcome: The proposed algorithm achieves sizable accuracy boosts over state-of-the-art forward reasoning methods on two challenging logical reasoning datasets.
BackMATH: Towards Backward Reasoning for Solving Math Problems Step by Step (2025.coling-industry)

Copied to clipboard

Challenge: Large language models (LLMs) have impressive results in reasoning, but when faced with more complex mathematical problems, performance drops significantly.
Approach: They propose a backward reasoning dataset that includes 14K backward thinking problems and 100K reasoning steps.
Outcome: The proposed model achieves an accuracy of 68.1% on the GSM8K dataset and 21.9% on the MATH dataset, exceeding the SOTA by 1.6% and 2.1% respectively.
FRVA: Fact-Retrieval and Verification Augmented Entailment Tree Generation for Explainable Question Answering (2024.findings-acl)

Copied to clipboard

Challenge: Existing methods for generating a entailment tree exhibit the reasoning chains from knowledge facts to predicted answers, but they have large fact search spaces and error accumulation problems resulting in the generation of invalid steps.
Approach: They propose a Fact-Retrieval and Verification Augmented bidirectional entailment tree generation method that contains two systems.
Outcome: The proposed method outperforms existing models and achieves state-of-the-art performance in fact selection and structural correctness.
Natural Language Deduction with Incomplete Information (2022.emnlp-main)

Copied to clipboard

Challenge: Existing systems for reasoning given incomplete information are inadequate . current approaches to reasoning are based on latent reasoning by large language models .
Approach: They propose a system that generates a natural language "proof" by abductively inferring a premise from another premise and a conclusion.
Outcome: The proposed system can handle the underspecified setting where not all premises are stated at the outset; additional assumptions need to be materialized to prove a claim.
From Sentences to Proof Trees: Leveraging Language Models for Structured Reasoning (2026.eacl-srw)

Copied to clipboard

Challenge: Multi-hop reasoning requires a chain of facts to reflect the reasoning behind the answer.
Approach: They propose an inference-guided prompting approach that performs well in natural language questions . they propose a neuro-symbolic approach to reasoning using large language models .
Outcome: The proposed model outperforms all prompting strategies and fine-tunes LLMs trained specifically for proof generation.

What is GenGO?

GenGO is an NLP powered publication search system. It currenctly indexes 30k+ papers from ACL Anthology, and implements multi-aspect summarization, semantic search, and more!

Information

About
Limitations