Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization

Thank you for your constructive feedback and we address individual points below.

The originality and theoretical contribution of this paper is rather limited, as this is mainly the clever combination of two existing tools.

Thank you for your thoughts and we would like to provide some clarifications. Although the core components of DTV are indeed large language models and theorem provers in the formal environment, we disagree with the conclusion that the contribution of the paper is limited. Several other reviewers have expressed and liked the originality and simplicity of our approach. We also note that using theorem provers as a tool allows us to solve challenging problems with the rich formal math libraries that go beyond simple calculators. Additionally, we are the first to demonstrate it is possible to automatically verify correct informal solutions with autoformalization.

The experimental comparison is mainly wrt vanilla voting methods. Also, there is no explanation about the reasons of the particular approached selected for comparison, and there is no comparison with the numerous other methods mentioned in the related work.

Sorry it seems like there was a miscommunication. The main contribution of DTV is that we can select a correct solution from a set of candidates via verification with a theorem prover (and the LLM as “translator”). We obtain the candidates by sampling multiple solutions. A natural baseline is therefore to aggregate the candidates through majority voting (which is very competitive). Other methods [1,2,3,4], different from majority voting, would also benefit from DTV verification if they provide multiple candidates. We therefore consider such methods complementary to our contribution.

p. 3: Is it the case that every yes/no question is translated into a request for proof? What if I ask "Is there a proof that \pi is irrational?"

Thanks for raising this question. In this paper, we primarily work on quantitative reasoning problems from standard benchmarks that typically have well-defined numerical answers rather than ask if there is a proof for X.

If there is a yes/no question or a question similar to "Is there a proof that \pi is irrational?", we will translate it to either "Show that there is a proof that \pi is irrational" or "Show that there is no proof that \pi is irrational" depending on the answer from LLMs. Although proving these meta-logic statements automatically without human guidance could be difficult, the statements can still be translated and grounded to a theorem proving environment such as Isabelle. For example, the Isabelle library has a formal statement (and a proof) of Gödel's Incompleteness Theorems at https://www.isa-afp.org/entries/Incompleteness.html.

[1] Fu, Yao, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. "Complexity-based prompting for multi-step reasoning." arXiv preprint arXiv:2210.00720 (2022).

[2] Zhang, Zhuosheng, Aston Zhang, Mu Li, and Alex Smola. "Automatic chain of thought prompting in large language models." arXiv preprint arXiv:2210.03493 (2022).

[3] Creswell, Antonia, Murray Shanahan, and Irina Higgins. "Selection-inference: Exploiting large language models for interpretable logical reasoning." arXiv preprint arXiv:2205.09712 (2022).

[4] Khot, Tushar, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. "Decomposed prompting: A modular approach for solving complex tasks." arXiv preprint arXiv:2210.02406 (2022).

Thank you for your encouraging review and comments! We respond to your individual questions below.

Figure 1, caption: how would results change if, instead of majority voting over all verified solutions, the 'smallest' solution was selected?

Thanks for the question. Selecting the "smallest" solution could negatively impact the performance. As discussed in the Limitations section, the autoformalization process is not perfect and therefore selecting the majority answer over all verified solutions is more robust.

is it meaningful to run a head-to-head comparison of DTV and Jiang et al.?

DTV and Jiang et al. are not directly comparable since the former only assumes access to natural language problem statements rather than the ground truth formal statements. Given ground truth formal statements, one can evaluate the performance simply using pass@k instead of majority voting (maj@k). Therefore, DTV assumes a much more difficult but realistic setting.

very minor curiosity (not necessary for the paper): what's the most impressive result that DTV was able to derive?

In Figure 2, 4 (3, 5), we showcase some of the statements (proofs) formalized correctly by DTV and are not solved correctly by majority voting. Many of the problems require a good understanding of the natural language text to arrive at a correct formalization.

is it possible to estimate how much of a performance improvement there might be if GPT3.5 ran the solution formalization and self-critique filter? How much extra time this would cost?

Thanks for the great suggestion. We have additionally conducted the experiment on Number Theory where we equip baseline methods and DTV fully with GPT-3.5. The results show consistent improvement upon baselines for both Minerva 62B and GPT-3.5.

again, out of curiosity (rather than for the paper): is there a branch of the autoformalization project working on extending the formal libraries? I'm wondering whether Gowers' Polymath, or Tao's recent interest in Lean could help plug gaps in formal libraries.

relatedly, could DTV help with Hales' Formal Abstracts project, https://formalabstracts.github.io/ ? (This seems to have been dormant.)

Thank you for the great idea and interest in formalization. In this paper, we restrict our scope to quantitative reasoning problems. We believe our work can be extended to formalizing more advanced topics as LLMs and automated theorem provers continue to improve. Specifically, natural language theorem statements can be translated into their formal counterparts and then proved. The filters we propose in the paper could help filter out many unfaithful translations.

Figure 3: to clarify the caption - the generated formal statement is too high level for Isabelle to solve in a single step; however, the formalized individual steps are granular enough to allow proof and verification?

Yes, this is fully correct.

Minor typos:

Thank you for the note and we have updated our paper pdf with fixed typos in blue.

Thank you for your thoughtful review and suggestions. We address individual points below.

While DTV consistently outperforms baselines at different model sizes as seen in Table 2, the benefits from using DTV seem to be decreasing as the model size scale up (i.e, Minerva 8B -> 540B).

Thank you for the comment and analysis. Table 2 shows that we use the same autoformalization model, either Minerva 64B or GPT-3.5, across each row to ensure autoformalization ability and cost are kept constant. Consequently, we see more improvement compared to the majority voting baseline in the second column, where Minerva 8B, a weaker reasoning model, is used for creating informal solutions, as opposed to a stronger Minerva 540B model in the fourth column.

We have additionally conducted the experiment on Number Theory where we equip baseline methods and DTV fully with the stronger GPT-3.5. The improvement from using DTV maintains very significant on GPT-3.5 compared to Minerva 62B.

It would be good if there is a paragraph describing how a solution is extracted from an informal answer provided by an LLM. If possible, a discussion on “extraction based on the final answer” versus “extraction based on the informal reasoning” would also be nice.

Thank you for the great point! We include the following answer format in the few-shot prompt examples: "The final answer is [placeholder].” and use regular expressions to extract the informal answer. We agree with the reviewer that in certain scenarios, extraction might be more challenging and not only restricted to the final answer. In this case, we could leverage various semantic parsing methods [1] and possibly use a language model to extract the informal reasoning as seen in [2] as well. We have included the above discussion in our updated paper pdf in blue.

It is good that this is not merely a large scale version of DSP — new mechanisms such as filters for faithful translations are good to have.

Thank you for your comment and supporting our work. We would like to add that our work which aims to ground LLM reasoning with formal theorem proving environments is distinct from DSP that improves theorem proving performance with LLM. DTV assumes a much more difficult but realistic setting where only natural language data is given. To improve the reliability of autoformalization of statements, we introduce new mechanisms such as filters for faithful translations.

[1] Kamath, Aishwarya, and Rajarshi Das. "A survey on semantic parsing." arXiv preprint arXiv:1812.00978 (2018).

[2] Kojima, Takeshi, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. "Large language models are zero-shot reasoners." Advances in neural information processing systems 35 (2022): 22199-22213.

Thanks for the response. Regarding the first point, I understand that the autoformalization models for these were kept the same. What I was trying to say was that, as the model (that generates informal solutions) gets bigger, the benefits from using DTV become smaller. For example, for number theory, majority voting gains 13% by going from Minerva 62B to 540B, while DTV only gains 8%. This observation is consistent on all the three domains in Table 2 (and it is even more noticeable when one looks at the numbers of going from Minerva 8B to 540B).

That is what I was trying to say. It is possible that with even larger models (that generate informal solutions), majority voting might be just as good as DTV.

Thank you for your valuable and detailed review on our paper. We address individual points below.

The results in Table 1. compare DTV with GPT-3.5 with baseline methods using Minerva 62B. It is an unfair comparison since the performance improvement comes from the power of GPT-3.5, and we should compare the results of baseline methods using GPT-3.5. Without GPT-3.5, the improvement by DTV seems marginal.

Thank you for the great suggestion. We have additionally conducted the experiment on Number Theory where we equip baseline methods and DTV fully with the stronger GPT-3.5. The improvement from using DTV maintains very significant on GPT-3.5 compared to Minerva 62B.

The paper claims that DTV improves the performance of LLMs and sets simple baseline methods using just LLMs. To prove the claim true, the paper should show experimental results when we combine DTV with multiple LLMs, as is reported in (Wang et al., 2022).

Could you please show how the performance changes if we use different LLMs?

Thank you for the question. In Table 2 of the paper, we show that DTV can be combined with multiple LLMs of different sizes and reasoning capability. Specifically, we experiment with all three sizes of the Minerva model: 8B, 62B and 540B. The results show that DTV consistently outperforms majority voting baselines. Additionally, as seen in the table above with GPT-3.5, DTV can also improve upon vanilla GPT-3.5 reasoning, suggesting DTV is applicable to diverse LLMs.

Concerns about the number of samples and the efficiency of the DTV: Compared with majority voting, the proposed method needs at least three times more queries to an LLM to obtain a sample solution (informal solution generation, formal statement generation, and formal sketch generation, and I think the self-critique filter needs more queries per sample)...

Could you please show how the performance of DTV and Wang 2022 changes with number of samples n?

Thank you for the thoughtful question. We first discuss the sampling efficiency comparison between majority voting and DTV.

It has been observed in AlphaCode and Minerva papers [1,2] that majority voting performance scales in a log-linear fashion as a function of number of samples (please see the Figure 6 for both papers for the visualization). That is, the performance improvement from 100 to 1000 samples is roughly the same as from 10 to 100 samples. Therefore, majority voting performance can saturate quickly with diminishing return.

On the contrary, DTV can greatly boost majority voting performance with less compute. In this Figure, we plot the performance comparison between DTV and majority voting as a function of the number of samples. It can be seen that majority voting saturates as the number of samples increases and DTV significantly outperforms majority voting.

Furthermore, the additional inference cost of DTV can be reduced. As shown in Table 3 of the paper, without formal solution sketch and self-critique filter, the performance of DTV is not greatly impacted. Besides, compared to generating full-blown informal solutions, statement formalization is relatively inexpensive since the formal statements are much shorter than informal solutions to generate.

Lastly, we would like to mention in certain domains and applications such as tutoring and education, spending additional compute to verify solutions for better performance could be desirable. Verifying solutions in the formal theorem proving environments opens up the possibility of mitigating inherent limitations of LLM on certain problems.