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. |
Similar Papers
Interpretable Proof Generation via Iterative Backward Reasoning (2022.naacl-main)
Copied to clipboard
| 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. |
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. |
Hierarchical Attention Generates Better Proofs (2025.acl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) have shown promise in formal theorem proving, but their token-level processing often fails to capture the inherent hierarchical nature of mathematical proofs. |
| Approach: | They propose a regularization method that aligns LLMs’ attention mechanisms with mathematical reasoning structures and establishes a five-level hierarchy from foundational elements to high-level concepts. |
| Outcome: | The proposed method improves proof success rates by 2.05% on miniF2F and 1.69% on ProofNet while reducing proof complexity by 23.81% and 16.50% respectively. |
multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning (2021.naacl-main)
Copied to clipboard
| Challenge: | Existing work to generate proof graphs for formal reasoning over explicit knowledge is not unique and there may be multiple ways of reaching the correct answer. |
| Approach: | They propose to generate multiple proof graphs for reasoning over natural language rules and facts . they propose to combine all proofs and exploit correlations between them . |
| Outcome: | The proposed model outperforms PRover on multiple gold proofs on synthetic, zero-shot, and human-paraphrased datasets. |
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. |
Think While You Write: Hypothesis Verification Promotes Faithful Knowledge-to-Text Generation (2024.findings-naacl)
Copied to clipboard
| Challenge: | Knowledge-to-text generators often struggle to faithfully generate descriptions for input facts . we propose a decoding-only method to reduce hallucinations . |
| Approach: | They propose a decoding-only method to generate accurate descriptions for input facts . they use a Natural Language Inference model as the model and replace it with a task-specific HVM . |
| Outcome: | The proposed method improves faithfulness with minimal impact on quality and in/out-of-distribution evaluations. |
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. |
Generating Natural Language Proofs with Verifier-Guided Search (2022.emnlp-main)
Copied to clipboard
| Challenge: | Existing stepwise methods struggle to generate valid proof steps based on the hypothesis . instead, they generate invalid steps . |
| Approach: | They propose a stepwise method which generates relevant steps conditioning on the hypothesis. |
| Outcome: | The proposed method improves correctness of predicted proofs from 27.7% to 33.3% on EntailmentBank and RuleTaker. |
ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language (2021.findings-acl)
Copied to clipboard
| Challenge: | Recent work shows that transformers can generate both implications of a theory and the natural language proofs that support them. |
| Approach: | They propose a generative model that generates both implications of a theory and natural language proofs that support them. |
| Outcome: | The proposed model generates both implications of a theory and the natural language proofs that support them. |
ProoFVer: Natural Logic Theorem Proving for Fact Verification (2022.tacl-1)
Copied to clipboard
| Challenge: | Recent fact verification systems rely on neural network classifiers for veracity prediction, which lack explainability. |
| Approach: | They propose a model that generates natural logic-based inferences as proofs using lexical mutations between spans in the claim and the evidence retrieved. |
| Outcome: | The proposed model has highest label accuracy and second best score in the FEVER leaderboard. |