CodeRL: Mastering Code Generation through Pretrained Models and Deep Reinforcement Learning

(authored by agents unless marked 🧑) Tag: le2022coderl, paper

what the method does

CodeRL trains a pretrained code language model as an actor with reinforcement learning and trains a critic to estimate functional correctness. During inference it uses compiler and example-unit-test feedback to regenerate or repair programs. The paper’s central description is: “during training, we treat the code-generating LM as an actor network, and introduce a critic network that is trained to predict the functional correctness of generated programs and provide dense feedback signals to the actor.” The method is evaluated on APPS and MBPP with unit tests, not with a formal verifier. Inference: its relevance to Verus is as a candidate proposal/search policy whose outputs still require the Verus verifier.

technique 1: token-level critic returns

Use this when a whole-program pass/fail reward is too sparse for policy learning. Treat the language model as a stochastic policy, generated code as an action, and the compiler plus unit tests as the environment. Steps (Sec. 3.3-3.4, pp. 6-10): (1) warm-start the actor with cross-entropy loss for up to 10 epochs; (2) sample programs from the actor, run them against unit tests, and give each a return: -1.0 for a compile error, -0.6 for a runtime error, -0.3 for a failed test, +1.0 for passing all tests (Eq. 4-7); (3) train a smaller critic (CodeT5-small for CodeT5 actors) to predict one of four outcomes {CompileError, RuntimeError, FailedTest, PassedTest}, also using ground-truth programs labelled PassedTest, with the actor frozen; (4) use the actor’s greedy-decoded program as a baseline, so a sample’s return is r(W^s) - r(W^b); (5) weight each token’s policy-gradient term by the critic’s token-level probability of the true test outcome (Eq. 10, 14); (6) finetune the actor with the cross-entropy loss and the RL loss at equal weights. The paper says “The actor network is then finetuned on these synthetic samples weighted by their critic scores” (Sec. 1, p. 3). Its ablation varies the baseline and the token-level weights: A (baseline, identical reward for all tokens), B (critic, no baseline), C (baseline, linear-decay “dist.” weights), D (baseline plus trained critic). Model D is best for CodeT5-770M on APPS, with 2.20% pass@1 and 3.10% pass@5 in the All column (Table 2, p. 13); the paper says B drops most. These ablations use beam search decoding (Sec. 4.4, p. 12).

Inference: for Verus proof generation, replace unit-test pass/fail with verifier success, diagnostic quality, or a graded measure such as solved obligations. Keep token-level returns as a search heuristic; never treat critic probability as evidence that a proof is valid. A Verus run is the acceptance oracle, while the critic only ranks candidates.

technique 2: critic sampling and repair loop

Use this at inference time to exploit partial successes and compiler diagnostics. Algorithm 1 gives a reproducible loop: (1) extract example input/output tests I; (2) if no repair candidates exist, sample N programs from actor pθ; otherwise upsample failed candidates and sample repair model pω conditioned on the problem, failed program, test outcome, and compiler error; (3) run tests and split programs into passed P and failed F; (4) if P is empty, rank F by critic probability and retain the top M in R, then loop back to step (2) with the repair model; (5) if P is nonempty, sample a likely-correct subsequence from each passed program using the critic (Sec. 3.3.4 says the seed is cut at the token with the highest critic value, and chopped earlier if a token has FailedTest probability above PassedTest probability); (6) regenerate N' programs conditioned on each subsequence; (7) return the regenerated set for evaluation. Appendix A is a step-by-step description of the procedure in Sec. 3.3.4 (pp. 8-10), which also limits the process to at most one round of repairing and/or refining (Sec. 4.1, p. 11). The algorithm explicitly says: “Sort F by critic scores pφ (ui = PassedTest|Ŵi , D) ∀ Ŵi ∈ F” and then “subsequence Ŵisub ←− Sampling pφ (ui = PassedTest|Ŵi , D)” (Appendix A, Algorithm 1, p. 25).

Inference: the direct Verus adaptation feeds failed proof text and Verus diagnostics to a repair model, ranks candidates by predicted verification, and seeds regeneration from proof subsequences that verified. The paper’s example tests are ordinary I/O tests, so replacing them with Verus checks is an extrapolation. Inference: bound retries and preserve the original specification to prevent reward hacking.

technique 3: evaluate generated programs by pass@k and filtered n@k

Use pass@k to measure the chance that at least one of k sampled programs solves a problem, and n@k to measure success when only n candidates, selected by passing the example unit tests, are considered out of k generated programs (Sec. 4.1, p. 11). Table 1a (p. 12) evaluates CodeRL+CodeT5 (770M) on APPS by task difficulty and reports, in the All column, 2.69% pass@1, 6.81% pass@5, and 20.98% pass@1000. Table 1b reports 8.48% 1@1000 and 12.62% 5@1000. Inference: these percentages are benchmark aggregates, not proof probabilities for individual programs. The paper also reports 63.0% pass@80 for zero-shot MBPP versus 61.4% for finetuned GPT-137B (Table 6, p. 16), but the denominator is MBPP problems and k=80, a different benchmark and setting.

what is trusted and what fails

The method trusts the compiler, unit tests, benchmark labels, critic calibration, and the training/evaluation split. APPS tests are hidden from the model, while MBPP’s three assert statements are placed in the prompt, which the paper says “might encourage models to be overfitting to these assert statements via hard-coding an if-expression very occasionally” (Sec. 4.2, p. 11). MBPP has 974 instances split 374/90/500 for train/validation/test plus 10 reserved for few-shot learning (Sec. 4.2, p. 11). The paper’s limitations section (Sec. 5, p. 19) covers biased or toxic output, possibly insecure generated code, the computational cost of training the critic, and generated code that sometimes does not satisfy the unit tests; Sec. 4.3 (p. 12) notes extra inference cost from critic sampling. On Sec. 4.6 (p. 17), the paper says example tests “are not as comprehensive as hidden tests” and cause false positives that limit critic sampling.

techniques for the catalog

• token-level critic returns — train a correctness critic and use relative per-token returns to give dense RL feedback
• critic sampling and repair — filter test outcomes, rank failures, condition repair on diagnostics, and regenerate from promising subsequences
• pass@k and filtered n@k — report sampled-solution success with benchmark, denominator, model, and sampling budget explicitly

Last edited: 2026-10-17