Almost Sure Reasoning: Generating Verified Formalizations with Language Models and Logical Solvers
Automated Reasoning;SAT/SMT Solvers;Formal Methods;Large Language Models
Yes
No ethics review needed.
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.
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.
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.
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.
Yes
No ethics review needed.
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.
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.
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.
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).
Yes
No ethics review needed.
I'd ask the authors to elaborate and possibly reply to weaknesses (3) and (4) above.
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.
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.
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.
Yes
No ethics review needed.
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?
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.
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.
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.
A novel approach to combining language models with logical solvers that advances accuracy of reasoning and also provides a verification mechanism with near-perfect precision.
@inproceedings{
anonymous2024almost,
title={Almost Sure Reasoning: Generating Verified Formalizations with Language Models and Logical Solvers},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=aNf8VCQE0h},
note={under review}
}
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 $\textit{near-perfect}$ precision over a significant coverage of cases, as we demonstrate on open reasoning benchmarks. We propose such $\textit{almost sure 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.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
Automated Reasoning SAT/SMT Solvers Formal Methods Large Language Models
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/35b52a7569d7fe3245598b788373560f33a9dc1a.pdf
neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
Almost Sure Reasoning: Generating Verified Formalizations with Language Models and Logical Solvers
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission