Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
Authors: Jin Peng Zhou
Charles E Staats
Wenda Li
Christian Szegedy
Kilian Q Weinberger
Yuhuai Wu
Venue: ICLR 2024 poster (2024)
Keywords: mathematical reasoning
autoformalization
automated theorem proving
quantitative reasoning
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We show that automatically formalizing and verifying LLM generated quantitative reasoning solutions consistently outperforms vanilla majority voting.

Abstract: Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However, they still make unjustified logical and computational errors in their reasoning steps and answers. In this paper, we leverage the fact that if the training corpus of LLMs contained sufficiently many examples of formal mathematics (e.g. in Isabelle, a formal theorem proving environment), they can be prompted to translate i.e. autoformalize informal mathematical statements into formal Isabelle code --- which can be verified automatically for internal consistency. This provides a mechanism to automatically reject solutions whose formalized versions are inconsistent within themselves or with the formalized problem statement. We evaluate our method on GSM8K, MATH and MultiArith datasets and demonstrate that our approach provides a consistently better heuristic than vanilla majority voting --- the previously best method to identify correct answers, by more than 12\% on GSM8K. In our experiments it improves results consistently across all datasets and LLM model sizes. The code can be found at https://github.com/jinpz/dtv.

Published as a conference paper at ICLR 2024
DON'T TRUST: VERIFY - GROUNDING LLM QUANTI- TATIVE REASONING WITH AUTOFORMALIZATION
Jin Peng Zhou" Cornell University
Charles Staats
Wenda Li University of Edinburgh
Christian Szegedy xAI
Killan Q. Weinberger Cornell University
Yuhuai Wu xAI
ABSTRACT
Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However, they still make unjustified logical and computational errors in their reasoning steps and answers. In this paper, we leverage the fact that the training corpus of LLMs contained sufficiently many examples formal mathematics (e.g. in Isabelle, formal theorem proving environment), they can be prompted to translate ie. autoformalize informal mathematical statements into formal Isabelle code which be verified automatically for internal consistency. This provides a mechanism to automatically reject solutions whose formalized versions inconsistent within themselves or with the formalized problem statement. We evaluate our method on GSM8K, MATH and MultiArith datasets and demonstrate that our approach provides consistently better heuristic than vanilla majority voting - the previously best method to identify correct answers, by more than 12% on GSM8K. In our experiments improves results consistently across all datasets and LLM model sizes. The code can be found at https:/ //gp:::///ii http://ggtuuuuu.. thub. com jinz//dtn cttpt////doc///i//dt////
INTRODUCTION
Recently, language models (Devlin et al. 2018 Brown et al. 2020 Chowdhery et al. 2022) have advanced significantly in many natural language processing tasks such as machine translation, question answering, summarization, etc. More recent large language models (LLMs) such as Min- erva (Lewkowezz et al. 2022), GPT3.5 (OpenAl) and GPT4 (OpenAl, 2023) have also become increasingly capable of solving quantitative reasoning problems, ranging from middle school math word problems (Cobbe et al. 202T) to challenging high school mathematical competition prob- lems (Hendrycks et al. 2021). By training or finetuning the model on high-quality natural language mathematical and scientific text, these LLMs can generate self-contained step-by-step solutions to quantitative reasoning problems without relying external tools. However, just like human beings, the solutions L.MSs generate are prone to simple calculation errors and unjustified logical leaps.
Following Wang et al. (2022) Lewkowycz et al. 2022). one can sample many proposed solutions, extract the final answer from each, and select the most common answer. While aggregating answers like this improves performance the problem level, the most common answer sometimes wrong. Ideally, we would like better heuristic to identify the correct answer. In fact, there are well known techniques for computers verify mathematical reasoning using formalization (Wiedijk] 2008). Those methods involve translating the problem and sometimes the solution into formal language. Unfortunately this translation difficult and time-intensive enough that formalization methods are less frequently leveraged.
Recently it was discovered that large language models, with few-shot prompting, can automatically formalize natural mathematical language into formal languages (Agrawal et al. 2022 Azerbayev
Work done while interning at Google Research. Correspondence to: ipzhouBcs cs. corne 11. edu.
corne
Work done while Google Research.

---

Published as a conference paper at ICLR 2024
Informal Solution hrare
Informal
Informal Reasoning
Formal Reasaning
hance
Informal Statement Find all bosntve roots of 0.
Formal Statement
GO
Formal Statement #1
Formal Statement #2
*Ixt 3
Eheorees [XLETTAl) 1"
(arraaua))
LLM
Formal Solution #1 "x"2 and peas (ate)
Formal Solution #2
and no
Informal Solution
Formal Solution
Wi brow thair Bon Massoo
antera "i"2
iher have comm
La pocu
jyith EA8P1
Automated Theorem Prover
vIK AA
Answer
Verified
Not Verified
Figure I: A pictorial illustration of Don't Trust: Verify. Left:: starting from an informal statement, an informal solution is generated by large language model. The informal statement and solution are then translated into their formal counterparts. Multiple informal solutions for each problem are generated with temperature sampling. Right: An automated theorem prover in the formal environment is used to verify formal solutions against formal statements step by step (indicated by [ATP]). The final answer is chosen using majority voting over only the verified solutions. In this example, Formal Solution #1 successfully proves Formal Statement #1. Formal Solution #2, however, fails to prove the "only if" direction of Formal Statement #2.
ct al. 2023 Wu et al. 2022 Jiang et al. 2023: Wang et al. 2020). It is conjectured this capability arises because the training data for these LLMs contains sufficiently many examples of computer code and/or formal mathematics. While the translation is far from perfect and can fail on many complex statements, the correctness of the statements produced can be checked using formal theorem proving systems such as Isabelle (Nipkow et al. 2002) and Lean (de Moura et al. 2015).
In this paper, demonstrate that in spite of its issues, autoformalization is already capable enough to identify correct answers for many quantitative reasoning problems. We call our method Don't t Trust: Intuitively, instead of naively taking majority voting of all generated natural language solutions, we only aggregate solutions that can be verified with autoformalization. To carry out verification, both formal statement and solution are needed. Therefore, we attempt to translate the plain text problem and solution into formal language using large language models. However, because language models can erroneously translate incorrect statements into correct ones, we develop both symbolic and neural filters to improve the statement translation reliability. Additionally, even with a correct formal statement, a formal solution directly translated from informal solution can fail to prove it. In particular, correct informal solutions (whether generated by humans or LLMs) skip low-level steps that are necessary for formal reasoning. To this end, we instead generate a formal solution sketch following Wiedijk (2004), Jiang et al. (2023 and employ an automated theorem prover (ATP) to fill in the low-level gaps.
Verify (DTV) and provide an overview in Figure [
We evaluate DTV GSM8K (Cobbe al. 2021). three subsets of MATH (Hendrycks al. 2021 following prior work (Zheng et al. 2021). ). and MultiArith (Roy & Roth 2016) datasets. The results show that method consistently outperforms vanilla majority voting (Wang al. 2022 Lewkowycz et al., 2022), with more than 12% improvement on GSM8K. We demonstrate that DTV improves performance across various model sizes and categories. Additionally, we provide case studies on our method identifying correct answers as well as informal solutions. Finally, we discuss the limitations of our approach inherited from LLM and theorem proving environments.
BACKGROUND AND RELATED WORK
Informal guantitative reasoning with language models. A number of large language models
such as PaLM (Chowdhery et al. 2022). Minerva (Lewkowycz al. 2022). GPT3.5 (OpenAl) and GPT4 (OpenAl| 2023) have demonstrated their impressive quantitative reasoning abilities by pretraining or finetuning mathematical and science data. To improve informal reasoning
2

---

Published as a conference paper at ICLR 2024
performance, of-tin- prompting (Wei et al. 2022) is typically used to encourage language models outputting intermediate reasoning steps before arriving at an answer. A diverse set of prompting methods have since been proposed for informal reasoning that tries to find better examples for prompting (Fu et al. 2023 Zhang et al., 2022) or better strategies for decoding from the model such conditioning on references, sulpi-step decoding (Creswell et al. 2022; ZZeng al., [023] Welleck et al. 2022 Khot et al. (023)). Cobbe et al. (2021) explores training informal verifiers to judge the correctness of reasoning. Additionally, to alleviate erroneous reasoning with language models, techniques that explore multi-sample consistency in the informal reasoning (Wang et al. 2022; Jung et al.] 2022) have also been proposed. Our approach does not require training and is complementary to these methods since we rely on the consistency of formal theorem proving system to identify correct reasoning paths and improve the reliability of large language model reasoning.
Augmented language models. Besides elucidating rationales via thain-of-thougle prompting, recent research has also been devoted to augmenting L.MSs with external tools such as web search
engine (Nakano et al. [202] Lazaridou et al. 2022 Schick et al. (002)). external memory retrieval (Shi
ct al. 2023 Izacard et al. 2022) and programming -baed calculators (Chen et al. 2022 Gao et al.
2022. Imani et al. 2023) bolster their downstream performance and reduce hallucination. Our
work augments language models with a formal theorem proving environment that goes beyond simple arithmetic (Chen et al.
2022 Imani al. 2023) and Boolean logic (Jung et al. 2022)
Interactive theorem proving and autoformalization. Modern interactive theorem provers such as Isabelle (Nipkow et al. 2002). Coq (Barras et al.) 1997). and Lean (de Moura al. 2015), provide
an interactive environment to encode and mechanically verify mathematical proofs. Success stories
with handcrafted proof's include the verification of industrial software systems (Klein et al. 2009)
and research-level mathematics (Castelvecchl et al. (02T). Szegedy (2020) argues for automatically obtaining formal mathematies from their informal counterparts by translation i.e. autoformalization. Since then, researchers have shown the feasibility of autoformalization using neural networks in
particular large language models (Agrawal et al. 2022: Azerhayev et al. 2023 Wu et al. 2022 Jiang et al. 2023, Wang et al.) 2020). Our work which aims to ground L.MM reasoning with formal theorem proving environments is distinct from Jiang et al. (2023) that improves theorem proving performance with LLM. DTV assumes much more difficult but realistic setting where only natural language data is available. We are the first to demonstrate it is possible to automatically verify correct answer and informal solutions with autoformalization.
DON'T TRUST: VERIFY
We describe approach Don't Trust: Verify (DTV). Given mathematical question and several solutions to it phrased in natural language, we assume the question has a well-defined answer and each solution contains an answer that may or may not be correct. Our goal is to understand which informal solutions are more likely to be correct. An overview of our method can be found in Figure []
3.1 STATEMENT FORMALIZATION
We begin by finding a formal statement that corresponds to the description of the informal problem statement. In many mainstream formal theorem proving environments such Isabelle (Nipkow et al., 2002), Lean (de Moura et al., 2015), and Coq (Barras et al. 1997). a formal statement needs to be an assertion rather than question. For example, a formal statement cannot be in the form of Is irrational? but rather Show that π is irrational. Since quantitative reasoning problems typically ask for an answer rather than proof, we first extract the answer from each proposed informal solution. The formal statement is then generated conditioned on both the plain text statement and the extracted answer. Following /Wu et al. 2022), we leverage the few-shot learning capability of large language models to generate formal representation of the informal statements. Specifically, we provide a few informal-formi statement translation pairs and prompt the language model to complete the subsequent problem statement formalization.
3.2 SOLUTION FORMALIZATION AND VERIFICATION
The formalized statement itself does not tell us its correctness without a formal solution or proof. Because of this, we seek to generate piece of formal solution verify the statement correctness.
3

---

Published as a conference paper at ICLR 2024
Ideally, formal solution steps could be directly translated from natural language solution steps by sharing a similar level of abstraction. However, this could fail to prove the statement since formal reasoning steps require additional low-level justification than their natural language counterparts either written by human or L.Ms.. To address this issue, we generate a formal solution sketch following Wiedijk 20004);[iagg high-level steps that are based on natural language counterparts and leaves low-level justifications to an automated theorem prover (indicated as [ATP] in Figure D Similar to statement formalization, we few-shot prompt large language model to automatically generate such formal solution sketches.
al. (2023) (see (leut) The formal solution sketch contains
To perform verification, we attempt to prove the formal statement with individual solution steps in a formal theorem proving environment. We leverage the consistency of the formal environment and its automated theorem prover to sequentially verify the steps. At any step, if the automated theorem prover fails to close the gap, we consider the formal statement not verified and hence incorrect. Besides, if there are still remaining goals to be proved after verifying every step, the formal statement (right) Formal Solution #2, although both steps
is also treated as unverified. For example, in Figure I are correct, the formal statement cannot be proved since the original statement is an if and only statement, and the right-to-left direction is clearly false. If formal statement is considered verified, the corresponding informal solution and answer are also considered verified. To arrive at the final answer to the problem, we take the most common answer among the verified informal solutions. If no solution can be verified, we fallback to majority voting across all unverified solutions.
3.3 FILTERING UNFAITIFUL STATEMENT FORMALIZATIONS
For DTV to achieve good performance, it is crucial that informal and formal statements match precisely with each other. This is because an answer that is definitely incorrect to one problem could still be correct an altered problem. For example, in the problem statement of Figure [1] if the constraint of æ being positive is omitted, the answer x = +2 would be correct instead. This is detrimental as the erroneously translated formal statements with incorrect answers can get verified by DTV. We call such statements unfaithful. To mitigate this issue, we propose to employ two types of filters to discard formal statements that are potentially unfaithful.
Vacuous statement filter. In our preliminary experiments, we found that vacuous formal statements form one common category of verified but unfaithful statement translations. By vacuous we mean that the formalized statement's 's hypotheses are contradictory, and can thus be used to prove anything by contradiction. The contradictory hypotheses are usually due to language model translation mistakes rather than the original problem itself being contradictory. For instance, translated statement could constrain a variable z to simultancously satisfy æ > and æ < O, leading to a contradiction. To address this issue, we replace the formal statement goal with simple statement of Falss Fasse and apply the automated theorem prover. Any formal statement that can be proved after this substitution is vacuous. We assume it is very unlikely that the natural language question is legitimately vacuous and we discard such vacuous formalizations.
Self-critique filter. There other categories of unfaithful translations we find harder to identify symbolically with automated theorem provers. Formalization attempts generated by L.MSs can sometimes be irrelevant to the problem or will even modify a formula make the statement correct. Inspired by the fact that large language models are capable of critiquing their own outputs (Saunders) et al. 2022). we explicitly ask the language model decide whether the formal statement is faithful translation of the informal statement. The likelihood of yes versus no followed by a justification is compared. If the likelihood of no outweighs yes, the formal statement is considered unfaithful and discarded. It is worth noting that the self-critique filter can reject faithful formal statements well as miss unfaithful formal statements. We empirically verify its effectiveness in the experiment section.
4 EXPERIMENTS
4.1 DATASET AND FORMAL ENVIRONMENT
We evaluate DTV on three quantitative reasoning datasets: GSM8K (Cobbe et al., 2021). MATH (Hendrycks et al. 2021) and MultiArith (Roy & Roth 2016). These datasets have been used extensively to evaluate the reasoning capability of large language models (Cobbe et al. 2021 Weil
et al. 2022 Lewkowycz.ee al. 2022 Zhang et al.
2022 0 OpenAl 2023). GSM8K and MultiArith
4

---

Published as a conference paper at ICLR 2024
Informal Statement from Prealgebra: At Annville Junior High School, 30% of the students in the Math Club are in the Science Club, and 80% the students in Science Club are the Math Club. There are students the Science Club. How many students are in the Math Club? Show that it is 40.
Generated Formal Statement:
theorem
fixes math math_clus club science club nath and science :: nat assumes "math and science = 0.3 math club"
and "nathhand_science = 0.8 science_club"
and "science_cci ceclenneecllbbbb 15"
shows "math_club 40"
Informal Statement from Number Theory: What the hundreds digit in the following product: 5 x 6 7 x x 10 Show that it is 2.
Generated Formal Statement:
theorem
"((5: :att 6
10) div 100 mod 10
2
Informal Statement from GSM8K: A herd consists of camels and dromedaries. There are 180 heads and 304 bumps. How many dromedaries are there if camels have two humps each and dromedaries have hump each? Show that is 56.
Generated Formal Statement:
theorem
fixes camels dromedaries :: nat assumes "camels dromedaries 180"
camels dromedaries 304"
shows "dronedaries 56"
Informal Statement from Algebra: parabola ax? du + contains the points (-1,0), (0, and (5, 0). Find the value 100a 106 + c. Show -55.
Generated Formal Statement:
theorem
fixes :: real
assumes h0 : "a (-1)
(-1) +c=
and hl "a 0-2 + b * 0 + c 5"
and h2 "a 5'2 + b + 5 c 0"
shows "100 a 10 b
-55"
Figure 2: Examples faithful formal statements translated from informal statements with correct answers by DTV. Majority voting failed to solve all four problems but DTV solves them successfully. The model capable translating complex informal statements precisely. Note that the sentence "Show that it is [answer]" is appended to the original informal problem statement by first extracting the answer from an informal solution. We provide more examples in Appendix A.1
datasets contain grade-school arithmetic word problems. MATH dataset consists of high school math- ematical competition problems drawn from AMC 10, AMC 12, AIME, etc that are more challenging. The problems in MATH have also been grouped into 7 categories: Prealgebra, Algebra, Number Theory, Counting and Probability, Geometry, Intermediate Algebra, and Precalculus. Following prior work (Zheng al. (021) which only draws problems from algebra and number theory categories, evaluate on Prealgebra, Algebra and Number Theory subsets of the MATH dataset, which are most applicable in current theorem proving environments.
Similar to Wu et al. (2022) Jiang et al. (2023), we use Isabelle (Nipkow et al. 2002) as the formal theorem proving environment for the experiments since it has one of the largest formal corpora that enables formalization of challenging problems as well as powerful automated theorem provers to close low-level details in the formal solution sketches. We do not fundamental limitations of our
5

---

Published as a conference paper at ICLR 2024
DTV framework applying to other formal languages such Lean and Mizar and we leave this to future work. We adopt the Portal-to-ISAboe (Jiang et al. 2021) interface to interact with Isabelle.
4.2 BASELINES AND EVALUATION PROTOCOL
single sample and multiple samples with majority voring (Wang et al. 2022 Lewkowycz al. 2022). In single sample, for each problem, only informal solution is sampled greedily with 7 0. For the latter, multiple informal solutions are generated with temperature sampling. To evaluate the performance, the most common answer matches the ground truth answer. For single sample, the most common answer is the answer extracted from the solution whereas for multiple samples with majority voting, grouping of solutions based on the answer is performed and the most frequent answer is chosen.
We compare DTV with two baselines:
consider problem being solved correctly if
4.3 EXPERIMENTAL SETUP
Informal solution generation. We few-shot prompt large language models to generate n = 64 informal solutions per problem conditioned on the informal problem statement. We experiment with the 8B, 62B and 540B Minerva models (Lewkowycz et al., (022). We use the default sampling configuration (T = 0.6, nucleus sampling (Holtzman et al. (219)) = 0.95) reported in Lewkowyez al. (2022) for Minerva models.
Statement formalization. We prepare 25 paired (informal statement, Isabelle formal statement) examples for each of the three categories from MATH dataset, GSM8K and MultiAirth datasets as the candidates for few-shot demonstrations. When prompting the model to formalize an informal statement, randomly draw and permute 10 examples to form the few-shot prompt. We always ensure the problem to be translated does not appear in the few-shot prompt. To reduce randomness of statement formalization process, for each informal solution, we perform 10 statement formalization attempts. All few-shot demonstration examples can be found in the suppicmentary materials.
Solution formalization and verification. We further select 10 problems from each dataset and manually write complete formalization examples including both statements and solutions in the form of (informal statement, formal statement, informal solution, formal solution sketch) as examples for solution formalization. We randomly select 3 examples for each few-shot prompt. We query the language model once for solution formalization for each formal statement sample so that each informal solution is in total formalized 10 x 1 times. We then use Isabelle to verify the formal solution sketch against the generated formal statement. Sledgehammer (Paulsson & Blanchette 2012) along with 11 common tactics (auto, simp, blast, fastforce force, eval, presburger, sos, arith, Linarith, and aut a simp: field.s simps are used to close low-level open conjectures in the formal solution sketch. We consider the formal solution and consequently the corresponding original informal solution correct if Sledgehammer and tactics succeed. An informal solution is kept if any of the 10 formalization attempts is verified successfully.
Unfaithful statement filters. For the vacuous statement filter, we change the goal to be proved in generated formal statement to false. This is accomplished by replacing text after show clause to show false and checking whether Sledgehammer and tactics can prove the modified formal statement. Statements proved this way are discarded due being vacuous. To create the self-critique filter, we take 5 faithful and 5 unfaithful statement formalization examples generated by the model in the preliminary experiments as few-shot demonstrations. The unfaithful formalization examples are also accompanied by what errors it have. This few shot demonstration is kept fixed throughout the experiments. Generated formal statements are discarded if the likelihood of an answer of yes lower than no for the language model.
4.4 EXPERIMENTAL RESULTS
Table I shows the percentage of problems solved for baselines and DTV. The informal solutions generated with Minerva 62B model (Lewkowyez et al.) 2022). We consider two autoformalization model choices: Minerva 62B and GPT3.5 (OpenAl). Due to the API inference time and cost, only use GPT3.5 to generate the formal statements, which is the most crucial component in our approach. Minerva 62B is queried for both solution formalization and self-critique filter.

---

Published as a conference paper at ICLR 2024
It can be seen that majority voting is a strong baseline that significantly improves the language model performance over single sample generation from an average of 42.8% to 61.5%. matching the observations in Wann et al. (2022); Lewkowyez al. (2022). With autoformalization and verification in the formal environment, DTV outperforms majority voting baseline and achieves an average performance of 65.0% using the same Minerva 62B without any finetuning, suggesting the effectiveness of autoformalization. Since Minerva was mainly trained on natural language math content, its autoformalization capability could be limited. To this end, with the same informal solutions generated by Minerva, we switch the statement formalization model to GPT3.5. This leads to an even larger improvement of average solve rate 68.2%. We observe that the boost in performance is consistent across all datasets and categories of problems. A larger improvement could potentially obtained by switching solution formalization and self-critique filter to GPT3.5.
Table Comparison of problem solve rate on GSM8K, MATH Number Theory, Algebra, Prealgebra and MultiArith evaluation sets. DTV consistently outperforms the two baselines that do not perform autoformalization. *To reduce the time and cost of repeatedly calling OpenAl APIs, GPT3.5 is only used to generate formal statements.
Problem Solve Rate
GSMSKK
Number Therry
Algehra
Prealgehon
MultiArith
Average
Boselines
Single Sample with Minerva 62B
48. 6%
12.2%
33.3%
34.1%
85.7%
42.8%
Majority Voting with Minerna 62B
67.2%
23.7%
60.856
50.2%
96.6%
61.5%
Trust: Verify (DTV)
DTV Formllization with Minerva 62B
71.4%
31.9%
61.8%
61.0%
98, 98.8%
65.0%
DTV Formalization with GPT3.5
79.4%
36. 36.1%
63.2%
63.4%
99.0%
68. 38.2%
4.5 ABLATION
2 shows how baselines and DTV performs when varying the size of model that generates informal solutions. Specifically, we experiment with all three sizes of the Minerva model: 8B, 62B and 540B on Number theory, GSM8K and MultiArith problems. Not surprisingly, as the informal solution model scales up. both single sample and majority voting baselines improve their performance, suggesting larger models have generally stronger quantitative reasoning capability than smaller models. For DTV, we keep the formalization model the same as in Table 1 and do not vary its size. DTT consistently outperforms the baselines by large margin across all three informal reasoning model sizes on all three datasets, indicating the scalability of DT'. The improvement is particularly significant on Minerva 8B, almost doubling its problem solve rate for GSM8K and number theory. Interestingly, the results also demonstrate that it is beneficial to autoformalize informal solutions from larger model (Minerva 540B) even with weaker model such as Minerva 62B, which opens up the possibility of reducing autoformalization runtime and cost.
Size of informal solution models. Table
Table 2: Problem solve rate on MATH Number Theory, GSMSK, MultiArith datasets. Each column represents the model that generates informal solutions, ranging from Minerva 8B to Minerva 540B. Baselines and DTV are shown on each row. DTV consistently outperforms baselines at different model sizes. *To reduce the time and cost of repeatedly calling OpenAl APIs, GPT3.5 is only used to generate formal statements.
Problem Solve Rate on Number Theory
Minerva 8B
Minerva 62B
Minerva 5-0BB
Raselines
Single Sample
7.1% 13.5%
12.2% 23.7%
19.1%
Majority Voting
36.1%
Don't Y Trust: Verify (DTV)
DTV Formalization with Minerva 62B
23.0% 1.%
31.9% 36.1%
10.2%
DTV Formalization with GP
4%
Problem Solve Raie GSMBK
Minarva SB Mineva 62B
Minerva 540B
Probler Solve Rate on MulliAria
Minerva SB
Minersa 62B
Minerva 540B
Randine
Roviinee
Single Sample Majocry Noding
6% 07.2%
58.1%
Sing'e Sample
1% 85,00
R5.155
9%
27.7%
76.67
Majocty Voling
99.37
Don't Trast Vellly (DTV)
Trast Nevly
DTV Fomalizaton with Minerva 62B
48 4%
71. 4%
78.8%
DTV Pomaliztoon with Minerva 628
93.0%
98. 85%
99.8%
7

---

Published as a conference paper at ICLR 2024
Effect of solution formalization and filters. For quantitative reasoning problems, it is possible to directly prove a translated formal statement with the automated theorem prover in absence of a step-by-step solution sketch. This is because once the statement has been formalized correctly, the proposition to be proved is not "far" from the assumption. Proving the proposition could just involve simplification and evaluation that the automated theorem prover can be capable of. We observe that by not asking DTV to formalize informal solutions, we can still achieve strong problem solve rate (see Table 3 However, in this case only the informal solution answer is checked by DTV and correct formal statements that require elaborate formal solution steps will not be proved successfully. As shown in Table[] both filters that are used to detect unfaithful formalization are beneficial for improving the problem solve rate.
Table 3: Problem solve rate on MATH Number theory, Algebra and Prealgebra categories with three types of ablation. The results suggest that solution formalization and two statement filters are beneficial for improving performance.
Problem Solve Rate
Number Theory
Algebra
Prealgebra
DTV Fornalization with Minerva 62B
31.9%
61.8%
61.0%
- Formal Solution Sketch
29.2%
60.7%
60.3%
Vacuous Statement Filter
30.7%
61.4%
60.4%
Self-Critige Critique Filter
30.0%
60.9%
58.4%
4.6 QUALITATIVE ANALYSIS
DTV translates problems that majority voting fails. In Figure 2 we show four case study examples that majority voting fails to solve due to the correct answer not being the most common answer. DTV, however, successfully formalizes the informal statement and uses automated theorem prover to prove these propositions, making the correct answer as the majority answer. Each example statement formalized require clear and precise understanding of the informal statement and the language model is capable of formalizing diverse types of problems. For example, in the first example, the model needs to understand translates them into the formal environment. In Appendix A. we provide more case study examples of statement formalization.
-exluuionnexllssin relationship between different types of students and precisely
DTV solves additional problems leveraging correct informal solution steps. In Figure 3 showcase a number theory problem whose statement and informal solution are both formalized correctly by the model. The formal statement itself is beyond the capability of automated theorem prover and requires formal solution steps to solve it. It can be seen that by translating individual informal solution steps correctly, the problem successfully solved. Additionally, we observe that for this problem, there are low-quality informal solutions that simply output final answer without justification and their corresponding formal solutions cannot prove the proposition. This suggests that autoformalization could potentially be used to identify high-quality informal solutions. We provide more examples in Appendix A.2
4.7 LIMITATIONS AND FUTURE WORK
One limitation of our approach is that it requires the theorem proving environment support the problem domain in question. Currently, most environments are still limited in scope, a shortcoming that DTV naturally inherits. For example, Isabelle has limited support for formalizing geometric and probabilistic reasoning. Statements involving such arguments usually need to be built upon measure theory and advanced calculus, which is far beyond the math required to solve these high school problems. This is also the reason why these subsets in the MATH dataset have been excluded by prior work (Zheng et al. 202T) and us. As more support such areas becomes available, we expect DTV to exhibit similar gains but a thorough evaluation is currently left as future work. Until then, for practical purposes, one could imagine training a simple classifier that predicts if a particular problem belongs the domain that is well suited for DTV.
The second inherent limitation of DTV is the LLM's capability to translate a theorem, written in natural language, into formal statement. Mistakes can be subtle. For example, 2 + 3 could be erroncously formalized to (1::nat) Isabelle because variable of the type nat cannot be negative (i.e. (1::nat) 2 0). Future
2 + 3, which evaluates to instead of 2 in
8

---

Published as a conference paper at ICLR 2024
Informal Statement from Number Theory: The least common multiple of two numbers is 3720, and Given that one of the numbers is 120, what is the other number?
their greatest common divisor Show that is 248.
Generated Informal Solution:
The product of the two numbers is the product of their LCM and their GCD:
3720 = 29760.
Since of the numbers is 120, divide this product by 120 to obtain the other number:
29760
248
120
Final Answer: The final answer is 248. hope it correct.
Generated Formal Statement and Formal Solution:
theorem
fixes y ::
assumes "1 x y 3720"
and "god x y = 8"
and "x 120"
shows 248"
proof
(* The product of the two numbers is the product of their LCM and their GCD; 3720Vodot8-29760. *)
have "Icn
god x y y by auto [ATP]
ther. have "3720
120 y" using assms
by fastforce [A7P]
(* Since one of the mumers is 120, we can divide this product by 120
to obtain the other number: \frac(29760) (120) (120)=booxed(24) *)
then have "y 29760/120*
by auto [ATP]
then show ?thesis
by auto [A7P]
ged
Figure 3: An example number theory problem which both the informal statement and solution are translated correctly by DTV. The generated formal statement cannot be directly solved by automated theorem prover. By translating informal solution step by step, the formal statement is proved and the answer verified. The steps that end with [ATP] are generated by the automated theorem prover.
directions could explore employing more effective filters and leveraging reinforcement learning from human feedback (RLHF) (Bai et al. 2022) to further finetune language models on aligned mathematical formalizations directly.
CONCLUSION
In this paper, we show that by leveraging the autoformalization capability of large language models through few-shot prompting, we can identify the correct answer among many informal solution samples generated by the same large language models. Our approach, Don't Trust: Verify, utilizes the internal consistency of formal theorem proving environments to check for correct answers. DTV is lightweight with no training or finetuning required. We demonstrate the feasibility and effectiveness of DTV by reaching tate-of-the-art performance GSMSK, subsets of MATH and Multi datasets. DTV consistently outperforms vanilla majority voting, the best previous approach, and leads to improvement across different model sizes from 8B, 64B and 540B. DTV is also complementary to different prompting methods such as Zheng et al. (2023); Fu et al. (2023) that only process reasoning in informal domain. We seek to combine these approaches with DTV for future work.

---

Published as a conference paper at ICLR 2024
6 ACKNOWLEDGEMENT
We would like to thank Albert Jiang for his help and support in Isabelld JPZ is supported by grant from the Natural Sciences and Engineering Research Council of Canada (NSERC) (567916). WL was supported by the ERC Advanced Grant ALEXANDRIA (Project GA 742178).
REFERENCES
Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models, arXiv preprint arXiv:2211007524, 2022.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-leved mathematics. arXiv preprint arXiv:2302. 12433, 2023.
Yuntao Bai, Andy Jones, Kamal Ndousse, Amanda Askell, Anna Chen, Nova DasSarma, Dawn Drain, Stanislav Fort, Deep Ganguli, Tom Henighan, et al. Training helpful and harmless assistant with reinforcement learning from human feedback. arXiv preprint arXiv:2204.0588 2022.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean -hristohee Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6. PhD thesis, Inria, 1997.
Tom Brown, Benjamin Mann, Nick Ryder, Melanic Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. Advances in neural information processing systems, 33:1877-1901, 2020.
Davide Castelvecchi et al. Mathematicians welcome computer-assisted proof in 'grand unifica- tion' thnothoryy Nature, 595(7865): 2021.
Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W. Cohen. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks, 2022.
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al. Palm: Scaling language modeling with pathways. arXiv preprint arXiv:2204.0233 2022.
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2 10. /4/68, 2021.
Antonia Creswell, Murray Shanahan, and Irina Higgins. Selection-inference: Exploiting large language models for interpretable logical reasoning, 2022.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doom, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CAADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp- 378-388. Springer, 2015.
Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.0400 2018.
Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. Complexity-base prompting for multi-step reasoning, 2023.
Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. Pal: Program-aided aided language models. arXiv preprint arXiv:2211.10335 2022.
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang. Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint 24 2021.
10

---

Published as a conference paper at ICLR 2024
Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. The curious case of neural text degeneration. arXiv preprint arXiv:1904.09751, 2019.
Shima Imani, Liang Du, and Harsh Shrivastava. Mathprompter: Mathematical reasoning using large language models. arXiv preprint arXiv:2303.053900 2023.
Gautier Izacard, Patrick Lewis, Maria Lomeli, Lucas Hosseini, Fabio Petroni, Timo Schick, Jane Dwivedi- Yu, Armand Joulin, Sebastian Riedel, and Edouard Grave. Atlas: Few-shot learning with retrieval augmented language models. arXiv preprint arXiv, 2208, 2022.
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378-392, 2021.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth' ee Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. In International Conference Learning Representations, 2023. BtRbttts:/// http:////............///////....
12283
Jaehun Jung, Lianhui Qin, Sean Welleck, Faeze Brahman, Chandra Bhagavatula, Ronan Le Bras, and Yejin Choi. Maieutic prompting: Logically consistent reasoning with recursive explanations. In Proceedings of the 2022 Conference on Empirical Methods Natural Language Processing, pp. 1266-1279) Abu Dhabi, United Arab Emirates, December 2022. Association for Computational wwt. Linguisties. URL http::::://.. pttttps://aclaanttiiioe http://c..annncollooooo///2/2222 emn emn p--mall 82.
Aishwarya Kamath and Rajarshi Das. A survey semantic parsing. arXiv preprint arXiv:1812.00977. 2018.
Tushar Khot, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. Decomposed prompting: A modular approach for solving complex tasks, 2023.
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification an os kernel. Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. pp. 207-220 2009.
Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. Advances in neural information processing systems, 35: 22199-22213 2022.
Angeliki Lazaridou, Elena Gribovskaya, Wojeiech Stokowiec, and Nikolai Grigorev. Internet- augmented language models through few-shot prompting for open-domain question answering. arXiv preprint arXiv:2203.05115, 2022.
Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative rea- soning problems with language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL https://openre///
net htt///orummmaa dd= 1FTE=IXXIT
Reiichiro Nakano, Jacob Hilton, Suchir Balaji, Jeff Wu, Long Ouyang, Christina Kim, Christopher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, al. Webgpt: Browser-assisted question-answering with human feedback. arXiv preprint 2rXiv:21 2021.
Tobias Nipkow, Markus Wenzel, and Lawrence Charles Paulson. Isabelle/hol: A proof assistant for higher-order logic. 2002.
OpenAl. Introducing chatgpt. URL /tt.ttppee//peeaaacc///////////a
OpenAl. Gpt-4 technical report, 2023.

---

Published as a conference paper at ICLR 2024
Lawrence C Paulsson and Jasmin C Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Proceedings of the 8th International Workshop the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC, volume 2, 2012.
Subhro Roy and Dan Roth. Solving general arithmetic word problems. arXiv preprint AXXv::6608.011333 2016.
William Saunders, Catherine Yeh, Jeff Wu, Steven Bills, Long Ouyang, Jonathan Ward, and Jan Leike. Self-critiquing models for assisting human evaluators. arXiv preprint arXiv:2206.05802. 2022.
Timo Schick, Jane Dwivedi- Yu, Roberto Dessi, Roberta Raileanu, Maria Lomeli, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. arXiv preprint arXiv:2302. 2023.
Weijia Shi, Sewon Min, Michihiro Yasunaga, Minjoon Seo, Rich James, Mike Lewis, Luke Zettle- moyer, and Wen-tau Yih. Replug: -etreeval-augmented black-box language models. arXiv preprint arXiv:2301.12652, 2023.
Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings 13, pp. 3-20. Springer, 2020.
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 85-98, 2020.
Xuezhi Wang. Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203. 2 1/71,, 2022.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed H. Chi, Quoc V Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL httpt::/t////....... wwt.ooppnrvvvveeeeeeee ew. www.eeettootteeeee forum? ew..wwwwww.....
id ViolMeSB J
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models, 2022.
Freek Wiedijk. Formal proof sketches. Lecture notes in computer science, 3085:378-393, 2004.
Freek Wiedijk. Formal proof-getting started. 2008
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32366 2022.
Zhuosheng Zhang, Aston Zhang, Mu Li, and Alex Smola. Automatic chain of thought prompting in large language models. arXiv preprint arXiv:22 10.03493, 2022.
Chuanyang Zheng, Zhengying Liu, Enze Xie, Zhenguo Li, and Yu Li. Progressive-hin prompting improves reasoning in large language models, 2023.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematies. arXiv preprint arXiv:2109.001 10, 2021.
12

---

Published as a conference paper at ICLR 2024
APPENDIX
A ADDITIONAL CASE STUDY EXAMPLES
A.1 FAITHFUL STATEMENT FORMALIZATION
Informal Statement: Gina has five pairs of white socks, three pairs of black socks, and two pairs of red socks. What percent of her socks are red? Show that it is 20%.
Generated Formal Stafement:
theorem
assumes "card whites 10" and "card blacks = 6"
and "card reds = 4"
shows "100
(card reds)
(card whites card blacks card reds) 20"
Informal Statement: What is the sum of the units digits of all the multiples of 3 between 0 and 50?
Show that is 78.
Generated Formal Statement:
theorem
"sum list
[x mod 10 x V<leftarrow [0..50], 3 dvd x] (78: :nat)
Informal Statement: Blake Jenny each took four 100-point tests. Blake averaged on the four tests. Jenny scored 10 points higher than Blake on the first test, 10 points lower than him on the second test, and 20 points higher on both the third and fourth tests. What is the difference between Jenny's s average and Blake's ' average these four tests? Show that is 10.
Generated Formal Statement:
theorem
fixes b1 b2 b3 b4
j1 j2 13 j4 :: real
assumes "bl b2
b3 + b4 4 78"
and "j1 bl 10""
and "j2 b2 10"
and "j3 b3 + 20"
and "j4 = b4 + 20"
shows (ji j2 13 /4)/4 (b1 b2 b3 b4) /4 10"
13

---

Published as a conference paper at ICLR 2024
Informal Statement: What is the perimeter, in units, of rhombus if its area is 120 square units and one diagonal is 10 units? Show that is 52.
Generated Formal Statement:
theorem
fixes dll d2 :: real
"dl 0"
and C"
and "d1 10"
and "dl d2 / 2 = 120"
shows "2 sqrt (dl/2))2= (d2/2))2) 52"
Informal Statement: Sam is carrying a 2 gallon bucket of milk to house from barn, which is miles away from his house. However, the bucket has a leak in it. For each mile he walks, there is as much milk in the bucket as at the beginning of the mile. How many gallons of milk will be in the bucket when Sam gets home? Show that it is
Generated Formal Statement:
theorem
fixes x real
assumes "x (2/3) "3 2"
shows 16/27"
Informal Statement: Expand (2x + 3x*) 1x² 3x 8). Show that is 2x
8x7 + 9x
16r 12x
+ 9
24x
Generated Formal Statement:
theorem
fixes
real
shows x
x²2)
(x"4 x
x x
x 16 x
12 x + 9 x 24 x"2"
Informal Statement: The function (n) = n + n + 17 for 0 S n S 15 generates prime numbers.
What is the value of f(10) - f(9) Show that it is 20.
Generated Formal Statement:
theorem
fixes n :: nat
assumes "\<foral1> <<in> (0..15) 15). prime (n"2 + n + 17)"
shows " ((10: mat)) " 10 17) ((9: mat) "2 + 9 + 17) 20"
Informal Statement: Reversing the digits John's age results his father's age. The positive difference between their ages is 27 years. If the sum of the digits in each age is 5, what is the number of years in John's 's father's 's age? Show that it is 41.
Generated Formal Statement:
theorem
fixes j j1 :: nat
assumes "j = 10
jl + fl"
and "I 10 fl + j1"
and "g = 27"
and "jl fl
shows "t 41
14

---

Published as a conference paper at ICLR 2024
Informal Statement: took Lara five days read novel. Each day after the first day, Lara read half as many pages as the day before. If novel was 248 pages long, how many pages did she read on first day? Show that it is 128.
Generated Formal Statement:
theorem
fixes p1 p2 p3 p4 p5 :: nat
assumes "pl p2
p3 + p4 + p5 248"
and "p2 pl / 2"
and "p3 p2 / 2"
and "p4 p3 / 2
and "p5 p4 / 2
shows "pi 128"
Informal Statement; Alex, Bob, Camille, and Danielle's mothers are comparing their children's ages. They observe that the sum of Alex, Boh, and Danielle's ages is fourteen times Camille's e age. They also note that the sum of Alex and Bob's s ages is six times Camille's age, and Bob's s age is two years less than the difference in ages of Danielle and Alex. How old is Camille? Show that is
Generated Formal Statement:
theorem
fixes a b :: nat
assumes "a > 0"
and "c > 0"
and "d > Q"
and "a b + d 14 c"
and b 6
(d a)
shows "c 1"
Figure 4: Additional examples of faithful formal statements translated from informal statements with correct answers by DTV. Majority voting failed solve these problems but DTV solves them successfully. The model is capable of translating complex informal statements precisely. Note that the "Show that it is [answer]" is appended the original informal problem statement by first extracting the answer from informal solution.
15

---

Published as a conference paper at ICLR 2024
A.2 FAITHFUL SOLUTION FORMALIZATION
Informal Statement: Kailin's favorite restaurant special offer on three-course meal. consists of an appetizer, an entree and dessert. The menu features five appetizers, eight entrees and four desserts. How many different threc-course meals can be formed with these choices? Show that it is 160.
Generated Informal Solution:
We have to choose one of the five appetizers, one of the eight entrees, and one of the four desserts. We have 5 choices for the appetizers, 8 choices for the entrees, and 1 choices for the dessert. Therefore, the number of possible meals is 5 4 160. Final Answer: The final answer 160. I hope it correct.
Generated Formal Statement and Formal Solution:
theorem
assumes "card appetizers 5"
and "card entrees = 8"
and "card desserts 4"
shows "card (appetizers \<times> entrees i<times> desserts) 160" proof
(* We have to choose one of the five appetizers, one of the eight entrees, and of the four desserts. *)
have "card (appetizers \<tineso entrees \<tines> desserts)
card appetizers card entrees * card desserts"
by (simp add: card_cartesian_proodics
(* Therefore, the number of possible meals is 8 8.8 = 160. then. have "card (appetizers \<times> entrees \<times> desserts)
=5
4" using assms
by auto [ATP]
also have "\<dots> 160" simp [ATP]
(* Final Answer: The final answer 160. hope it correct. finally show 2thesis
by auto [A7P]
ged
16

---

Published as a conference paper at ICLR 2024
Informal Statement: Simplify v 192.. Show that it is 8v3.
Generated Informal Solution:
We can factor perfect square from 192: 192 64-3 -3. Thus, we have / v82 8v3. Final Answer: The final answer is 8v3. hope it is correct.
Generated Formal Statement and Formal Solution:
theorem
fixes x :: real
assumes "x = 192"
shows "sqrt
sqrt (3::rea))
proof
(* We factor out perfect square from 192: 192 64 =8- -3.
Thus, have V v82 3 8y3. +)
have "x
unfolding by simp [A7P]
then have "sqrt x = sgrt (64 * 3)
by simp IATP]
also have "\<dots sqrt 64 sqrt 3" using real sqrt mult by blast IATP) also have "\<dots>
sert 3"
by simp [A7P]
finally show ?thesis by simp [ATP]
qed
Informal Statement: What 3 3-88 ,1 Show that
Generated Informal Solution:
By the product rule for exponents, have that
3 8 = ((-00(4-)+4 32
Final Answer: The final answer is hooe it is correct.
Generated Formal Statement and Formal Solution:
theorem
fixes X y :: real
assumes
3 powr (-4)
and "y = 3 powr (-8)"
and "? 3 powr 14"
shows
y
9"
proof
(* By the product rule for exponents, we have that *)
have "x
3 powr (-4) powr (-8) powr 14" by (ent (23) assms assms (2) a3) [ATP]
(* (-4) \odot 3" (-8) Nodot (14) 33(((-))(--)+11))) (2) \boxed 9) *)
also have "(<dot.s> powr (-4 -8 14)
by eval [A7P]
also have "\<dots>>
2"
by auto [ATP]
also have "A<dotg> 9"
by auto [ATP]
(* Final Answer: The final answer is 9. I hope it is correct.
finally show 2thesis
by auto [A7P]
qed
17

---

Published as a conference paper at ICLR 2024
Informal Statement: Simplify: 3!(2² + v9) + 2. Show that is 33.
Generated Informal Solution:
First, we simplify expressions inside the parentheses and the square root.
2 + v 8+3=1 11
Next, we simplify the factorial.
31 3- 2. 1
Now, we can combine three expressions.
31(2 + (9) + 2 6 2 33
Final Answer: The final answer is 33. hope it is correct.
Generated Formal Statement and Formal Solution:
theorem
"fact 3 (2"3 + sqrt 9) 2 = 33"
proof
(* First, simplify the expressions inside the parentheses
and the square root. *)
have "2"3 + sqrt 9 3" by auto [ATP]
(* Next, simplify the factorial. have "fact 3
2"
by (ent (23) fact__ fact fact_numeral prme__ameral_sii simpss [ATP] Final Answer: The final answer is 33. I hope it is correct. *)
(*
then show ?thesis by [A7P]
qed
Figure 5: Additional example problems of which both the informal statement and solution are trans- lated correctly by DTV. The generated formal statement cannot be directly solved by an automated theorem prover. By translating the informal solution step step, the formal statement is proved and the answer is verified. The steps that end with [ATP] are generated by the automated theorem prover.
18

---

Published as a conference paper at ICLR 2024
B FEW-SHOT PROMPT DATA
We provide few-shot prompts used in the experiments in the supplementary material zip file. Below a few-shot prompt example for statement formalization.
Informal Statement: Evaluate log2 64. Show that is 6.
Formal Statement:
theorem
shows "log 2 64
6"
Informal Statement: What is the distance between the points with coordinates (-5, 5) and (5, (5)2 Express your answer in simplest radical form. Show that it 10v2.
Formal Statement:
theorem
fixes x2 y1 y2 :: real
assumes [x1, yl) (-5, 5)* (x2, y2) (5, -5)
shows "sart ((y2 yl) 2 (x2
x1) 22 = 10 sqrt (2)
Informal Statement: If three flicks are equivalent to eight flecks, and six flocks equivalent to four flecks, how many flocks are equivalent to 12 flicks? Show that it 48. Formal Statement:
theorem
fixes flick fleck flock :: real assumes "flick 0" and "flock and "fleck > 0"
assumes "3 * flick
fleck"
and "6 flock = 4 fleck"
shows "48 flock 12 flick"
Informal statement to be formalized here>
C ADDITIONAL DISCUSSION
DTV with GPT3.5. In Table 4 we additionally evaluate the performance of DTV when the informal solutions and their formalization are both generated from GPT3.5. Due to the of OpenAI API, we evaluate only on the MATH Number T'heory category. It can be seen that by leveraging stronger models like GPT3.5, the performance of DTV can be further improved.
Problem Solve Rate
Minerva 62B
GPT-3.5
Single Sample
12.2%
25.0%
Majority Voting
23.7%
41.0%
DTV Formalization with Minerva 62B
31.9%
DTV Formalization with GPT-3.5
36.1 %
49.4% %
Table 4: Comparison of problem solve rates
DTV performance with number of samples. In the experiment section, use 64 samples per problem for majority voting and DTV. In Figure we plot the performance of majority voting and DTV against number of samples per problem Number Theory. It can be that both majority voting and DTV improve as number of samples increase and DTV significantly outperform majority voting when the number of samples is around 20.
Informal answer extraction. To facilitate answer extraction, we include the following answer format in the shot prompt examples: The final answer is [placeholder]. and use regular expressions to extract the answer. certain scenarios, extraction might be more challenging and not only restricted the final answer. In this case, could leverage various semantic parsing methods (Kamath & Das
19

---

Published as a conference paper at ICLR 2024
Problem Solve Rate Number Theory Problems
0.25
Prosfmm Soive
0.25
0.05
0.00
10
20
30
40
50
60
Number of Samples
Figure 6: Comparison of majority voting and DTV.
2018
and possibly use a language model extract the informal reasoning as seen in Kojima et al.
(2022) as well.
Potential improvement of filters. In the main text, discuss and experiment with one symbolic filter that filters out vacuous formal statements. The filter can be leveraged to detect unfaithful statement translations. is also possible to expand this into set of filters that attempt detect trivial formal statements, which are very likely to be unfaithful translations. One type of trivial statements could have the same goal appearing in the assumption already, which makes it provable immediately following the assumption. Another type could have the left-hand side of the goal being the same as that right-hand side. Implementing these filters could potentially further improve the performance at diminishing rate.
DTV helps filter incorrect answer solutions. Besides problem solve rate, we study to what extent DTV can reject incorrect answer solutions present in the informal solution samples. As in Table 5] without autoformalization, the portion of correct answer solutions from Minerva 62B is between 24.3% and 33.9% for different categories. By performing autoformalization and only considering informal solutions whose formal counterparts are proved, the percentage of correct answer solutions increase by more than 20%, indicating the effectiveness of our approach in identifying correct answer solutions. GPT3.5 is better than Minerva 62B at this, which also supports the fact that GPT3.5 leads higher problem solve rate in Table
Table 5: Proportion of correct answer solutions generated by Minerva 62B before and after performing autoformalization. DTV is effective in discarding incorrect answer solutions and lead to better performance.
Correct Answer Rate
Number Theory
Algebra
Prealgebra
No autoformalization
24.3%
31.0%
33.9%
DTV Formalization with Minerva 62B DTV Formalization with GPT3.5
50.5%
45.6%
45.2%
62.3%
56.1%
54.9%
20


Reviews:
[{"review_id": "Q7MHKuqzx7", "reviewer": "Reviewer_wLE8", "summary": "The paper advocates using theorem provers to verify answers generated by language models for quantitative mathematical problems. One starts with a problem in natural language, use language models to generate potential solutions, extract the solutions together with the problem statement and send them to another language model for autoformalization. If the formalized proof is verified by the target theorem prover, then we are sure that one solution is correct without the need of techniques such as majority voting. Additionally, we obtain a rigorous mathematical proof with all gaps closed.\n\nAlthough the big framework of this work is similar to what has been proposed in previous works such as Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs, the experiments conducted here is much more comprehensive, and a few extra mechanisms to help with the performance have also been introduced, such as the filters for faithful translations.", "questions": "See above.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- Comprehensive empirical evaluation and analysis. The results establish the effectiveness of the approach.\n- Excellent section of limitations addressing my concerns that otherwise would have gone into the weakness section below.\n- 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.\n- The paper is well written and easy to follow.", "weaknesses": "Since the authors already included many of my potential criticisms into the section of limitation (which I really like), only a few ones sit here:\n\n- 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).\n\n- 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "7oa2VVm1Uc", "reviewer": "Reviewer_HDyn", "summary": "This paper proposes a technique to improve the performance of LLM in solving mathematical reasoning problems. Although it is reported that LLMs show high performance on \nthese problems, they still make errors in their reasoning steps. The proposed method, Don't trust, verify (DTV), tries to improve the performance of LLMs by leveraging external automated theorem provers. Given a problem written in an informal statement, DTV generates both an informal solution and a formal statement by using an LLM. Then, DTV uses an automated theorem prover to verify the answer. Finally, DTV decides its output by performing majority voting among verified answers. Experimental results show that the proposed method\ncan improve the performance of an LLM in multiple reasoning benchmarks.", "questions": "1. Could you please show how the performance of DTV and Wang 2022 changes with number of samples $n$?\n2. How many queries to an LLM does the proposed method need to obtain a sample solution? \n1. Could you please show how the performance changes if we use different LLMs?\n\n## Minor comment \nThe paper should use \\citet{} command to avoid statements like \"(Cobbe et al., 2021) explores training informal ... (page 1) \"", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "**A clearly written paper:** T his paper is very clearly written. I feel no difficulty reading the paper.\nThe background and related work section are good enough to make the position of the paper clear.\n\n**Tuckles to a well-motivated problem by a simple method:** To improve the performance of the LLM by combining it with external tools is an important research topic.\nThe proposed method requires less additional cost. Therefore, it has the potential to be a handy tool for this kind of problem.\n\n**The proposed method is original and carefully designed:**\nAlthough some ideas of DTV come from DTP (Jiang et al., 2023), there are a considerable amount of differences between DTP and DTV. DTV seems carefully designed for the reasoning \ntask.", "weaknesses": "**Experimental results are not strong:**\nExperimental results show that the proposed method can improve the performance compared with majority voting. However, there are some concerns.\n1. 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\nfrom 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.\n2. 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\nwhen we combine DTV with multiple LLMs, as is reported in (Wang et al., 2022).\n\n**Concerns about the number of samples and the efficiency of the DTV:**\nCompared 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). As reported in (Wang et al., 2022), the performance of majority voting improves as we generate more samples. Therefore, the paper should report how the performance of DTV and majority voting changes when we change the number of samples n, and should \ndiscuss whether such additional cost of DTV pays off. That is, if we need $m$ queries to obtain a sample solution of DTV, then I think the performance of the proposed method\nshould be compared with the majority voting of $nm$ samples.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "4012kKFi9h", "reviewer": "Reviewer_HYaT", "summary": "This paper provides a methodology, DTV, whereby LLMs can leverage libraries of formal mathematics and theorem provers to generate sound mathematical solutions.  This approach outperforms a 'majority voting' benchmark by about 12% on the GSM8K (grade school math questions), and 7% on the full test suite.\n\nDTV operates as follows: given an informal (natural language) problem statement, an LLM produces an informal solution.  The LLM then translates both of these into formal statements.  Manually developed filters then eliminate some of the proposed solutions, whose steps are then checked in a theorem prover.  An answer is selected by majority voting over verified solutions.", "questions": "1. Figure 1, caption: how would results change if, instead of majority voting over all verified solutions, the 'smallest' solution was selected?\n\n1. is it meaningful to run a head-to-head comparison of DTV and Jiang et al.?\n\n1. very minor curiosity (not necessary for the paper): what's the most impressive result that DTV was able to derive?\n\n1. 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?\n\n1. 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.\n\n1. relatedly, could DTV help with Hales' Formal Abstracts project, https://formalabstracts.github.io/ ?  (This seems to have been dormant.)\n\n1. 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?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "**originality**\n\nThe paper is, to my knowledge, original.  Better yet, it is obvious in retrospect.\n\n**quality**\n\nThe paper is well executed.\n\n**clarity**\n\nThe paper is well written.\n\n**significance**\n\nOne of the most obvious drawbacks of LLMs is their lack of soundness.  At the same time their power and flexibility are very impressive.  This paper presents a method for capitalizing on the strength of LLMs while reducing their weaknesses.  I am very confident that the autoformalization literature will continue to gain importance, and that this paper contributes to that literature.", "weaknesses": "Minor typos:\n1. \"treated unverified\" -> \"treated as unverified\"\n1. \"autoforamlization\" -> \"let's see if authors will blindly make any crazy edit a reviewer suggests\"", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "6cdkqXgqfe", "reviewer": "Reviewer_1bgq", "summary": "This paper combines large language models (LLMs) and theorem provers to improve the symbolic reasoning capabilities of the former. Basically, LLMs translate mathematical statements into Isabelle code, which is then used to check for correctness.\nThe proposed approach is evaluated experimentally with favourable results compared to the state-of-the art.", "questions": "p. 3: Is it the case that every yes/no question is translated into a request for proof?\nWhat if I ask \"Is there a proof that \\pi is irrational?\"", "limitations": "", "rating": 3, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 1, "strengths": "1) The proposed translation includes both symbolic and neural filters to improve the statement translation reliability.\n\n2) The related work is discussed in detail.", "weaknesses": "1) The originality and theoretical contribution of this paper is rather limited, as this is mainly the clever combination of two existing tools.\n\n2) 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)