Almost Sure Reasoning: Generating Verified Formalizations with Language Models and Logical Solvers

Authors: Mohammad Raza, Natasa Milic-Frayling
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
Keywords: Automated Reasoning, SAT/SMT Solvers, Formal Methods, Large Language Models

Abstract:
Robustness of reasoning remains a challenging problem for large language models, and addressing it is crucial for advancing the reliability and practical application 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 translate the reasoning problem from natural language to the formal language of the solver. SSV produces strong abstract formalizations of problems  by verifying and refining them against 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 $\textit{near-certain reasoning}$ as a new approach that can reduce the need for manual human verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.

Decision: reject
Reviewer scores: 6, 5, 3, 6

Reviews and discussion:
<thread>
creation date:
1730697153059

thread_type:
official_review

<thread_object>
creator: reviewer_gmco

<content>
summary:
This paper considers the problem of autoformalization of natural language queries for use in with formal methods, e.g. automata theorem provers and SMT solvers. This work extends existing works on proposer/verifier LLM architectures by having the LLM generate both the autoformalization and the concrete instantiations (unit tests). These tests act to guide to correct the autoformalization. The paper then validates the approach and empirically finds this to be a successful addition to the LLM toolbox.

strengths:
1. The addressed problem of autoformalization is interesting and the potential benefits are clear: improved reasoning and synthesis using formal methods.

2. The presentation is clear and easy to follow. The core idea is summarized and illustrated well.

3. The two key ideas of adding concrete instantiations to check against and adding a feedback signal of whether the answer was verified are simple and applicable to a wide number of domains. In particular, while simple, this idea does differentiate itself from a number of AI systems papers targeting autoformalization via the proposer/verifier pattern.

4, The empirical benchmarks show a clear improvement over the baselines.

5. The limitations does a good job of outlining the limits, particularly in problems that cannot be identified with a finite number of concrete instances.

weaknesses:
1. The approach appears to be a simple extension of the proposer/verifier pattern -- Although I think many great ideas can be small / surgical modifications to existing approaches / frameworks.

2. Perhaps I'm missing something, but it's unclear from the draft how many concrete instantiations are necessary or if tuning this is important. For example, I can imagine a trade off where too many might increase the likelihood of an incorrect example slipping in. Conversely too few do not exercise edge cases.

3. (minor) I must admit I do not like the language around almost sure reasoning. To me this sounds to much like "almost surely" "almost certainly", etc from probability theory. These have a precise meaning that if I understand the paper, this approach does not and can never have.

questions:
1. How many instances were generated per round.

2. In the limit of many instances, does it make sense to benchmark against passive learning algorithms for the concepts being tested?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730754828758

thread_type:
official_review

<thread_object>
creator: reviewer_hoje

<content>
summary:
This paper introduces Semantic Self-Verification (SSV), a method to combine large language models (LLMs) with logical solvers. Specifically, the LLM is used to infer a formal representation of the problem that can then be solved by the solver.

strengths:
The main contributions of Semantic Self-Verification (SSV) are summarized by the authors as follows:

1) It improves the overall accuracy of reasoning significantly over SoTA.
2) It provides a novel feature of verification that has near-perfect precision.

weaknesses:
1) The introduction is 4 pages, which is perhaps too much for a paper which is 10 pages in total. 
For instance, on p. 3 there is a long example, which is hard to appreciate if one doesn't already know the details of the proposed method.

2) The discussion in the paper is always rather informal, so it often hard to understand what is going one. For instance, on p. 5 the authors say that "our program generation phase creates programs with an explicit structure P_init + C_1... + C_N + O_1 + ... + O_M", where P_init is the initial definitions segment, and the Cs and Os are constraints and options. However, the form of these constraints and options is not specified. 

3) Related to the previous point, it is not clear to which kind of problems we can apply the method proposed in this submission. Are the authors claiming that their methods applies to any problem that can be passed to an LLM? The limitations (if any) of SSV are never really discussed in the paper.

4) Overall the contribution seems a bit generic and limited to the SSV algorithm. But basically any LLMs can be considered, any benchmark, and possibly any solver.
One is left wondering what is the actual contribution of the paper.

questions:
I'd ask the authors to elaborate and possibly reply to weaknesses (3) and (4) above.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730834484831

thread_type:
official_review

<thread_object>
creator: reviewer_9aes

<content>
summary:
The paper presents a new method called Semantic Self-Verification (SSV), designed to improve the reliability of AI reasoning by combining LLMs with logical solvers for semantic in-context feedback. Previous AI reasoning often relies solely on LLMs, which can make mistakes, especially on complex problems. SSV addresses this by having the LLM translate a problem into a formal logical representation, then using a logical solver to verify that the translation accurately reflects the problem's constraints.

SSV does this by generating concrete instantiations or specific examples, that test each rule or constraint in the problem. For instance, if a rule says "Stacy and Yolanda cannot repair the same machines," SSV will create scenarios where this rule is both upheld and violated, then use the solver to confirm that the rule is consistently applied across these cases. If an answer option satisfies all constraints under these test cases, SSV flags it as "verified". In experiments on complex reasoning benchmarks, such as those from law and logic exams, SSV achieved significantly higher accuracy than existing approaches. This method not only improves accuracy but also helps reduce the need for human intervention in verifying answers, especially on high-confidence cases.

strengths:
1. SSV introduces an interesting approach by generating concrete examples to verify the logical accuracy of language model outputs, rather than relying on the model’s abstract reasoning. 
2. The method achieves near-perfect precision on verified cases, meaning it is highly reliable for a subset of answers.

weaknesses:
1. My main concern is the novelty aspect. Its main innovation is the concrete instantiation, that seems like an incremental improvement on the established method of combining LLMs with logical solvers. The use of counter-example guided feedback, in which semantic verification is conducted through a solver, has been explored in other reasoning tasks, such as in Stechly et al. [1], which examines the self-verification limitations of LLMs in reasoning and planning, and in Jia et al. [2], which explores counter-example guided feedback in material discovery tasks.
2. SSV’s success relies heavily on the LLM's ability to produce accurate formal representations and concrete instantiations, which can vary in quality, particularly on ambiguous tasks. This has also been addressed in the limitations section, but it still remains an important concern.
3. While SSV is precise in verified cases, the coverage is relatively low on challenging datasets (e.g., AR-LSAT). This limited coverage raises questions about the method's practicality, as it may leave many complex cases unverifiable. 
4. The paper could improve by providing a more detailed analysis of cases where SSV fails verification. Understanding common sources of error could help readers evaluate the limitations more clearly.

Minor formatting issues:
1. Latex formatting issues: Use `` for opening quotes - ``Gary is nice.”
2. For references, write “we use the same datasets as in Pan et al. (2023)” and apply ~\cite{} instead of ~\citep{} for such cases.

[1] Stechly, Kaya, Karthik Valmeekam, and Subbarao Kambhampati. "On the self-verification limitations of large language models on reasoning and planning tasks." arXiv preprint arXiv:2402.08115 (2024).
[2] Jia, Shuyi, Chao Zhang, and Victor Fung. "LLMatDesign: Autonomous Materials Discovery with Large Language Models." arXiv preprint arXiv:2406.13163 (2024).

questions:
The paper covers several limitations, such as the difficulty of verifying natural language accurately and how errors might occur if examples are not comprehensive. Moreover, SSV may struggle with large, unstructured data, high computational costs, and performance variations with different language models. Additionally, its ability to verify complex or ambiguous language is limited, and its effectiveness outside formal logic tasks is still uncertain.

It would be great if the authors can address the concerns raised above as well as in the Weaknesses section.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730904624778

thread_type:
official_review

<thread_object>
creator: reviewer_sw9f

<content>
summary:
The authors propose SSV, a new reasoning approach to achieve "near-prefect" reasoning in LLMs using SMT solvers.
In their approach, the authors convert a query of text into a format readable by the Z3 theorem prover. They achieve this by converting each constraint from natural language (NL) to Z3 queries separately using an LLM. They then generate instances of the constraint in NL and also convert that to Z3 using an LLM. They use these as a sanity check to see whether the conversion was correct (although this is not guaranteed as pointed out by the authors). Once all of the constrainst are in place, the SMT solver will determine the solution.

strengths:
The authors did a good job in keeping everything at a high level. From the writing and the examples, it is immidiately clear how they intend to mix LLMs with SMT solving using only high-level interfaces. The results also show that this approach has quite some potential, showing high precision. I also appreciate the attempt to incorporate SMT solvers into LLMs for better reasoning.

weaknesses:
I would have liked to see more about performance. SMT solvers are known to be expensive in terms of required computational resources. Given that this approach uses the SMT solver in a nested loop, makes me question how scalable this is.

