# Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 30 of its 40 references that are in the map.
- First posted on arXiv 28 Jan 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

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

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models](https://mlsanity.com/paper/2206.04615/) (2022)
- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [Decomposed Prompting: A Modular Approach for Solving Complex Tasks](https://mlsanity.com/paper/2210.02406/) (2022)
- [DIN-SQL: Decomposed In-Context Learning of Text-to-SQL with Self-Correction](https://mlsanity.com/paper/2304.11015/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Large Language Models are Better Reasoners with Self-Verification](https://mlsanity.com/paper/2212.09561/) (2022)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [Leveraging Pre-trained Large Language Models to Construct and Utilize World Models for Model-based Task Planning](https://mlsanity.com/paper/2305.14909/) (2023)
- [Self-Evaluation Guided Beam Search for Reasoning](https://mlsanity.com/paper/2305.00633/) (2023)
- [An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation](https://mlsanity.com/paper/2302.06527/) (2023)
- [SelfCheck: Using LLMs to Zero-Shot Check Their Own Step-by-Step Reasoning](https://mlsanity.com/paper/2308.00436/) (2023)
- [Solving Math Word Problems by Combining Language Models With Symbolic Solvers](https://mlsanity.com/paper/2304.09102/) (2023)
- [Deductive Verification of Chain-of-Thought Reasoning](https://mlsanity.com/paper/2306.03872/) (2023)
- [Can Large Language Models Really Improve by Self-critiquing Their Own Plans?](https://mlsanity.com/paper/2310.08118/) (2023)
- [Improving Coherence and Consistency in Neural Sequence Models with Dual-System, Neuro-Symbolic Reasoning](https://mlsanity.com/paper/2107.02794/) (2021)
- [Generating Natural Language Proofs with Verifier-Guided Search](https://mlsanity.com/paper/2205.12443/) (2022)
- [Entailer: Answering Questions with Faithful and Truthful Chains of Reasoning](https://mlsanity.com/paper/2210.12217/) (2022)
- [Thought Propagation: An Analogical Approach to Complex Reasoning with Large Language Models](https://mlsanity.com/paper/2310.03965/) (2023)
- [LLM-ARC: Enhancing LLMs with an Automated Reasoning Critic](https://mlsanity.com/paper/2406.17663/) (2024)

## Built on by (most cited first, 7 of 7)

- [Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Models](https://mlsanity.com/paper/2503.09567/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving](https://mlsanity.com/paper/2505.20869/) (2025)
- [Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis](https://mlsanity.com/paper/2601.06181/) (2026)
- [VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification](https://mlsanity.com/paper/2607.20474/) (2026)
- [Reasoning Systems as Structured Processes: Foundations, Failures, and Formal Criteria](https://mlsanity.com/paper/2508.01763/) (2025)

## Abstract (arXiv)

Robustness of reasoning remains a significant challenge for large language models, and addressing it is essential for the practical applicability of AI-driven reasoning systems. We introduce Semantic Self-Verification (SSV), a novel approach that addresses the key challenge in combining language models with the rigor of logical solvers: to accurately formulate the reasoning problem from natural language to the formal language of the solver. SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver. In addition to significantly advancing the overall reasoning accuracy over the state-of-the-art, a key novelty that this approach presents is a feature of verification that has near-perfect precision over a significant coverage of cases, as we demonstrate on open reasoning benchmarks. We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.