LEVER: Learning to Verify Language-to-Code Generation with Execution

Introduction

The ability of mapping natural language to executable code is the cornerstone of a variety AI applications such as database interfaces (Pasupat & Liang, 2015; Yu et al., 2018; Shi et al., 2020), robotics control (Zhou et al., 2021; Shridhar et al., 2020) and virtual assistants (Agashe et al., 2019; Lai et al., 2022). Recent advances on large language models (LLMs) (Brown et al., 2020; Wei et al., 2021; Chowdhery et al., 2022), especially those pre-trained on code (code LLMs) (Chen et al., 2021a; Fried et al., 2022; Nijkamp et al., 2022; Li et al., 2022a), have shown great promise in such tasks with in-context few-shot learning (Shi et al., 2022; Chen et al., 2022a; Zhang et al., 2022). Yet their performance is still far from perfect (Chen et al., 2021a). Considering the computation cost to finetune such models, it is appealing to explore ways to improve them without changing their parameters.

A key observation is that while LLMs struggles with precision in the few-shot setting, it often produces the correct output when enough samples are drawn. Previous work have shown that majority voting and filtering by test cases can significantly boost their performance when samples are drawn at scale (Chen et al., 2021a; Austin et al., 2021; Li et al., 2022a). Shen et al. (2021) and Cobbe et al. (2021) further demonstrated the effectiveness of training a verifier and using the verification scores to rerank the candidate solutions for math world problems. Comparing to approaches that solely rely on execution consistency and error pruning, trained verifiers can make use of the rich semantic features in the model solutions, such as data types, value range, and variable attributes, which can be strong indicators of correctness of the programs. While Cobbe et al. (2021) and subsequent work (Li et al., 2022b; Kadavath et al., 2022) focus on verifying natural language solutions by LMs, a natural question is whether the same approach can be applied to program solutions.

In this work, we propose learning to verify (Lever) language-to-code generation by code LLMs, with the help of execution. More specifically, we train a verifier that learns to distinguish and reject incorrect programs based on the joint representation of the natural language description, the program surface form and its execution result. We further combine the verification probability with the LLM generation probability and marginalize over programs with the same execution results. We use this aggregated probability as the reranking score and output the programs that execute to the most probable result.

We conduct extensive experiments on four different language-to-code benchmarks across domains of text-to-SQL semantic parsing, table QA, math reasoning and basic Python programming. Experiment results with three different code LLMs show that Lever consistently improves the execution accuracy of the generated programs. Notably, Lever coupled with code-davinci-002 improves over strong baselines that use execution error pruning by 4.6% to 10.9%, and achieves the new state-of-the-art results on all four benchmarks, without using task-specific model architecture or prompting methods. Ablation studies show that execution results are crucial for the verification and Lever also yields non-trivial improvements in low-resource and weakly-supervised settings.We open-source our experiment code for reproducibility: https://github.com/niansong1996/lever. Following Cobbe et al. (2021), by “verifying” we mean assessing whether a program’s functionality matches its programmer’s intent. This is distinct from the notion of formal verification in programming languages (Seligman et al., 2015).

Approach

We now introduce the detailed formulation and training procedures of Lever. The key components are illustrated in Figure 1.

The input for a language-to-code task typically consists of the natural language (NL) description and optionally some programming context (e.g., data stores, assertions and so on). We denote such input as $x$. Given $x$, a generation model $P(y|x)$ generates a program $y$ which is later executed via an executor $\mathcal{E}(\cdot)$ to obtain the resultSome datasets such as Spider (Yu et al., 2018) require the input values to be generated together with the programs, hence $y^{*}$ is directly executable. Others require the programs to be executable on separately provided test cases, e.g., MBPP (Austin et al., 2021). We adopt this notation for simplicity. $\mathcal{E}(y)$. For few-shot learning with large LMs, the generation is also often conditioned on a fixed set of $m$ exemplars, $\{(x_{i},y_{i})\}_{i<m}$. Thus the few-shot language-to-code generation with code LLMs can be formulated as:

