# Generating Natural Language Proofs with Verifier-Guided Search

arXiv: https://arxiv.org/abs/2205.12443 · HTML: https://mlsanity.com/paper/2205.12443/

## Key facts

- Cited by 52 papers in the map (data through 14 Oct 2026).
- Builds on 45 of its 70 references that are in the map.
- First posted on arXiv 25 May 2022.

## Builds on (most cited first, 30 of 45)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [RoBERTa: A Robustly Optimized BERT Pretraining Approach](https://mlsanity.com/paper/1907.11692/) (2019)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [HotpotQA: A Dataset for Diverse, Explainable Multi-hop Question Answering](https://mlsanity.com/paper/1809.09600/) (2018)
- [A large annotated corpus for learning natural language inference](https://mlsanity.com/paper/1508.05326/) (2015)
- [Leveraging Passage Retrieval with Generative Models for Open Domain Question Answering](https://mlsanity.com/paper/2007.01282/) (2020)
- [BLEURT: Learning Robust Metrics for Text Generation](https://mlsanity.com/paper/2004.04696/) (2020)
- [Scaling Language Models: Methods, Analysis & Insights from Training Gopher](https://mlsanity.com/paper/2112.11446/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Diverse Beam Search: Decoding Diverse Solutions from Neural Sequence Models](https://mlsanity.com/paper/1610.02424/) (2016)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [HoVer: A Dataset for Many-Hop Fact Extraction And Claim Verification](https://mlsanity.com/paper/2011.03088/) (2020)
- [CLUTRR: A Diagnostic Benchmark for Inductive Reasoning from Text](https://mlsanity.com/paper/1908.06177/) (2019)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [Multi-hop Reading Comprehension through Question Decomposition and Rescoring](https://mlsanity.com/paper/1906.02916/) (2019)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [A Benchmark for Systematic Generalization in Grounded Language Understanding](https://mlsanity.com/paper/2003.05161/) (2020)
- [PRover: Proof Generation for Interpretable Reasoning over Rules](https://mlsanity.com/paper/2010.02830/) (2020)
- [ProoFVer: Natural Logic Theorem Proving for Fact Verification](https://mlsanity.com/paper/2108.11357/) (2021)
- [Measuring Systematic Generalization in Neural Proof Generation with Transformers](https://mlsanity.com/paper/2009.14786/) (2020)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [NLProlog: Reasoning with Weak Unification for Question Answering in Natural Language](https://mlsanity.com/paper/1906.06187/) (2019)
- [Natural Language Deduction through Search over Statement Compositions](https://mlsanity.com/paper/2201.06028/) (2022)
- [FaiRR: Faithful and Robust Deductive Reasoning over Natural Language](https://mlsanity.com/paper/2203.10261/) (2022)
- [Flexible Generation of Natural Language Deductions](https://mlsanity.com/paper/2104.08825/) (2021)

## Built on by (most cited first, 30 of 52)

- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs](https://mlsanity.com/paper/2406.01297/) (2024)
- [Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategies](https://mlsanity.com/paper/2308.03188/) (2023)
- [Deductive Verification of Chain-of-Thought Reasoning](https://mlsanity.com/paper/2306.03872/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Evaluating Step-by-step Reasoning Traces: A Survey](https://mlsanity.com/paper/2502.12289/) (2025)
- [Natural Language Reasoning, A Survey](https://mlsanity.com/paper/2303.14725/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Physics of Language Models: Part 2.2, How to Learn From Mistakes on Grade-School Math Problems](https://mlsanity.com/paper/2408.16293/) (2024)
- [Reasoning in Token Economies: Budget-Aware Evaluation of LLM Reasoning Strategies](https://mlsanity.com/paper/2406.06461/) (2024)
- [Vera: A General-Purpose Plausibility Estimation Model for Commonsense Statements](https://mlsanity.com/paper/2305.03695/) (2023)
- [Entailer: Answering Questions with Faithful and Truthful Chains of Reasoning](https://mlsanity.com/paper/2210.12217/) (2022)
- [Ever: Mitigating Hallucination in Large Language Models through Real-Time Verification and Rectification](https://mlsanity.com/paper/2311.09114/) (2023)
- [GRACE: Discriminator-Guided Chain-of-Thought Reasoning](https://mlsanity.com/paper/2305.14934/) (2023)
- [Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models](https://mlsanity.com/paper/2310.00836/) (2023)
- [Language Models as Inductive Reasoners](https://mlsanity.com/paper/2212.10923/) (2022)
- [Logical Reasoning over Natural Language as Knowledge Representation: A Survey](https://mlsanity.com/paper/2303.12023/) (2023)
- [Language Models can be Logical Solvers](https://mlsanity.com/paper/2311.06158/) (2023)
- [HumanEvalComm: Benchmarking the Communication Competence of Code Generation for LLMs and LLM Agent](https://mlsanity.com/paper/2406.00215/) (2024)
- [RECKONING: Reasoning through Dynamic Knowledge Encoding](https://mlsanity.com/paper/2305.06349/) (2023)
- [Learning Deductive Reasoning from Synthetic Corpus based on Formal Logic](https://mlsanity.com/paper/2308.07336/) (2023)
- [Dissecting Logical Reasoning in LLMs: A Fine-Grained Evaluation and Supervision Study](https://mlsanity.com/paper/2506.04810/) (2025)
- [NELLIE: A Neuro-Symbolic Inference Engine for Grounded, Compositional, and Explainable Reasoning](https://mlsanity.com/paper/2209.07662/) (2022)
- [Faithful Question Answering with Monte-Carlo Planning](https://mlsanity.com/paper/2305.02556/) (2023)
- [Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement](https://mlsanity.com/paper/2402.00745/) (2024)
- [When Does Verification Pay Off? A Closer Look at LLMs as Solution Verifiers](https://mlsanity.com/paper/2512.02304/) (2025)
- [Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition](https://mlsanity.com/paper/2504.03930/) (2025)
- [Natural Language Deduction with Incomplete Information](https://mlsanity.com/paper/2211.00614/) (2022)
- [Enhancing Systematic Decompositional Natural Language Inference Using Informal Logic](https://mlsanity.com/paper/2402.14798/) (2024)
- [Learning and Leveraging Verifiers to Improve Planning Capabilities of Pre-trained Language Models](https://mlsanity.com/paper/2305.17077/) (2023)

## Abstract (arXiv)

Reasoning over natural language is a challenging problem in NLP. In this work, we focus on proof generation: Given a hypothesis and a set of supporting facts, the model generates a proof tree indicating how to derive the hypothesis from supporting facts. Compared to generating the entire proof in one shot, stepwise generation can better exploit the compositionality and generalize to longer proofs but has achieved limited success on real-world data. Existing stepwise methods struggle to generate proof steps that are both logically valid and relevant to the hypothesis. Instead, they tend to hallucinate invalid steps given the hypothesis. In this paper, we present a novel stepwise method, NLProofS (Natural Language Proof Search), which learns to generate relevant steps conditioning on the hypothesis. At the core of our approach, we train an independent verifier to check the validity of the proof steps to prevent hallucination. Instead of generating steps greedily, we search for proofs maximizing a global proof score judged by the verifier. NLProofS achieves state-of-the-art performance on EntailmentBank and RuleTaker. Specifically, it improves the correctness of predicted proofs from 27.7% to 33.3% in the distractor setting of EntailmentBank, demonstrating the effectiveness of NLProofS in generating challenging human-authored proofs.