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

TL;DR

This paper introduces Semantic Self-Verification (SSV), a novel method combining language models and logical solvers to improve reasoning accuracy and reliability through formal problem formulation and verification.

Contribution

The paper presents SSV, a new consistency-based approach that enhances reasoning accuracy and introduces near-certain reasoning to reduce manual verification needs.

Findings

Significantly improves reasoning accuracy over state-of-the-art methods.

Achieves near-perfect precision in verification across many cases.

Demonstrates effectiveness on open reasoning benchmarks.

Abstract

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.