Furthermore, I am convinced that this will indeed work most of the time given that the entire context is given in text. However, if part of the reasoning is based on hidden but trivial facts, then the SMT solver will not know about these. I suspect that LLMs may generally be more accurate here, because they do have that context. E.g. how would this approach answer to this (or similar) query: "Urma is on earth. Urma releases a glass of water. What happens next? A. The glass falls. B The glass hovers in the air." GPT 3.5 is able to answer A and that the glass will fall because of gravity which is present due to Urma being on Earth, but the SMT solver does not have this context. I am not sure if this can be solved using the authors' approach. In that sense the author's approach is a natural language parser for an SMT solver that can attempt to self-repair the parsing when a counterexample is identified. I am not convinced that this approach contributes to "logical reasoning in LLMs" because one loses this context that is an essential feature of LLMs in my opinion.

questions:
Specific comments:

Performance in terms of runtime

Work on the phrasing of your contribution. While this is a noteworthy paper, I think it should not be sold as contributing to logical reasoning in LLMs because I do not think that this holds for this approach. It is a more reliable parser from NL to SMT in my opinion.

Figure 2: What does it mean that the solver verification fails or succeeds for an initialization? To me it is unclear why one fails while the other does not. One or two lines on that would be appreciated.

Figure 4:   Line 6 states that we take the first answer to find as the best one, this does not make sense to me. I would say that an answer which has seen more counterexamples would be mopre trustworthy.
            Line 10 checks that P is well formed, why do we not check that before line 5?

257. "demarcated in explicit segments along with their NL descriptions (from the original problem) stated as comments." Add reference to Figure 1 for readability, at this point I had forgotten what constraints and options are.

348. Main results using GPT 4.0?

473. Related work: There are some papers explicitly on SMT solvers and LLMs (that I am not familiar with). I would have expected to see a comparison explicitly to these papers as well.
</content>
</thread_object>

</thread>
<thread>
creation date:
1733050111546

thread_type:
official_comment

<thread_object>
creator: authors

<content>
comment:
We sincerely thank the reviewers for the very valuable discussion. It has greatly helped to emphasize the distinctive contribution of this work in many important dimensions:

- **Unprecedented Verification Feature.** We have introduced a novel verification feature where the system guarantees answer correctness with near-perfect certainty (100% correctness on standard benchmarks). No prior work in natural language reasoning has provided such a capability (to the best of our knowledge).

- **Strong Empirical Advancement.** Apart from the near-certain verification, we have significantly advanced answer accuracy on reasoning tasks above SoTA approaches consistently over standard reasoning benchmarks, and in particular from 43% to 71% on the most challenging law school tests benchmark.

- **Core Conceptual Novelty.** In contrast to the standard proposer-verifier paradigm where formal verifiers can be used to check *correctness* in formal problem task domains (which is inherently impossible in our informal-to-formal setting), we show how one can leverage *consistency* between abstract and concrete inferences to use formal verifiers for informal-to-formal prediction tasks. This novel consistency-based paradigm provides near-certain correctness where full correctness is impossible.

Apart from the significant concrete advancements, these novel contributions establish a new research direction: aiming for near-certain verification in natural language reasoning using formal methods, which is an orthogonal and complementary direction to the ongoing focus on only improving answer accuracy. We hope that the foundational nature of these contributions and their potential to inspire future research can be recognized.
</content>
</thread_object>

</thread>
<thread>
creation date:
1739081065012

thread_type:
public_comment

<thread_object>
creator: ~mohammad_raza1

<content>
title:
Misrepresentation in the meta-review summary

comment:
Thank you again to all the reviewers for their time and feedback. To avoid potential confusions, we want to clarify that there is a significant misrepresentation of this work in the meta-review summary:

*"This paper combines LLMs with logical solvers, where the LLM is set to present a formal representation of a problem to a (SMT) solver. The core motivation is to shift the responsibility of the full reasoning from the LLM to the solver."*

This describes exactly the existing baseline works (e.g., Pan et al. EMNLP’23, Ye et al. NeurIPS’23) and does not reflect the new contribution of this work. This paper instead addresses a key limitation of such LLM+solver approaches: that the LLM very often generates the wrong problem formalization. It proposes a novel method that leverages solver-based consistency between abstract and concrete inferences by the LLM to address this issue.
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper combines LLMs with logical solvers, where the LLM is set to present a formal representation of a problem to a (SMT) solver. The core motivation is to shift the responsibility of the full reasoning from the LLM to the solver. 

While the reviewers generally agree that the paper provides a good idea, all reviewers also agree that the contribution is rather small and in the current state of the paper presented too boldly. The authors are encouraged to sharpen the message to the actual technical contribution. In the current form, the paper cannot be accepted.