where $\operatorname{prompt}(x,\{(x_{i},y_{i})\}_{i<m})$ is a string representation of the overall input. Greedy search is typically used to find the program with the (approximately) highest generation probability, i.e., $\hat{y}_{\text{greedy}}\thickapprox\arg\max_{y}P_{\mathbf{LM}}(y|x)$.

2 Reranking of Program Candidates

The key observation motivating our method is that a reasonably large sample set from $P_{\mathbf{LM}}(y|x)$ often includes the correct programs. This suggests that reranking of the program candidates may yield significant result improvement. The idea of discriminative reranking (Shen et al., 2004; Collins & Koo, 2005) is to learn a scoring function $R(x,\hat{y})$ that measures how likely $\hat{y}$ is the best output for input $x$. Given $R(\cdot)$, the reranker outputs the program with the highest reranking score among the set of candidates $S$:

Next we introduce how we adopt a trained verifier to verify and rerank program candidates sampled from code LLMs such that $\hat{y}_{\text{rerank}}$ is better than $\hat{y}_{\text{greedy}}$.

Given input $x$, instead of performing greedy search, we obtain $k$ programs from $P_{\mathbf{LM}}(y|x)$ with temperature sampling, i.e., $\{\hat{y}_{i}\}_{i=1}^{k}\sim P_{\mathbf{LM}}(y|x)$. As the same programs may be sampled more than once, we perform deduplication to form a set of $n$ unique program candidates $S=\{\hat{y}_{i}\}_{i=1}^{n}$, where $n\leq k$. We choose to do sampling instead of beam search mainly for two reasons: 1) recent work suggests that beam search for code generation typically results in worse performance due to degenerated programs (Austin et al., 2021; Zhang et al., 2022); and 2) beam search is not available or efficiently implemented for all LLMs that we test on (e.g., Codex).

Verification with Execution.

We use a simple concatenation of the problem description $x$, candidate program $\hat{y}$ and a representation of its execution results $\mathcal{E}(\hat{y})$ as the input to the reranker. Inspired by recent work (Cobbe et al., 2021; Li et al., 2022b), we parameterize our discriminative reranker as a verification (i.e., binary classification) model $P_{\theta}(v|x,\hat{y},\mathcal{E}(\hat{y}))$, where $v\in\{0,1\}$. In practice, the reranker can be implemented using any binary classification architecture. We report experiments using T5 (Raffel et al., 2020) and RoBERTa (Liu et al., 2019) in §B.2.

Given an input $x$ and a candidate program $\hat{y}\in S$, we obtain the reranking probability as the joint probability of generation and passing the verification:

Execution Result Aggregation.

Since programs with the same semantics may have different surface forms, we further aggregate the reranking probability of the programs in $S$ that executes to the same result. In this way, we relax the dependency on the surface form and focus on the execution results instead. The final scoring function for reranking is therefore:

Since there might be several programs that share the same execution result of the highest probability, we break tie randomly in this case when outputting the programs.

3 Learning the Verifiers

The previous sections described how to use a verifier at inference time. Next we introduce its training process.

Learning Objective.

Given this set of verification training examples, we formulate the loss for input $x$ with the negative log-likelihood function, normalized by the number of program candidates

The normalization step is important to prevent an example with a large number of unique program candidates to dominate learning.

Experimental Setup

We conduct experiments on four language-to-code datasets across domains of semantic parsing, table QA, math reasoning and basic python programming. The main settings of these four datasets are shown in Table 1. More detailed settings for verification are in Table 7 of the Appendix.

$\triangleright$ Spider (Yu et al., 2018) is a semantic parsing dataset on generating SQL queries from natural language questions. With 7k parallel training data, it is also ideal for finetuning generators; $\triangleright$ WikiTableQuestions (WikiTQ) (Pasupat & Liang, 2015) is a table question answering dataset, for which we attempt to solve by generating and executing SQL queries over the source tables. We use the preprocessed tables from Shi et al. (2020) and adopt their annotated SQL queries for adding gold programs for the originally weakly-supervised dataset; $\triangleright$ GSM8k (Cobbe et al., 2021) is a benchmark for solving grade-school level math word problems. Following previous work (Chowdhery et al., 2022; Chen et al., 2022b; Gao et al., 2022), we approach this benchmark by generating Python programs from questions in NL, which should produce the correct answer upon execution. The original dataset only has natural language and not program solutions, thus it is weakly-supervised for language-to-code; $\triangleright$ MBPP (Austin et al., 2021) contains basic Python programming programs stated in natural language. Each example is equipped with 3 test cases to check the correctness of the programs. Following previous work (Shi et al., 2022; Zhang et al., 2022), we use the first test case as part of the prompt for the model to generate correct function signatures and use all three of them for evaluating correctness.

2 Code LLMs

We evaluate Lever with three different code LLMs: $\triangleright$ Codex (Chen et al., 2021a) is a family of code LLMs of different sizes developed by OpenAI. Specifically, we use the code-davinci-002 APIhttps://openai.com/api/ through its official Python bindings. $\triangleright$ InCoder (Fried et al., 2022) is a family of code LLMs up to 6B parameters trained on a large corpus of code with permissively licenses. We experiment with InCoder-6B and use it for left-to-right generation. $\triangleright$ CodeGen (Nijkamp et al., 2022) is a family of code LLMs and we evaluate the CodeGen-16B-multi version. Although SQL files are not included in the training corpus for CodeGen, we found it to still perform reasonably well on SQL generation tasks possibly because the SQL queries were mixed in with source files of other programming languages.

3 Baselines and Evaluation Metric

We compare Lever to the following baseline approaches for generating programs using code LLMs. $\triangleright$ Greedy: Select the most likely token per decoding step. $\triangleright$ Maximum Likelihood (ML): From $k$ sampled program candidates, select the program with the highest generation log-probability, i.e., $\log P_{\mathbf{LM}}(\hat{y}|x)$ (or normalized generation log-probability as $\log P_{\mathbf{LM}}(\hat{y}|x)/|\hat{y}|$). We determine empirically using the development set whether to use the normalized probability for each dataset. More details can be found in Appendix A. $\triangleright$ Error Pruning + ML (EP + ML): Prune out the candidate programs with execution errors; then select the program with the maximum likelihood; $\triangleright$ Error Pruning + Voting (EP + Voting): Take the majority vote on the execution results among the error-free programs, and select the most-voted execution result and its corresponding programs.

We focus on comparing with the EP+ML baseline, as it is a simple reranking method that exploits execution and yields competitive results consistently across different datasets and code LLMs.

Evaluation metric.

Following previous work (Xie et al., 2022; Liu et al., 2021; Ni et al., 2022; Zhang et al., 2022), we use execution accuracy as the main evaluation metric for all datasets, which measures the percentage of examples that yields the gold execution result or pass all test cases.

4 Implementation Details

We create the verification training data by sampling from the LLMs on the training set, using the sampling budget described in Table 1. More statistics of the resulting training data can be found in Table 7 in the Appendix. When learning the verifiers, as shown in Eq. 4, the training loss is computed by averaging over all the program samples for each example. As we batch the program samples for the same examples together, the effective batch size will also be multiplied by the sample size. This could be problematic when sample size gets large (up to 100 in our experiments) as they may not be able to fit into the GPU memory at once. Therefore, we down-sample the programs used for learning per example in each iteration. The random down-sampling happens at the beginning of every epoch of training so the verifiers are able to see different programs each epoch. Detailed batch sizes and downsampling factor can be found in Table 7 in the Appendix.

Execution result representation.

The input to the verifier is a concatenation of the task input, the candidate program and its execution results. For Spider and WikiTQ, we use the linearized resulting tables from SQL execution as the execution results. For GSM8k, we use the value of the variable named “answer” after executing the program as the execution results. For MBPP, we use the type and value (casted to string) returned by the functions. All execution errors are represented as “ERROR: [reason]”, such as “ERROR: Time out”. Examples of these verifier inputs for different datasets can be found in Table 11.

Verifier model selection.

We use the development set to choose the best verifier model. We select T5-base for Spider, T5-large for WikiTQ and MBPP, and RoBERTa-large for GSM8k as the base LM for the verifiers to use in the main experimentsWe attempted using the code LLM itself as the verifier in a few-shot manner, but the performance is inferior than EP+ML. . The selection process is detailed in § B.2. For the T5 models (Raffel et al., 2020), we train them to output the token “yes/no” for each positive/negative example given the verifier input, and we take the probability of generating “yes” as the verification probability during inference. For RoBERTa (Liu et al., 2019), we add a linear layer on top of the [CLS] head, following the standard practice of sequence classification with encoder-only models (Devlin et al., 2019).

The details of LLM sampling, few-shot prompt construction and dataset-specific setups can be found in Appendix A.

Main Results

We show the performance of Lever coupled with Codex-Davinci and compare it with the state-of-the-art finetuning and few-shot performances from previous work for Spider (Table 2), WikiTQ (Table 3), GSM8k (Table 4) and MBPP (Table 5). In addition, we also evaluate Lever with InCoder and CodeGen models on Spider and GSM8k (Table 6).

Lever consistently improves the performance of all code LLMs on all tasks, yielding improvements of 6.6% (Spider) to 17.3% (WikiTQ) over the greedy decoding baselines for Codex-Davinci. For weaker models such as InCoder and CodeGen, we observe improvements up to 30.0% for Spider and 15.0% for GSM8k. Moreover, Lever combined with Codex-Davinci also achieves new state-of-the-art results on all four datasets, with improvements ranging from 1.2% (WikiTQ) to 2.0% (MBPP). On the challenging text-to-SQL dataset, Spider, where the previous state-of-the-art is achieved by finetuning a T5-3B model augmented with relational-aware self-attention, we achieved even better results with Codex-Davinci + Lever, where the verifier is finetuned using a T5-base model. Lever also improves the previous best results on Spider using InCoder and CodeGen, by 13.2% and 20.6%, respectively.

As Lever is a simple method that combines few-shot LM generation with learned verifiers, it can potentially benefit more advanced prompting methods (Li et al., 2022b; Cheng et al., 2022) or model architectures (Qi et al., 2022; Wang et al., 2020), which we leave as future work.

2 Ablations with Lever

We perform ablation study for Lever with Codex-Davinci and compare with the baselines mentioned in § 3.3, and the results are shown in Figure 2. The same ablations are conducted for InCoder and CodeGen with results in Table 6. In these results, we include an “Oracle” performance which is obtained by always selecting the correct program as long as they appear in the sample set.

According to Figure 2, the performance drops considerably on all four benchmarks when execution result is removed from the verifier input, indicating that the execution outcome is important for verifier training. The effect varies across different datasets. While it causes an absolute performance drop of 6.6% and 5.6% for WikiTQ and MBPP, as the drop is smaller for Spider (3.0%) and GSM8k (1.2%). We found the code samples for WikiTQ and MBPP contain more execution errors, which explains why our approach is more effective on these two datasets. Table 6 shows similar trends for InCoder-6B and CodeGen-16B on Spider and GSM8k. The smaller LMs have worse few-shot performance and removing the execution information from the verifier often results in even greater performance drops. Moreover, we found that Lever in general outperforms the EP+ML baseline, indicating that the verifiers can make use of clues beyond simple execution errors. More detailed quantitative analysis of when execution information helps is in Figure 6.

Effect of execution result aggregation.

Aggregating the programs with the same execution result is a simple and widely used technique (Chen et al., 2022b; Cheng et al., 2022). We find execution aggregation work well with Lever on datasets with Python output, but only marginally benefit the SQL datasets. A probable reason is that the Python code structure is more flexible than that of the domain-specific languages as SQL. In the database querying domain, it is more likely for an incorrect program to execute to some trivial but wrong results (e.g., “0” or empty table). After aggregation, such incorrect results may accumulate enough probability mass to out-weight the correct one, leading to negative impact on the performance.

Weakly-supervised settings.

We also compare the performance of Lever under fully- and weakly-supervised settings. Figure 2 and Table 6 show that the performance of Lever is largely preserved when the gold programs are not given and the weakly-supervised setting is used (§2.3), with an absolute performance drop up to 1.1%. This suggests that Lever works well under the weakly-supervised settings, and the program itself is less informative for verification comparing to the execution results.

Analysis

We show how the performance of Lever changes with fewer training examples in Figure 3, using Spider as an example. More results on WikiTQ and GSM8k are in § B.3. The improvements with Lever over base LLMs are still consistent even when only 250 examples are given, with improvements ranging from 1.7% to 10.0% over different datasets and LLMs. This suggests that Lever can work under few-resource settings. Moreover, the trend also varies for different datasets and code LLMs, for example, when using Codex as the LLM, the performance of Lever drops by 6.4% for WikiTQ and only 3.2% for Spider. However, also on Spider, the performance is lowered by 6.9% and 5.3% for InCoder and CodeGen. This suggests that having more training examples for Lever has larger effect for harder datasets and weaker LMs.

With Figure 3, we also compare the performance of Lever with the T5 models being directly finetuned for generation given the same number of training examples. While verification can be learned with only hundreds of examples, the performance of finetuned T5 models drastically drops when less training examples are available. As an example, for 500 examples, a T5-base verifier on InCoder/CodeGen outperforms a finetuned T5-3B generator by $\sim 7\%$.

2 Sample Size Scaling

Since drawing samples from LLMs in may be costly computational-wise, here we study the how sample size during training and inference time affects the performance. As we can see from 4(a), during inference time, when lowering the sample size from 50 to 10 programs per example, the performance of Lever drops by 1.8% (Spider) to 5.2% (WikiTQ). This indicates that the Lever is sensitive to the sample size at inference time, which is expected as it also greatly affects oracle results (i.e., the upper-bound for reranking). In comparison, 4(b) shows that Lever is highly insensitive to the sample size for providing training data, with the performance gap all below 1% for the three datasets. Overall, the results show that a higher sampling budget helps more at test time.

3 Verifier and Generator Calibration

We study how well-calibrated are the verifier and generator in identifying correct programs. Ideally, correct program samples shall be given higher probabilities thus we should observe higher percentage of programs being correct when it is closer to the top. To this end, we sort the prediction scores of the verifier, the generator and LEVER (as in Eq. 3), and move the percentile threshold and measuring the percentage of correct programs in the top ranked programs. According to Figure 5, the verifiers are generally better calibrated than the generators, especially when the threshold is in the lower percentiles. This indicates that it is easier for the verifiers to identify obvious mistakes in the programs with execution results as part of their input. Interestingly, when distinguishing between the top-ranked programs, the verifiers are poorly calibrated in three of the four tested datasetsOur hypothesis is that the programs ranked at the top have very similar form and execution results (e.g., same type and range), making it hard for a small, though finetuned, model to discriminate.. However, the generators are generally better calibrated in this region, and combining the probability of the verifier and the generator yields the best results on all four benchmarks. More specifically, on the GSM8k dataset, where the calibration of both models are quite poor for top-ranking programs, their joint probability is surprisingly well-calibrated, showing that the two models complement each other on this dataset.

4 Quantitative Analysis

We present a quantitative analysis on why Lever successfully or failed to improve the performance of LLMs. According to Figure 6, when Lever reranks a program to replace another with higher generation probability, it is oftentimes because the execution results provide crucial information such as execution errors, variable type and range. This is consistent with our findings in § 4.2 about the importance of execution results for Lever. It is also worth noticing that there are cases when Lever is still able to rerank the correct program when the error-free execution results are of the same type and range with the greedy program, i.e., in “others” category. Our hypothesis is that this is when the program itself becomes the main feature for the verifiers to exploit. In addition, when Lever fails to rank correct programs to the top, the most common reason is that no correct program can be found in the samples (i.e., upper-bound is reached), which is especially the case for weaker LMs. The second most common reason for Lever to fail is that the execution results of the incorrect program upon reranking has the same type and range as the correct program in the samples. In this case, execution results do not provide rich information for the verifiers thus Lever fails to improve code LLMs.

Related Work

Translating natural language to code is a long-standing challenge through all eras of artificial intelligence, including rule-based systems (Woods, 1973; Templeton & Burger, 1983), structured prediction (Zelle & Mooney, 1996; Zettlemoyer & Collins, 2005; Gulwani & Marron, 2014) and deep learning (Xiao et al., 2016; Dong & Lapata, 2016; Rabinovich et al., 2017; Zhong et al., 2017; Lin et al., 2017). Recently, pre-trained code language models (Chen et al., 2021a; Wang et al., 2021; Fried et al., 2022; Nijkamp et al., 2022; OpenAI, 2022) have demonstrated surprisingly strong performance in this problem across programming languages (Lin et al., 2018; Yu et al., 2018; Austin et al., 2021; Cobbe et al., 2021; Li et al., 2022a). A number of approaches were proposed to refine LLM sample selection, including test case execution (Li et al., 2022a), cross-sample similarity (Chen et al., 2021a; Li et al., 2022a; Shi et al., 2022) and maximum mutual information (Zhang et al., 2022) based filtering. Our work proposes a learnable verification module to judge the sample output of LLMs to further improve their performance.

Code Generation with Execution.

Previous code generation work have exploited execution results in different ways. Weakly-supervised learning approaches (Berant et al., 2013; Pasupat & Liang, 2015; Guu et al., 2017) model programs as latent variables and use execution results to derive the supervision signal. Intermediate execution results were used to guide program search at both training (Chen et al., 2019, 2021b) and inference time (Wang et al., 2018). When sampling at scale, majority voting based on the execution results has been shown effective for candidate selection (Li et al., 2022a; Cobbe et al., 2021). Shi et al. (2022) generalizes this principle by selecting samples that have the maximum concensus with other samples in the execution results. We propose to train a verification model to judge the correctness of code generation taking the execution results into account.

Learning to Verify.

Previous work have shown the effectiveness of learned verifiers for sample filtering in domains such as math QA (Shen et al., 2021; Cobbe et al., 2021) and commonsense QA (Li et al., 2022b), where the solution is mostly described in natural language. While it is more common to train the verifiers independently from the generator (Cobbe et al., 2021; Li et al., 2022b), Shen et al. (2021) jointly fine-tuned both at the same time. Previous work have also used different base LMs for the verifiers. Cobbe et al. (2021) uses GPT-3 (Brown et al., 2020) while Li et al. (2022b) uses DeBERTa (He et al., 2020). Besides task-specific verifiers, Kadavath et al. (2022) shows that large LMs can self-verify their output in a few-shot setting for a wide range of tasks. Chen et al. (2022a) and other works (Tufano et al., 2020; Li et al., 2022a) use LMs to generate test cases instead of directly judging the correctness of the output programs. In comparison, the setting of Lever is closer to Li et al. (2022b) as we train the verifier separately and use a much smaller LM for it (approximately $0.5\%$ of the generator parameter size). We report the first set of comprehensive evaluation on language-to-code tasks, making use of the program execution resultsWhile Kadavath et al. (2022) also reported self-verification results on HumanEval, their approach does not leverage execution..

Discriminative Reranking.

Discriminative reranking approaches have long been used to further improve the performance of sequence generation tasks, including summarization (Wan et al., 2015), machine translation (Shen et al., 2004; Lee et al., 2021), dialogue response generation (Olabiyi et al., 2018) and more rencently, code generation (Yin & Neubig, 2019). Lever can be viewed as a discriminative reranking framework.

Limitations

In this work, we use execution information to verify the programs in Lever. However, the execution of the programs depends on at least one set of inputs (e.g., arguments for a function) and adequate execution context (e.g., databases), which may not be provided for certain applications. Moreover, we can not always assume that model-generated programs are safe to execute. In addition, we pass@$1$ as the main evaluation metric in the experiments. While it is ideal for applications such as text-to-SQL and math reasoning where the users are only looking for answers to their questions, metrics as pass@$k$ or n@k could provide different perspectives for general programming tasks as MBPP.

Conclusion

We propose Lever, a simple approach for improving code LLMs on language-to-code tasks, by learning separate verification models to judge the correctness of the generated programs, taking their execution results into consideration. We show that it is possible to train verifiers approximately 0.5% the size of the generators using supervised benchmark datasets. Instead of directly perform rejection sampling based on the verifier output, we show it is better to mix the generation and verfication probabilities for sample reranking. Lever consistently improves the performance of code LLMs on four language-to-code tasks, and achieves new state-of-the-art results on all of them. Further analysis suggest that the program execution results are crucial for verification and the proposed approach is generalizable across different LLMs.

Acknowledgements

The authors would like to thank Xi Ye, Tianyi Zhang, Mengzhou Xia, Luke Zettlemoyer, and the anonymous reviewers for the useful discussion and comments.

References

Appendix A Additional Implementation Details

We use temperature sampling to obtain program candidates given the input formats and sampling hyperparameters as described in Table 7. We set the temperature as $T=0.6$ for Codex and $T=0.8$ for InCoder and CodeGen, as the optimal temperatures for the best pass@k by referring to the original papers (Fried et al., 2022; Nijkamp et al., 2022). An ablation study on sampling budget is reported in §5.1.

Few-shot prompt construction.

The numbers of few-shot exemplars to include in the prompt for different datasets are shown in Table 1. All exemplars are randomly sampled and ordered from the training set, with the exception of MBPP, where we use the 3 examples provided by the original dataset. Full prompts used for each dataset are shown in Appendix C.

Dataset-specific setups.

The detailed experiment setups for specific datasets are shown as Table 7. In particular, we use normalized probability for GSM8k and MBPP datasets as we find these two datasets can benefit from such normalization. We think this is because the Python programs have higher variance in length due to the flexible grammar and being more expressive. Moreover, the percentage of positive labels also denotes the “random” baseline, which is the expected execution accuracy by randomly picking from the sampled programs. This provides the additional perspective of the ability of the code LLMs, as well as the difficult of learning the verifiers for them.

Verifier Input Examples

Here we show examples of the inputs to the verifiers for different datasets in Table 11.

Appendix B Additional Results

One other way to avoid the cost of sampling from code LLMs is to train verifiers using samples from one LLM and directly apply to the programs sampled from a different LLM, i.e., between LLM transfer, and we show the results of such on Spider and GSM8k in Table 8. From the results, we can first observe that Lever still non-trivially improves the baseline performance most of the time, with the exception of transferring from InCoder and CodeGen to Codex on the GSM8k dataset. This suggests that the knowledge learned by the verifiers are generalizable to different LLM outputs. Moreover, we can see that the transfer typically works better when the percentage of positive labels are closer, as the transfer is more successful between the InCoder and CodeGen models than that with Codex. These results show between-LLM transfer as an interesting way to reduce the training data need for Lever.

B.2 Ablation on Base LMs for Verification

In this work, we treat the choice of base models for the verifiers as a hyperparameter and use the best performing model for further experiments. Here we show the performance of all the base models we attempted on the four datasets, with results in Table 9.

B.3 Training Example Scaling for WTQ and GSM8k

Due to space limit, we are only able to show the ablation in number of training example for Spider. Here in Figure 7, we show the results for WikiTQ and GSM8k as well. From the results, we can see that the learning of Lever is also very data efficient on those two benchmarks, as non-trivial improvements can be observed even when only 250 training examples are given.

B.4 WikiTQ Results with the Official Evaluator

Following Cheng et al. (2022), we fix the official evaluator of WikiTQ by normalizing units, Boolean values, etc. Here we also report the performance of Lever with previous work based on the official WikiTQ evaluator in Table 10. From the results, we can see that Lever still presents the state-of-the-art result under this setting.

B.5 Case Study

Here we give some concrete examples to illustrate how Lever work and when does it fail in Table 12. In the first example from the Spider dataset, we can see that program candidate $\hat{y}_{2}$ selects from the wrong table, which results in an execution error. This is easily detected by the verifier thus put a low verification probability on such program. Meanwhile, the execution result $\hat{z}_{1}$ from program $\hat{y}_{1}$ seems much more likely to be the answer of the question to the verifier. In the second example from WikiTQ, however, the execution results $\hat{z}_{1}$ and $\hat{z}_{2}$ do not provide clear information as they are both county names. In this case, the verifier does not possess much more meaningful information than the generator, thus not able to identify the incorrect program.

Appendix C Prompts for Few-shot Generation

Finally, we append the full prompts we used for few-shot prompting the code LLMs for Spider (Appendix C, Appendix C, Appendix C), WikiTQ (Appendix C, Appendix C), GSM8k (Appendix C, Appendix C), and MBPP (Appendix C).