Source-linked AI summary
LEVER: Learning to Verify Language-to-Code Generation with Execution
Ansong Ni, Srini Iyer, Dragomir Radev, Ves Stoyanov, Wen-tau Yih, Sida I. Wang, Xi Victoria Lin
TL;DR
Code LLMs remain imperfect, while test cases are difficult to obtain and execution heuristics miss semantic correctness signals. LEVER learns verifiers from inputs, programs, and execution results, then reranks candidates; it consistently improves four benchmarks and reaches state-of-the-art results.
Problem
Code LLM performance remains imperfect, while obtaining test cases is challenging and execution heuristics poorly capture semantic correctness signals.
Method
LEVER trains verifiers on the input, program, and execution result, then combines verification and generation probabilities while marginalizing programs with identical results for reranking.
Results
4.6% to 10.9% improvement over strong execution-error-pruning baselines with code-davinci-002, with new state-of-the-art results on all four benchmarks.
Takeaways & Limitations
LEVER consistently improves code LLMs across four language-to-code tasks, and execution results are crucial for verification.
Takeaways & Limitations
Execution-based verification requires suitable inputs and execution context, and generated programs may not always be safe to execute.
Abstract
from arXiv · showhide
The advent of large language models trained on code (code LLMs) has led to significant progress in language-to-code generation. State-of-the-art approaches in this area combine LLM decoding with sample pruning and reranking using test cases or heuristics based on the execution results. However, it is challenging to obtain test cases for many real-world language-to-code applications, and heuristics cannot well capture the semantic features of the execution results, such as data type and value range, which often indicates the correctness of the program. In this work, we propose LEVER, a simple approach to improve language-to-code generation by learning to verify the generated programs with their execution results. Specifically, we train verifiers to determine whether a program sampled from the LLMs is correct or not based on the natural language input, the program itself and its execution results. The sampled programs are reranked by combining the verification score with the LLM generation probability, and marginalizing over programs with the same execution results. On four datasets across the domains of table QA, math QA and basic Python programming, LEVER consistently improves over the base code LLMs(4.6% to 10.9% with code-davinci-002) and achieves new state-of-the-art results on all of them.
1. Introduction
LEVER improves few-shot language-to-code generation by learning to verify sampled programs using their execution results, then reranking candidates. Across four benchmarks, it consistently improves code LLM performance and reaches state-of-the-art results.
- Language-to-code generation supports applications including database interfaces, robotics control, and virtual assistants.
- Code LLMs show promise with few-shot learning, but their performance remains imperfect and parameter-efficient improvement is desirable.
- Large samples from code LLMs often include correct programs, motivating candidate filtering, majority voting, and verifier-based reranking.
- LEVER trains a verifier on the natural-language input, program surface form, and execution result to estimate program correctness.
- 4.6% to 10.9% improvement over strong execution-error-pruning baselines with code-davinci-002, alongside new state-of-the-art results on four benchmarks.The benchmarks cover text-to-SQL semantic parsing, table QA, math reasoning, and basic Python programming.
2. Approach
LEVER samples and executes candidate programs, verifies them using their inputs, code, and execution results, and reranks them using combined generation and verification probabilities. Its verifier is trained from sampled programs labeled by whether their execution matches the gold result.
- Language-to-Code Generation with Code LLMs: LEVER formulates language-to-code generation as sampling programs conditioned on task inputs and few-shot exemplars.
- Reranking of Program Candidates: Rather than relying only on greedy decoding, LEVER samples k programs, deduplicates them, and forms a candidate set for reranking.Sampling avoids degenerated programs associated with beam search and accommodates models where beam search is unavailable or inefficient.
- Verification with Execution: A binary verifier estimates correctness from the task input, candidate program, and execution result.
- Reranking of Program Candidates: LEVER combines LLM generation probability with verification probability, then aggregates candidates sharing an execution result to reduce dependence on program surface form.
- Training Data Creation: Verification labels compare each candidate's execution result with the gold result, while gold programs are added as positive examples when available.Weakly supervised datasets provide gold execution results without gold programs.
- Learning Objective: The verifier loss is normalized by the number of unique candidates so examples with many candidates do not dominate training.
3. Experimental Setup
LEVER is evaluated across four language-to-code datasets using multiple code LLMs, execution-based baselines, and execution accuracy. The setup also specifies verifier inputs and model selection procedures.
- Datasets: Four benchmarks cover semantic parsing, table QA, math reasoning, and basic Python programming.The datasets are Spider, WikiTableQuestions, GSM8k, and MBPP.
- Code LLMs: Three code LLM families—Codex, InCoder, and CodeGen—provide the generation models.The main Codex experiments use code-davinci-002, alongside InCoder-6B and CodeGen-16B-multi evaluations.
- Baselines and Evaluation Metric: Baselines include greedy decoding, maximum likelihood, execution-error pruning with maximum likelihood, and execution-error pruning with voting.The study focuses particularly on EP + ML, which uses execution errors before likelihood-based selection.
- Baselines and Evaluation Metric: Execution accuracy measures the percentage of examples producing the gold execution result or passing all test cases.This metric is used across all datasets.
- Implementation Details: The verifier receives the task input, candidate program, and execution results, with result representations varying by dataset.Representations include linearized SQL tables, an answer variable's value, returned type and value, and explicit execution-error strings.
- Implementation Details: Development-set selection chooses T5-base for Spider, T5-large for WikiTQ and MBPP, and RoBERTa-large for GSM8k.T5 verifiers predict yes/no, with the probability of yes used as the verification probability.
4. Main Results
LEVER improves execution accuracy across language-to-code benchmarks and code LLMs, while ablations show that execution results and result aggregation affect its effectiveness.
- LEVER consistently improves all code LLMs on all tasks, with Codex-Davinci gains of 6.6% to 17.3% over greedy decoding.
- LEVER with Codex-Davinci achieves new state-of-the-art results on four datasets, improving prior best results by 1.2% to 2.0%.
- Removing execution results from verifier inputs causes absolute performance drops of 1.2% to 6.6% across datasets.The largest drops occur on WikiTQ and MBPP, while Spider and GSM8k show smaller declines.
- LEVER generally outperforms EP+ML, indicating that its verifiers use clues beyond simple execution errors.
- Execution-result aggregation helps Python-output datasets but provides only marginal gains on SQL datasets.Incorrect SQL programs may accumulate probability mass on trivial wrong results such as “0” or an empty table.
- Weak supervision preserves LEVER’s performance with an absolute drop of at most 1.1% when gold programs are unavailable.
5. Analysis
LEVER’s gains depend on sampling and execution-aware verification: more examples and inference samples generally help, while execution results improve calibration and reranking. Its joint probability can complement weak generator and verifier calibration, but failures remain when correct candidates are absent or execution signals overlap.
- Training Example Scaling: 1.7% to 10.0% improvements over base LLMs persist with only 250 training examples, supporting LEVER in few-resource settings.The effect of additional training data is larger for harder datasets and weaker language models.
- Training Example Scaling: ∼7%: a T5-base verifier on InCoder/CodeGen outperforms a finetuned T5-3B generator with 500 examples.Verification remains learnable with hundreds of examples, while directly finetuned T5 generation degrades sharply with fewer examples.
- Sample Size: 1.8% to 5.2%: reducing inference samples from 50 to 10 programs lowers LEVER performance on Spider to WikiTQ.The result indicates sensitivity to inference sample size; higher sampling budgets help more at test time.
- Verifier Calibration: On GSM8k, the combined generator-verifier probability is well-calibrated even though both individual models calibrate poorly for top-ranked programs.The authors describe this as evidence that the two models complement each other on this dataset.
- Success and Failure Analysis: LEVER often succeeds because execution exposes errors, variable types, or value ranges, but fails when no correct sample exists or execution signals overlap.The latter failure occurs when an incorrect reranked program has the same type and range as a correct sampled program, especially for weaker models.
6. Related Work
Related work uses execution for supervision, search guidance, voting, and filtering, while learned verifiers have mainly been studied for natural-language solutions. LEVER separately trains a much smaller verifier and provides comprehensive execution-based evaluation on language-to-code tasks.
- Language-to-Code Generation: Prior language-to-code systems span rule-based, structured-prediction, deep-learning, and pretrained code-language-model approaches.Recent code LLMs use in-context few-shot learning but remain imperfect and costly to finetune.
- Code Generation with Execution: Execution has supported weak supervision, program-search guidance, majority voting, and sample filtering in prior code-generation work.These approaches use execution at training or inference time in different ways.
- Learning to Verify: Learned verifiers have been effective for math and commonsense QA, where solutions are mostly described in natural language.Prior work commonly trains verifiers independently from generators or uses language models to generate test cases.
- Learning to Verify: LEVER trains a separate verifier approximately 0.5% the size of the generator and evaluates execution-based verification comprehensively on language-to-code tasks.The paper positions this setting near independently trained-verifier approaches while using a much smaller language model.
- Discriminative Reranking: LEVER can be viewed as a discriminative reranking framework, connecting it to reranking methods for sequence generation and code generation.The related-work framing includes summarization, translation, dialogue, and code-generation applications.
7. Limitations
LEVER depends on executable programs, inputs, and adequate execution context, and execution safety cannot always be assumed. Its experiments emphasize PASS@1, whereas PASS@k or N@k may offer different perspectives for general programming tasks.
- Execution Requirements: LEVER requires program inputs and adequate execution context, such as function arguments or databases, which may be unavailable in some applications.This constrains execution-based verification beyond the evaluated settings.
- Execution Safety: Model-generated programs cannot always be assumed safe to execute, creating a practical boundary for execution-based verification.The limitation is stated as a general safety concern rather than a reported experimental failure.
- Evaluation Scope: PASS@1 is the main evaluation metric, while PASS@k or N@k could provide different perspectives for general programming tasks such as MBPP.The authors consider PASS@1 especially suitable when users seek answers to questions.
8. Conclusion
LEVER improves code LLMs by separately learning verification models that use execution results, combining verification and generation probabilities for reranking. It consistently improves four language-to-code tasks, reaches state-of-the-art results, and generalizes across LLMs.
- Conclusion: LEVER learns separate verification models that judge generated-program correctness using execution results.The verifiers can be trained at approximately 0.5% of the generators’ size using supervised benchmark datasets.
- Conclusion: Mixing generation and verification probabilities for sample reranking performs better than directly applying rejection sampling to verifier outputs.The conclusion identifies probability mixing as the preferred reranking strategy.
- Conclusion: LEVER consistently improves code LLM performance across four language-to-code tasks and achieves new state-of-the-art results on all four.Further analysis identifies execution results as crucial for verification and reports generalization across different LLMs.
A. Additional Implementation Details
The experiments use dataset-specific verifier settings, temperature-sampled program candidates, and few-shot prompts. LEVER also evaluates transfer between code LLMs and provides verifier-input examples.
- Verifier training uses dataset-specific settings and statistics, including batch size, program samples per example, and sampled-program label percentages.
- Temperature sampling uses T = 0.6 for Codex and T = 0.8 for InCoder and CodeGen, selected for best pass@k according to the original papers.
- Few-shot exemplars are randomly sampled and ordered from training data, except MBPP, which uses its three original examples.
- Normalized probability is used for GSM8k and MBPP because Python programs have higher variance in length.
- Between-LLM transfer applies verifiers trained on one code LLM to programs sampled from another, improving baseline performance most of the time.
B.2. Ablation on Base LMs for Verification
The paper evaluates different verifier base models and reports their performance across datasets, with additional ablation results summarized in the accompanying tables and figure.
- Verifier base models are treated as a hyperparameter, and the paper reports results for all attempted models across four datasets.
- Figure 7 reports the effect of training-example count for Codex+LEVER on WTQ and GSM8k, using T5-base for LEVER.
B.3. Training Example Scaling for WTQ and GSM8k
LEVER remains data-efficient on WTQ and GSM8k, showing non-trivial gains with limited training data. The paper also reports official-evaluator results and case studies illustrating both successful verification and ambiguity.
- B.3. Training Example Scaling for WTQ and GSM8k: Non-trivial improvements are observed on WikiTQ and GSM8k even with only 250 training examples.
- B.4. WikiTQ Results with the Official Evaluator: LEVER achieves a state-of-the-art result on WikiTQ when evaluated with the official WikiTQ evaluator.
- B.5. Case Study: In the Spider case study, an execution error from selecting the wrong table receives a low verification probability.
- B.5. Case Study: In the WikiTQ case study, two county-name execution results provide insufficient information for the verifier to identify the incorrect program.
- The appendix includes verifier-input examples, case-study tables, and few-shot prompts for Spider, WTQ, GSM8k, and MBPP.