Source-linked AI summary
Toward Trustworthy Neural Program Synthesis
Darren Key, Wen-Ding Li, Kevin Ellis
TL;DR
Language-model code generators can produce plausible but buggy programs, making it difficult to know when to trust their outputs. Speculyzer samples candidate programs and behavioral specifications, then estimates correctness and identifies useful explanations. The authors report improved overall generation accuracy, and study participants preferred top-ranked specifications to raw language-model outputs.
Problem
Language-model code generators can produce plausible but buggy programs, while users may lack a way to detect failures or understand why generated code behaves as intended.
Source: Introduction · p. 1Method
Speculyzer independently samples candidate programs and behavioral specifications, checks them, and uses a learned classifier to predict correctness and identify useful explanatory specs.
Source: Introduction · p. 1Results
The authors report that their methods boost overall natural-language-to-code accuracy, and study participants preferred top-ranked specs over raw LLM specs (p < .05; Cohen’s d = 0.14).
Source: Introduction · p. 1, Specs as explanations for program… · p. 7Takeaways & Limitations
Well-calibrated correctness estimates support analysis of metrics connected to trust and safety.
Source: Introduction · p. 1Speculyzer inherits costly sampling from large language models, adds execution cost and sandboxing risks, and cannot match the trust of synthesis from human-crafted formal-logic specs.
Source: Contributions and Outlook · p. 7
Abstract
from arXiv · showhide
We develop an approach to estimate the probability that a program sampled from a large language model is correct. Given a natural language description of a programming problem, our method samples both candidate programs as well as candidate predicates specifying how the program should behave. This allows learning a model that forms a well-calibrated probabilistic prediction of program correctness. Our system also infers which predicates are useful to explain the behavior of the generated code, and humans preferred these in a human study over raw language model outputs. Our method is simple, easy to implement, and maintains state of the art generation accuracy results.
Introduction
Speculyzer addresses the trust gap in language-model code generation by estimating program correctness and surfacing behavioral specifications as explanations. It combines calibrated prediction with specification-based checks, and the authors report improved overall accuracy on natural-language-to-code tasks.
Introduction
- The authors report that speculyzer boosts overall accuracy on natural-language-to-code generation problems.They frame accuracy as a goal that might seem in tension with calibration and explainability.Source: Introduction · p. 1
Methods
- Speculyzer independently samples candidate programs and behavioral specifications, checks their agreement, and uses a learned model to estimate program correctness and rank solutions.Specifications include input-output tests and logical relations; returned specs can help users check intended behavior.Source: Introduction · p. 1, Methods · p. 2
Related Work
- Prior approaches include formal-specification synthesis and language-model reranking, while speculyzer centers trust on calibrated probabilities and symbolically checkable, human-comprehensible properties.The paper presents symbolic checking as complementary to statistical prediction.Source: Related Work · p. 2
Sampling programs and specs
- The system samples 100 candidate programs and candidate specs from a pretrained language model, using transformed prompts to generate specs.The spec types considered are input-output test cases and logical relations.Source: Introduction · p. 1, Sampling programs and specs · p. 2
Checking specs against programs
- Input-output specs can be checked directly, but logical relations are approximately validated by running them on language-model-generated candidate inputs.This fuzzing approach can overapproximate the relations a program satisfies; concrete test inputs are shown.Source: Checking specs against programs · p. 3
Scoring and analyzing test coverage
- A logistic regressor estimates correctness using spec pass rates, behavioral cluster size, feature ranks, and normalized program log probability.The features reflect both program-spec agreement and how many sampled programs exhibit the same behavior.Source: Scoring and analyzing test coverage · p. 3
Test time metrics
- A score threshold trades precision against recall: programs below it are discarded, and the system can decline to return an answer when all candidates fall below it.The paper defines precision and recall in terms of ranking correct programs when outputs are available.Source: Test time metrics · p. 4
Results
The results show that calibrated scoring can trade coverage for high precision, support human-preferred specification explanations, and maintain strong program-ranking accuracy. Classifier-guided model cascading also reduces large-model queries while retaining a similar number of solved problems.
Results
- Evaluation spans MBPP and HumanEval, which differ because HumanEval sometimes includes example input-output pairs while MBPP does not.The paper frames evaluation around calibration, spec explanations, and the effect of reranking on success rates.Source: Results · p. 5
Calibration, Precision, and Recall
- 100% precision on HumanEval drops recall from 93.4% to 44.4%; 90% precision yields 90.7% recall, and learned scores calibrate better than raw log-likelihood.Threshold τ lets users target a desired precision based on predicted correctness.Source: Calibration, Precision, and Recall · p. 5, Figure 3 · p. 5, Figure 4 · p. 6
- In the largest Davinci setting, the full method typically leads on precision-recall statistics; input-output-only and relation-only specs each outperform uniform random.The figure reports AUC, maximum F1, and recall at 90% precision.Source: Calibration, Precision, and Recall · pp. 5–6, Figure 3 · p. 5
- Cushman-to-Davinci cascading approximately halves large-model queries while maintaining a similar number of solved problems, including MBPP cases where the small model wins.The learned classifier supplies the routing signal.Source: A further application of calibration:… · p. 6, Figure 6 · p. 6, Figure 5 · p. 6
Specs as explanations for program behavior
- The selected spec must be true of the chosen program yet informative; ranking by selectivity favors specs satisfied by fewer programs.A spec that is true of every program is uninformative even if it holds for the selected program.Source: Specs as explanations for program… · p. 6
- Participants preferred the top-ranked specification over raw LLM specs and dispreferred bottom-ranked specifications versus raw LLM output (both p < .05, two-tailed t-test); overall effect size was modest (Cohen’s d = 0.14).Source: Specs as explanations for program… · p. 7
speculyzer for ranking programs
- 85.7% pass@1 on HumanEval and 70.5% pass@1 on MBPP exceed comparable published reranking results, and speculyzer can improve on CodeT.The paper reports that calibration does not sacrifice raw accuracy.Source: speculyzer for ranking programs · p. 7, Figure 8 · p. 7
Contributions and Outlook
- The wrapper inherits expensive LLM sampling; executing synthesized code adds cost and sandbox-dependent security risk, while trust remains below human-crafted formal specifications.Formal logic is less accessible than natural language.Source: Contributions and Outlook · p. 7
Experimental setup
The experiments use Codex samples and nested cross-validation, with the HumanEval and MBPP data and code planned for release.
Experimental setup
- Codex samples used temperature 0.8 and TopP 0.95, with zero-shot prompts for programs and input-output tests and few-shot prompts for logical relations.Generation settings also specified max-token limits and stop tokens for each sample type.Source: Experimental setup · p. 10
- The logistic regressor used the lbfgs solver and repeated 5-fold nested cross-validation with regularization hyperparameter C = 1.Source: Experimental setup · p. 10
- The authors use existing HumanEval and MBPP datasets and state that they will release samples and make the code public upon publication.Source: Experimental setup · p. 10
Dataset Statistics
The dataset statistics report the share of programs satisfying at least one test across input-output and logical-relation specifications on HumanEval and MBPP.
Dataset Statistics
- The reported dataset statistics use Davinci Codex samples generated with temperature 0.8 and topP=0.95.Source: Dataset Statistics · p. 10
- 84.02% of HumanEval programs satisfy at least one input-output test, compared with 88.73% for logical-relation tests.Source: Dataset Statistics · p. 10
- 82.49% of MBPP programs satisfy at least one input-output test, compared with 82.43% for logical-relation tests.Source: Dataset Statistics · p. 10
User Study
In an IRB-approved study, 22 users rated ranked specifications for sampled programs, preferring top-ranked specifications to random and bottom-ranked ones.
User Study
- The study recruited 22 users, primarily computer science students, who rated specifications for eight sampled programs on a 1–7 Likert scale.For each program, participants saw top-ranked, bottom-ranked, and random specifications and judged how well each communicated program correctness.Source: User Study · p. 10
- Participants preferred top-ranked specifications over random-ranked ones, and random-ranked ones over bottom-ranked specifications.Source: Figure 9 · p. 10
- Median ratings were around 5 for top-ranked specifications; the first quantile exceeded random specifications, and the third quantile reached 6, surpassing bottom-ranked specifications.Source: User Study · p. 10
Precision-Recall Curves
The precision-recall curves cover four settings and indicate that high precision can be achieved without substantially compromising recall.
Precision-Recall Curves
- Figure 11 presents four precision-recall curves, each corresponding to one of the four settings in Figure 3.Source: Precision-Recall Curves · p. 10
- The curves indicate that high precision can be achieved without substantially compromising recall across the conditions shown.Source: Precision-Recall Curves · p. 10
Generalization across datasets
The learned parameters generalize across MBPP and HumanEval: pass@1 and precision-recall statistics are similar when training and testing use different datasets. The authors interpret this as generalization across similar, but not identical, data distributions.
Generalization across datasets
- Pass@1 and precision-recall statistics are similar when models trained on MBPP are tested on HumanEval, and vice versa.The authors interpret this as generalization across similar, but not identical, data distributions.Source: Generalization across datasets · pp. 10–11
Example Zero-Shot Prompts for program
The appendix shows zero-shot prompt examples for HumanEval and MBPP, alongside figures about the survey, precision-recall curves, and cross-dataset generalization.
generation
- For MBPP, prompts were converted into function docstrings using the function name called by the ground-truth tests, while HumanEval prompts were used as is.The section introduces two examples of zero-shot prompts for program generation.Source: generation · p. 11
HumanEval
- A HumanEval example asks whether a string is happy, defining it as length at least three with every three consecutive letters distinct.The prompt gives example inputs and expected Boolean outputs.Source: HumanEval · p. 11
- A code example asks for a string’s spaces to be replaced with underscores and shows “_Example_2” alongside a call on “ Example 3” whose output is “_Example-3”.Source: HumanEval · p. 11
- Figure 10 is a screenshot of the survey.Source: Figure 10 · p. 11
MBPP
- An MBPP example pairs the function signature sum_range_list with a prompt to sum list numbers within a range specified by two indices.Source: MBPP · pp. 11, 13
- Figure 11 presents precision-recall curves for each model and dataset.Source: Figure 11 · p. 12
- Figure 12 concerns generalization when train and test data come from the same problem corpus versus different corpora.Source: Figure 12 · p. 13
- Another MBPP example pairs diff_even_odd with a prompt to find the difference between the first even and first odd number in a list.Source: MBPP · p. 13
Example Zero-Shot Prompts for input-output generation
The appendix describes how test cases were generated and presents example prompts for extracting input-output cases from HumanEval and MBPP problems.
input-output generation
- The authors generated 100 samples per HumanEval/MBPP prompt and extracted each distinct single-line test case to test programs on individual cases.Their stated reason is that each generation may contain multiple test cases.Source: Example Zero-Shot Prompts for… · p. 13
HumanEval
- A supplied example defines a happy string as length at least 3 with every three consecutive letters distinct, gives is_happy examples, and begins an assertion checking is_happy.Source: Example Zero-Shot Prompts for… · p. 13
MBPP
- MBPP examples include sum_range_list and diff_even_odd prompts, with assertion lines asking Codex to test the corresponding functions.Source: Example Zero-Shot Prompts for… · p. 13
Few-Shot Prompt for logical relations spec
The section shows how few-shot prompts can turn programming-task descriptions into executable predicates that test candidate behavior. Through two-shot and five-shot examples, it illustrates tests of output properties across tasks including filtering, vowel repetition, missing-number and kth-largest outputs, and substring reversal.
generation
- Two-shot and five-shot examples prompt the 2k-context Cushman and 8k-context Davinci models, respectively, to test different kinds of properties.The examples are used to guide property testing.Source: generation · p. 14
HumanEval (Cushman)
- For Cushman HumanEval, example predicates check that filtered output contains odd integers and that vowel counts double after `repeat_vowel`.The examples also run each test function on three input cases that satisfy the task description.Source: HumanEval (Cushman) · p. 14
HumanEval (Davinci)
- For Davinci HumanEval, example predicates check odd filtered output, doubled vowel counts, and that output integers come from the input list.The tests are run on three task-satisfying input cases.Source: HumanEval (Davinci) · p. 15
- Davinci HumanEval examples also specify checks for a missing number's type and range, a kth-largest result's membership in the input, and reversed substrings.For substring reversal, checks include output length and character preservation.Source: HumanEval (Davinci) · pp. 16–17
MBPP (Cushman)
- The MBPP Cushman example presents the filtered-even-integers task with a test function intended to check whether its implementation is correct.The task asks for a list with even integers filtered out.Source: MBPP (Cushman) · p. 17
- For filtered_even_integers, tests require odd outputs drawn from the input and run three satisfying input cases.Source: MBPP (Cushman) · p. 17
- For repeat_vowel, tests check that the output has twice the input’s vowel count and run three satisfying input cases.Source: MBPP (Cushman) · p. 18
MBPP (Davinci)
- For filtered_even_integers, tests require every output value to be odd and present in the input, then run three satisfying input cases.Source: MBPP (Davinci) · p. 18
- For repeat_vowel, tests check that the output has twice the input’s vowel count and run three satisfying input cases.Source: MBPP (Davinci) · p. 19
- For find_missing_number, tests require an integer output in the range 1 to n and run three satisfying input cases.Source: MBPP (Davinci) · p. 19
- For find_kth_largest, tests check that the output is an integer found in the input list and run three input cases.Source: MBPP (Davinci) · pp. 19–20
- For reverse_substrings, the provided test checks that characters outside the specified substrings remain the same and runs three input cases.Source: MBPP (Davinci) · p. 20
Transformation of input problems to logical
The transformation pipeline formats MBPP and HumanEval problems as input-output or logical-relation prompts. HumanEval prompts use parsed function information and dataset-specific templates, with few-shot examples prepended.
relations prompts
- MBPP has separate templates for logical-relation and input-output prompts.For logical relations, the resulting string is prefixed with a few-shot example; for input-output prompts, a blank-lines prefix is stripped when the import is empty.Source: Figure 13 · p. 20, Figure 14 · p. 21, relations prompts · p. 21
- HumanEval problems are parsed into a function definition, English description, and function name, then inserted into input-output or logical-relation templates.The resulting prompt is prepended with a few-shot example string.Source: relations prompts · p. 21
- HumanEval’s input-output and logical-relation prompts use distinct templates.The templates are identified as Figures 15 and 16, respectively.Source: Figure 15 · p. 21, Figure 16 · p. 21, relations prompts · p. 21
Examples of Top Spec versus Random Spec
The section presents eight HumanEval problems with programs generated by code-davinci-002, alongside top-ranked, random, and bottom-ranked specifications. Four examples use relation specifications and four use input/output specifications.
Examples of Top Spec versus Random Spec
- Eight HumanEval problems are paired with code-davinci-002 program samples and top-ranked, random, and bottom-ranked specifications.Four examples show relation specifications; the remaining four show input/output specifications.Source: Examples of Top Spec versus Random Spec · p. 21
- The cited figures present examples of top-ranked, random, and bottom-ranked specifications, with numbered examples identified for Programs 2, 3, 4, and 5 and one example set lacking a program number.Source: Figure 18 · p. 22, Figure 17 · p. 22, Figure 19 · p. 23
- Program 1 examples are labeled as random and bottom-ranked relation specifications, while Program 5 examples are labeled as top-ranked and random relation specifications.The labels identify the displayed examples without stating their comparative quality.Source: Examples of Top Spec versus Random Spec · pp. 22, 24
- Further examples present top-ranked, random, and bottom-ranked specifications for three programs: Program 6 in Figure 22, Program 7 in Figure 23, and Program 8 in Figure 24.Source: Figure 22 · p. 24, Figure 23 · p. 25, Figure 24 · p. 26