arXiv CSopen access

SCOPE: Leveraging Subgoal Critiques for Code Generation

SCOPE: Leveraging Subgoal Critiques for Code Generation Yueke Zhang∗ , Yifan Zhang∗ , Zihan Fang∗ , Kevin Leach∗ , Juan Zhai† , Wei Zhang‡ , Yu Huang∗ ∗ Vanderbilt University

arXiv:2607.05810v1 [cs.SE] 7 Jul 2026

{yueke.zhang, yifan.zhang.2, zihan.fang, kevin.leach, yu.huang}@vanderbilt.edu † University of Massachusetts at Amherst [email protected] ‡ IBM [email protected]

Abstract—Code generation with large language models (LLMs) remains unreliable because generated programs can appear correct while still violating key semantic requirements in the naturallanguage specification. Existing feedback-based methods improve over coder-only generation, but they often rely on unstructured critique or execution signals that do not explicitly identify what the code is semantically missing. We present SCOPE, a proverinitialized subgoal critic for code generation. SCOPE adapts a Lean-oriented prover model to produce three parseable feedback fields for downstream code generation: subgoals, gap analysis, and a robustness checklist. Our approach combines supervised fine-tuning, process-aligned reinforcement learning (RL), and feedback-guided inference, with two complementary rewards during RL: a dense reward for structured critique quality and a sparse reward based on whether the critique improves the coder’s execution score. Experiments show that SCOPE improves over the compared feedback baselines. On LiveCodeBench V6, SCOPE achieves 39.4% pass@1, compared with 36.6% for Reflexion and 20.6% for the coder-only baseline. On BigCodeBench (Hard), it reaches 42.6%, surpassing Reflexion at 36.5% and coder-only generation at 34.5%. Further analysis shows that SCOPE’s gains are concentrated in tasks with concrete semantic constraints and that its localized code corrections than Reflexion’s. Index Terms—LLM for Coding, Code Generation

I. I NTRODUCTION Large Language Models (LLMs) for coding are now mainstream [1], [2]. AI coding assistants have moved from early trials to routine practice across industry and open source: enterprises report broad adoption and measurable productivity gains [3], [4]. Recent data highlights rapid growth in AIassisted development, while field studies with large organizations document sustained usage and positive developer experience impacts [5]. However, reliability remains the central obstacle for LLMbased code generation [6]. Code LLMs often produce programs that look plausible but violate the user’s actual intent: they may hallucinate APIs, invent unsupported behaviors, or implement logic that passes superficial checks while failing on edge cases [7], [8]. Testing helps, but it does not fully solve the problem [9]. In realistic software settings, developers cannot enumerate tests for every path, corner case, and semantic constraint, and recent studies show that LLM-generated tests are themselves incomplete, sometimes invalid, and often weak

at exposing real defects [10], [11]. Thus, passing a limited test suite is useful evidence, but it is not the same as showing that the generated code actually satisfies the intended behavior [12].

Fig. 1. A natural-language task usually contains latent semantic requirements that are difficult to recover from execution feedback alone. SCOPE fills this gap by asking a prover-initialized critic to expose those requirements as explicit repair obligations before the coder revises the program.

A natural response to unreliable code generation is verification, but this is precisely where the difficulty deepens [13]. Existing approaches based on contracts, symbolic reasoning, and SMT solvers can verify well-specified properties, yet they rely on precise formal statements of behavior that are rarely available in open-ended natural-language programming tasks [14], [15]. Recent work at the intersection of LLMs and formal methods is encouraging: models can generate and repair proofs in interactive theorem provers and produce verifier hints for formally checked programs [13], [16]. However, these successes largely assume that the task is already formalized, that the target language is verifier-native, or that rich proof state feedback is available during search. When these assumptions are relaxed, end-to-end verified code generation remains difficult even for the most advanced LLMs [16], [17]. Thus, the main bottleneck is not only discharging formal obligations, but first deriving useful obligations from ambiguous natural-language intent. This leaves a gap between weak evidence from testing and the high cost of full manual

formalization. Recent progress in formal mathematics suggests a promising direction for narrowing this gap [18], [19]. Proof assistants such as Lean provide a reasoning environment in which intermediate steps are explicit, modular, and machine-checkable under a small trusted kernel [20], [20]. Moreover, the Lean ecosystem has matured substantially, with infrastructure such as LeanDojo exposing proof states, premises, and benchmarks to learning-based systems [21], [22]. At the same time, Leanoriented LLMs have shown that models can make progress by decomposing difficult problems into intermediate subgoals rather than relying on unconstrained text generation alone [23], [24]. These developments suggest a more limited and practical use of prover-trained models for code generation. Rather than treating Lean as a runtime verifier for Python, we ask whether the decomposition behavior learned by Lean-oriented prover models can be repurposed as structured semantic feedback for code repair [25]. Motivated by this idea, we propose SCOPE, a proverinitialized subgoal critic for code generation. As illustrated in Figure 1, SCOPE is designed to fill the gap between ambiguous natural-language intent and actionable repair signals. Given a task and a draft program, the critic emits three structured fields: subgoals that state what the solution should satisfy, gap analysis that compares the draft against those subgoals, and a robustness checklist that highlights boundary conditions. The output is natural language, not a machine-checked Lean proof, but it is constrained enough to be parsed and fed back to the coder. SCOPE therefore provides a practical middle ground between weak test-only feedback and expensive end-to-end formal verification. Concretely, our approach has three stages: (1) supervised fine-tuning to adapt a Lean-oriented prover model to the critic interface, (2) process-aligned reinforcement learning with dense semantic rewards and sparse execution rewards, and (3) feedback-based inference, where the critic’s structured output guides iterative code revision. We summarize the contributions of this paper as follows: 1) We present SCOPE, a prover-initialized LLM as a subgoal critic in two model code generation framework. 2) We design a process-aligned reward framework for training the critic in coding tasks. It combines a dense reward for producing structured, semantically useful critiques and a sparse reward based on whether the critique ultimately helps the coder generate a correct program under execution based evaluation. 3) We show that SCOPE achieves stronger performance than competitive self-refinement baselines. On LiveCodeBench V6, SCOPE reaches 39.4% pass@1, outperforming Reflexion at 36.6%, Self-Refine at 33.1%. On BigCodeBench, SCOPE achieves 42.6% pass@1, again surpassing Reflexion 36.5%. 4) We provide evidence for why SCOPE works better. Our analysis shows that, SCOPE rescues more failed solutions than Reflexion (19 vs. 16), achieves better bugtriggered localization (42.1% vs. 31.3% localized wins

within 20 lines), and does so with more surgical repairs (28.0 vs. 35.0 median changed lines). The remainder of this paper is organized as follows. Section II introduces the background. Section III presents a motivating example. Section IV reviews related work. Section V describes the SCOPE methodology. Section VI presents the evaluation protocol. Section VII reports the empirical results and explains where SCOPE helps most and why. Section VIII discusses implications and limitations. Finally, Section IX concludes the paper. II. BACKGROUND : W HY P ROVER -S TYLE D ECOMPOSITION F ITS C ODE G ENERATION Lean is an interactive theorem prover in which reasoning is expressed as a sequence of machine-checkable proof states. As illustrated in Figure 2A, a proof starts from a goal together with local hypotheses, and tactics transform that state by reducing one difficult goal into several smaller subgoals. A proof is complete only when all subgoals are discharged. For SCOPE, this view is an analogy and a source of model prior, not a runtime verification procedure. Each emitted subgoal is a natural-language semantic obligation, such as a precondition, an invariant, an output constraint, or an edge case requirement. The useful property for code generation is not formal certification, but disciplined decomposition. In Lean, reasoning does not proceed as unconstrained text generation. At each step, the prover operates on an explicit proof state: a typed goal together with local hypotheses. This state rules out many irrelevant directions, and tactics further narrow the search by transforming one hard goal into a small number of concrete subgoals. SCOPE borrows this decomposition pattern for feedback: the critic should not rewrite the program or produce a long reflection, but should identify a compact set of obligations that a coder can inspect and repair. This is exactly the kind of structure that natural-language-tocode generation lacks. A programming prompt usually bundles together several requirements, such as functional behavior, boundary conditions, interface constraints, and hidden invariants, but standard code generation leaves these requirements implicit. As a result, a code model may produce a plausible program while missing one thin semantic condition that later causes failure. SCOPE uses a prover-initialized critic as an intermediate layer because it can turn mixed natural-language intent into explicit repair obligations. Once these obligations are exposed, the search problem becomes smaller and better organized: instead of searching broadly for any revision that might pass tests, the system can focus on edits that address a specific violated condition. DeepSeek-Prover-V2 is especially well matched to this role because it is already trained to reason through recursive subgoal decomposition rather than free-form explanation [23]. SCOPE uses this model in a limited way. We do not ask it to synthesize Python, call Lean, or certify the entire program end to end. We prompt and post-train it to recover a semantic view of the task, identify which obligations the current draft appears to violate, and return those failures as structured

Fig. 2. Illustration of the subgoal-decomposition prior that motivates SCOPE. (A) In Lean, tactics transform one formal goal into smaller subgoals that must all be discharged. (B) DeepSeek-Prover-V2 is trained for Lean proof construction and inherits this bias toward decomposing a problem into intermediate obligations. SCOPE does not run this proof search on Python code; it reuses the model as a critic that emits natural-language obligations for repair.

Fig. 3. The figure contrasts Reflexion’s broad natural-language reasoning with SCOPE’s subgoal-guided analysis, which exposes the missing invariant and maps failure to a precise local fix.

feedback. In this sense, the prover model acts as a semantic search controller: it makes intent explicit, prunes semantically irrelevant revisions early, and converts vague failures into localized repair targets. III. M OTIVATION E XAMPLE Figure 3 shows a real example from LiveCodeBench. The task is: count distinct 3-digit even numbers formed from a multiset of digits, allowing reuse only when multiple copies exist. The prompt contains several constraints at once: the number must be 3-digit, the first digit cannot be zero, the last digit must be even, each digit can be used only as often as it appears in the input, and duplicate valid numbers should be counted once. Both R EFLEXION [26] and our approach are feedback-based code generation methods: they improve an initial draft by feeding critique generated by feedback LLM back to the coder for revision. The key difference is that R EFLEXION relies mainly on natural-language feedback from test traces, whereas SCOPE asks a prover-initialized critic to produce structured semantic feedback that makes missing obligations and likely failure points more explicit. The left side of Figure 3 illustrates this failure mode with a Reflexion setup. The coder is Qwen3-Coder-30B, and the feedback model is Qwen3-8B. The Reflexion fails because the coder generates plausible counting logic but misses one hidden semantic constraint: it allows a leading zero, so an invalid

number such as 022 is counted as valid. Given the failing case [0, 2, 2] → 2, the system knows only that the current output is wrong. It generates a long natural-language critique, but the feedback does not isolate the violated constraint. As a result, the search remains broad: the model can revise many parts of the program without directly addressing the real issue, namely that a number with a leading zero is being treated as valid. The right side of Figure 3 shows how SCOPE changes this process. We keep the same coder, but replace free-form feedback with a structured critic initialized from DeepSeekProver-V2-7B. Instead of producing broad discussion, the critic decomposes the prompt into explicit obligations and identifies that the validity condition is violated. This turns the error into a local repair problem: the revision only needs to enforce that the first digit is non-zero. The resulting fix is small, targeted, and semantically grounded. This example captures the main motivation for SCOPE. The advantage comes from using structured semantic feedback emitted by the critic. By converting informal intent into explicit obligations, SCOPE narrows the repair space and makes code revision more precise. IV. R ELATED W ORK This section reviews prior work most relevant to our approach, including LLM-based code generation, feedback-

Fig. 4. SCOPE couples a coder with a prover-initialized critic that receives the problem and draft code, then emits structured subgoals, gap analysis, and robustness checks. During training, the critic is aligned with dense semantic rewards and sparse execution-based rewards. During inference, its critique guides iterative revision by the coder.

driven refinement, and formal reasoning for program repair and verification. A. LLMs for Code Generation and Hallucination Code LLMs have rapidly advanced natural-language-tocode generation. Open models, including C ODE L LAMA and S TAR C ODER, further improved support for multi-language generation and deployment in developer-facing tools [27], [28]. A growing body of work shows that the remaining reliability gap is a hallucination problem. Recent studies develop taxonomies of code hallucinations and show that these errors include invented APIs, incorrect package names, resource assumptions, mapping mistakes, and faulty program logic [29], [30], [6]. These failures are obvious from surface form alone: a generated program can look polished while violating hidden constraints or relying on nonexistent dependencies. Package hallucinations make this risk even more concrete by turning generation errors into potential software-supply-chain exposure [31]. Several mitigation strategies have therefore been proposed. For example, D E -H ALLUCINATOR grounds generation with iteratively retrieved project-specific API context to reduce repository-level API hallucinations [32]. However, most existing approaches still ground code using retrieved context, execution feedback, or post-hoc detection, rather than explicitly representing the semantic obligations implied by the original natural-language task. B. Feedback-Based LLM Code Generation Systems Feedback-based code generation systems improve on singleshot decoding by inserting an iterative critique, verification, or repair loop around a base model. A first line of work studies self-feedback: S ELF -R EFINE shows that the same LLM

can generate feedback on its own output and then repeatedly revise it, while R EFLEXION extends this idea with verbal reinforcement and episodic memory across attempts [33], [26]. In the coding setting, S ELF -D EBUG further demonstrates that execution results and natural-language explanations can help a model inspect and repair its own programs rather than merely resample candidates [34]. These methods establish an important point: even without changing model weights, test-time feedback can substantially improve code generation quality [35], [36]. A second line of work makes the feedback signal more explicit or more structured. C ODE RL introduces a critic trained to estimate functional correctness from unit-test outcomes, bringing feedback into the training loop rather than relying only on post-hoc prompting [37]. More recent frameworks such as T EXT G RAD cast natural-language critique as a gradient-like optimization signal over compound LLM systems [38], while R EPAIR AGENT frames repair as an autonomous agentic loop that alternates among fault localization, patch generation, and validation [39]. C. Lean, Formal Proof, and LLM-Based Provers Lean is a modern interactive theorem prover with a small trusted kernel and dependent type theory, making proofs explicit and machine-checkable [20]. Recent infrastructure such as L EAN D OJO has made Lean more accessible to learning-based systems by exposing proof states, premises, and benchmarks, which helped turn formal proving into a more standard LLM setting [21]. Building on this ecosystem, specialized provers such as D EEP S EEK -P ROVER and D EEP S EEK P ROVER -V2 show that LLMs can learn premise use, proof search, and especially subgoal decomposition in Lean, rather than relying only on free-form reasoning [40], [23].

A related line studies LLMs for formal proof and verified programming more directly. BALDUR explores whole-proof generation and repair with LLMs, while benchmarks such as DAFNY B ENCH and CLEVER show both the promise and the difficulty of generating machine-checked proofs or verified programs from natural-language tasks [13], [16], [17]. However, most of this work assumes a verifier-native target language, a pre-existing formal specification, or direct proofstate feedback. V. M ETHODOLOGY Figure 4 summarizes our methodology. SCOPE has two runtime models: a frozen coder and a critic initialized from DeepSeek-Prover-V2-7B. The critic receives the naturallanguage problem and the coder’s draft program. The methodology consists of three stages: data construction, where we build critique traces with a tutor LLM for code generation; supervised fine-tuning, where we warm-start the critic to emit the exact tag format consumed by the coder; and processaligned reinforcement learning, where dense semantic rewards and sparse execution rewards further optimize the critic to produce feedback that helps the coder generate correct code. A. Data Construction We construct training data by replaying the same critiqueguided revision process used by SCOPE at inference. To avoid overfitting to our main evaluation benchmark, we build the training set from LiveCodeBench V1–V3. Each task provides a natural-language problem statement, optional starter code, and test cases. For each task, a coder first generates an initial draft p0 . A tutor critic then analyzes the draft and produces a structured critique y, including subgoals, gap analysis, and a checklist. Conditioned on this critique, the coder produces a revised program p1 . This yields a process-level training tuple (x, p0 , y, p1 ), where x is the original problem. In our pipeline, we use Qwen3-Coder-30B as the coder and DeepSeek-V3 to generate critique traces. We store the task, draft, revision, and normalized critique fields for each example. We next use these critique-guided traces to warmstart the critic with supervised fine-tuning, which provides a smoother transition from data construction to the downstream RL stage. Across LiveCodeBench V1 to V3, this procedure yields 528 critique-guided training tuples. Each tuple contains the original task, the initial draft, the structured critique, and the revised program. The reference critiques are teachergenerated and therefore are not treated as ground truth proofs; they provide dense format and content supervision, while downstream execution reward later checks whether a critique actually helps repair. B. Supervised Fine-Tuning of the Prover Critic We first warm-start the critic with supervised fine-tuning (SFT) so that it learns the subgoal decomposition interface in

the code generation task. Given a problem description x and an initial draft program p0 , the critic is trained to generate a structured critique y = (s, g, c), (1) where s denotes the subgoals, g the gap analysis, and c the robustness checklist. The target here is a compact semantic decomposition of the draft that can guide later repair. We initialize from DeepSeek-Prover-V2-7B and fine-tune it on the critique traces constructed in Section V-A. These targets are refined by a tutor model so that the supervision is consistent in both structure and quality. As a result, SFT serves primarily as a role-alignment stage: it teaches the model to act as a semantic critic in the code generation task instead of mathematical proving. The supervised completion is the exact format used in the implementation: <subgoal> s </subgoal> <gap_analysis> g </gap_analysis> <checklist> c </checklist>.

Formally, for each training example (x, p0 , y ⋆ ), where y ⋆ = (s⋆ , g ⋆ , c⋆ ),

(2)

we optimize the standard conditional language-model objective |y ⋆ | X ⋆ LSFT (θ) = − log pθ (yt⋆ | x, p0 , y<t ). (3) t=1

In implementation, the prompt tokens corresponding to (x, p0 ) are masked out, so the loss is applied only to the completion tokens of the structured critique. Intuitively, SFT teaches the model what kind of critique to produce, while the later RL stage teaches it which critiques actually help the coder. In this sense, SFT provides the structural prior that makes process-aligned reinforcement learning feasible. C. Process-Aligned Reinforcement Learning with Dense and Sparse Rewards SFT alone does not guarantee that a critique is useful for downstream repair. A critic may produce well-formed subgoals and fluent gap analysis that look reasonable to a human reader, yet still fail to help the coder generate a correct program. We therefore further optimize the critic with Group Relative Policy Optimization (GRPO), using a reward that combines dense semantic guidance with sparse execution-based feedback. For a task x and draft program p0 , the critic policy πθ samples a structured critique y. This critique is then fed to the coder, which produces a revised program p(y). The revised program is executed on benchmark tests, and the critic is rewarded according to whether its critique actually improves downstream correctness. This makes the RL signal processaligned: The critic is rewarded not for writing code, but for producing feedback that helps another model repair code. We optimize the policy with GRPO: max Ey∼πθ (·|x,p0 ) [R(y)]−β KL(πθ (· | x, p0 ) ∥ πref (· | x, p0 )) , θ (4)

where πref is the reference policy initialized from SFT, and β controls the strength of KL regularization. a) Dense reward.: The dense reward encourages the generated critique to remain structurally valid, semantically aligned, and practically readable. We define Rdense (y) = λemb Remb (y) + λqual Rqual (y).

D. Inference: SCOPE as a Critique-Guided Revision Loop At inference time, SCOPE instantiates a two-model revision loop between a coder and a post-trained critic. Given a task x, the coder first produces an initial draft program p0 . The critic then receives (x, p0 ) and returns a structured critique

(5)

y = (s, g, c),

(9)

The first term, Remb , measures semantic alignment between the generated critique and the teacher-generated targets in the training trace. Concretely, it scores the generated subgoals, gap analysis, and checklist against their target counterparts:

where s, g, and c denote the subgoals, gap analysis, and robustness checklist, respectively. Conditioned on this critique, the coder produces a revised program

Remb (y) = αs sim(s, s⋆ )+αg sim(g, g ⋆ )+αc sim(c, c⋆ ), (6)

p1 = C(x, p0 , y),

where sim() denotes an embedding-based similarity function and αs + αg + αc = 1. The second term, Rqual , scores critique quality. Its role is to reward outputs that are concise, grounded in the current draft, parseable by the revision prompt, and structurally useful for repair. In our main setting, this signal is provided by a frozen GPT-5.2 judge, which evaluates whether the critique is actionable rather than merely fluent. The semantic similarity alone is not enough: a critique can overlap with the target text yet still be vague or unhelpful. b) Sparse reward.: The sparse reward captures the actual downstream value of the critique from testing. After sampling y, we invoke the coder to revise p0 into p(y), then run the revised program on benchmark tests. Let S(·) denote the shaped execution score, which reflects not only binary pass/fail but also partial test progress and lightweight penalties for runtime failures. We then define the sparse reward as

where C(·) denotes the frozen coder. In this way, inference mirrors the same critic-guided repair process used during training, ensuring that the critic is deployed in exactly the role for which it was optimized. The subgoals define what the program must satisfy, the gap analysis explains where the current draft violates those obligations, and the checklist highlights boundary conditions that are easy to miss during revision. By packaging these three components into a single output, SCOPE gives the coder a unified repair target rather than a set of loosely related suggestions. Formally, the inference objective is not to search directly over programs, but to improve the draft through critic-guided revision. If S(·) denotes the hidden execution-based correctness signal, SCOPE aims to produce critiques such that

Rsparse (y) = S(p(y)) − S(p0 ).

(7)

It rewards the critic only for improvement over the original draft. As a result, the critic is encouraged to generate critiques that expose the draft’s missing semantic obligations and help the coder make targeted repairs. c) Final reward.: Our final reward combines the dense and sparse terms: R(y) = wdense Rdense (y) + wsparse Rsparse (y),

(8)

This combination reflects the two goals of SCOPE. The dense term keeps the critic anchored to the intended semantic structure and prevents drift into unstructured free-form text. The sparse term ensures that the critic is ultimately optimized for what matters most: whether its feedback helps the coder produce a correct program under execution-based evaluation. A useful way to interpret the two terms is as follows. The dense reward teaches the critic to produce well-formed critiques; the sparse reward teaches it to produce useful critiques. SCOPE needs both. Without the dense term, optimization becomes unstable and the model may exploit noisy execution signals. Without the sparse term, the critic may learn to imitate well-formed obligations that are linguistically plausible but do not improve code generation in practice.

S(p1 ) > S(p0 ),

(10)

(11)

and, more generally, such that the revised program moves closer to satisfying the problem’s latent semantic constraints. This formulation reflects the central intuition of our method: the critic adds value not by replacing the coder, but by exposing the obligations that the current draft has not yet made explicit. VI. E VALUATION We organize the evaluation around three questions: RQ1: Does SCOPE improve end-to-end code generation accuracy over coder-only and iterative baselines? RQ2: Where are these gains concentrated: are they consistent across benchmarks, or do they appear mainly in particular difficulty levels and problem categories? RQ3: When SCOPE improves a failed baseline solution, does it do so through more precise repair behavior, such as localized edits or specific types of semantic corrections? A. Baselines a) Coder-Only: This is the coder-only baseline.Qwen3Coder-30B receives the problem description and function signature, generates a single solution, and that solution is evaluated directly. There is no critic model and no refinement step.

b) Self-Refine [33]: This baseline keeps Qwen3-Coder30B as the coder and uses Qwen3-8B to generate a lightweight natural language critique of the draft. The feedback points out weaknesses in the current solution and suggests possible improvements in text, after which the coder revises the solution once based on that critique. This baseline tests whether generic textual self feedback is sufficient for code repair. c) Reflexion [26]: This baseline also uses Qwen3Coder-30B as the coder and Qwen3-8B as the feedback model. Unlike Self-Refine, the critic additionally observes execution feedback, such as failing inputs, expected outputs, and runtime errors. It then produces natural language debugging feedback, which the coder uses for iterative revision. This setting represents a strong execution guided interactive baseline. d) SCOPE (Untrained): This variant uses Qwen3Coder-30B as the coder and a raw DeepSeek-Prover-V27B model as the critic. The critic is prompted to produce structured subgoals, gap analysis, and a checklist, but it is used without SFT or RL. This comparison isolates the value of the prover-initialized critic before adaptation. e) SCOPE (SFT): This variant keeps the same coder, Qwen3-Coder-30B, and replaces the critic with an SFTadapted DeepSeek-Prover-V2-7B. The goal of this comparison is to measure how much role alignment alone helps, before reinforcement learning is introduced. f) SCOPE (Full).: Our full system again uses Qwen3Coder-30B as the coder, but the critic is the fully posttrained DeepSeek-Prover-V2-7B after both SFT and GRPO. The critic outputs structured semantic feedback in the form of subgoals, gap analysis, and a robustness checklist, which the coder uses for revision. B. Benchmarks, Metrics, and Analysis Protocol a) Benchmarks.: We evaluate primarily on Python code generation with LiveCodeBench V6, using the official execution harness. This subset contains 175 tasks, each defined by a natural-language problem description together with a Python function signature. Our setting is a controlled same-coder repair comparison. To test whether the method generalizes beyond the benchmark used most heavily during development, we also evaluate on BigCodeBench-Complete (Hard), which contains 148 Python tasks. b) Primary metric.: Our main metric is pass@1, defined as the fraction of tasks for which a method produces a final submission that passes all hidden tests. For the coderonly baseline, pass@1 is computed from its single generated solution. c) Pairwise comparison and failure modes.: Beyond overall pass@1, we compare SCOPE against each baseline on a per-task basis. For each pair, we count wins, where SCOPE solves a task that the baseline fails, and regressions, where the baseline solves a task that SCOPE fails. This analysis shows whether SCOPE’s gains come from broad improvements across many tasks or only from a small number of isolated cases. For unsolved tasks, we also group failures

into four categories: crash-like failures, which include nonAssertionError runtime failures; assertion-only failures, where the program runs but does not satisfy the hidden tests; mixed failures, where multiple failure types appear across attempts. This lets us examine not only whether SCOPE improves final accuracy, but also whether it changes the kinds of errors the system tends to make. d) Difficulty and category breakdown.: To understand where the method helps most on LiveCodeBench, we join each task’s official difficulty label with the corresponding binary pass/fail outcome and aggregate solved counts by difficulty level. We report results for Easy, Medium, and Hard tasks separately. We also analyze performance by algorithmic category, following the benchmark’s LeetCode style taxonomy, such as array, string, hash table, math, greedy, dynamic programming, graph, tree, binary search, and simulation. This breakdown helps show whether the gains are broadly distributed or concentrated in particular classes of problems. e) Repair localization and revision analysis.: We also study where successful repairs occur and what kinds of revisions they make. For tasks where a coder-only approach fails but a target method succeeds, we perform a manual fault-localization check on the failing coder-only solution. Concretely, we inspect the failing program together with its execution feedback, including traceback information, assertion messages, and failing input & output behavior, and then mark the line, or smallest contiguous region, most directly responsible for the failure. We refer to the center of this marked region as the trigger line, denoted by ℓtrigger . We then compare the failing coder-only solution against the final successful solution and identify the main edited hunk; the center of that hunk is treated as the fix line, denoted by ℓfix . We summarize localization quality by the absolute line distance d = |ℓfix − ℓtrigger | .

(12)

Smaller d indicates that the successful repair stays closer to the inferred fault location. To quantify edit magnitude, we compute the changed-line count between the failing solution and the final successful solution. Let Lbase and Lfinal be the sets of non-empty lines in the two versions after line based alignment. This yields a directly comparable trigger–fix view across methods under the same failure pool. Under this protocol, we report several complementary repair metrics. N Wins is the number of tasks where the coder-only solution fails but the target method succeeds. Recovery Rate normalizes this count by the size of the coder-only non-pass pool. Localized Wins @20 is the fraction of all recovered tasks whose fix lies within 20 lines of the trigger, that is, |ℓfix − ℓtrigger | ≤ 20. Trigger+Fix Coverage is the fraction of recovered tasks for which localization can be evaluated under our protocol. A task is counted as covered only when we can identify both (1) a trigger line in the coder-only failing solution from its failure signal, and (2) a dominant fix line in the target successful solution from the main diff hunk. Localized Share Among Covered is the fraction of these covered tasks whose fix lies within 20 lines of the trigger. This metric conditions on

TABLE I PASS @1 BY D IFFICULTY ON L IVE C ODE B ENCH V6 ACROSS SIX APPROACHES . B EST PER ROW IN BOLD .

Difficulty

Coder-Only

Reflexion

Self-Refine

SCOPE (Untrained)

SCOPE (SFT)

SCOPE (Full)

Easy Medium Hard

26/43 (60.5%) 8/52 (15.4%) 2/80 ( 2.5%)

39/43 (90.7%) 16/52 (30.8%) 9/80 (11.2%)

39/43 (90.7%) 16/52 (30.8%) 3/80 ( 3.8%)

41/43 (95.3%) 17/52 (32.7%) 6/80 ( 7.5%)

41/43 (95.3%) 16/52 (30.8%) 5/80 ( 6.2%)

42/43 (97.7%) 18/52 (34.6%) 9/80 (11.2%)

Overall

36/175 (20.6%)

64/175 (36.6%)

58/175 (33.1%)

64/175 (36.6%)

62/175 (35.4%)

69/175 (39.4%)

the subset where a trigger-to-fix comparison is actually well defined. Median Changed Lines is the median line-diff size between the coder-only solution and the target final solution. Median Changed Ratio further normalizes edit size by the length of the coder-only program. Higher is better for recovery and localization metrics, while lower is better for edit-size metrics. C. Training settings We train the critic in two stages: a supervised warmstart followed by GRPO-based reinforcement learning. All training is conducted on 2× NVIDIA RTX A6000 GPUs using parameter-efficient fine-tuning. For both stages, we adopt QLoRA with rank r = 16, α = 32, dropout 0.05, alllinear target modules, and 4-bit NF4 quantization. In the SFT stage, we fine-tune DeepSeek-Prover-V2-7B with optimizer AdamW, gradient accumulation 8, learning rate 1 × 10−4 , warmup ratio 0.03, and 80 training steps. We then initialize GRPO from the SFT checkpoint and continue training with the same backbone and LoRA setting for 120 maximum steps. The RL training mixture keeps broad regenerated LiveCodeBench V1–V3 data and upweights focused hard-fail slices used for curriculum. We therefore interpret the LiveCodeBench V6 result as an in-family repair evaluation and use BigCodeBench as the cleaner cross-benchmark generalization check. VII. R ESULTS We organize the results from overall effectiveness to deeper analysis: we first compare SCOPE against baselines on benchmark performance, then study behavior across difficulty levels and problem categories, and finally examine where the gains come from through a fine-grained error analysis. A. RQ1: Does SCOPE Improve Overall Code Generation Accuracy Across Benchmarks? In table I, the comparison isolates the effect of the feedback mechanism: no feedback for the Coder-Only, unconstrained self-critique for Self-Refine, execution trace guided natural language feedback for Reflexion, and prover-initialized subgoal feedback for SCOPE. Under this setup, SCOPE (Full) is the best-performing system overall. On LiveCodeBench V6, SCOPE (Full) solves 69/175 tasks, achieving 39.4% pass@1, compared with 64/175 (36.6%) for Reflexion, 58/175 (33.1%) for Self-Refine, 64/175 (36.6%) for SCOPE (Untrained), 62/175 (35.4%) for SCOPE (SFT), and 36/175 (20.6%) for the coder-only baseline. Relative to the strongest baseline, Reflexion, SCOPE improves by 5 additional solved tasks

and +2.8 absolute pass@1 points; relative to the coder-only baseline, the gain is 33 additional solved tasks and +18.8 points. We also evaluate on BigCodeBench (Hard) as a crossbenchmark generalization check. This second benchmark differs in composition and is evaluated with its own official calibrated execution setting. The result is consistent with the main benchmark in table III: SCOPE (Full) achieves 63/148 solved tasks (42.6% pass@1), compared with 54/148 (36.5%) for Reflexion, 51/148 (34.5%) for coder-only generation, and 62/148 (41.9%) for SCOPE (SFT). SCOPE remains the strongest method even when evaluated on a second executionbased benchmark with a different task distribution. Overall, SCOPE delivers the strongest performance in our main evaluation, and this advantage remains visible when we test on a second benchmark designed to reduce concern about benchmark-specific fitting. B. RQ2: On Which Kinds of Tasks Does SCOPE Help Most, by Difficulty and Problem Category? In Table I, we demonstrate the difficulty breakdown performance. On Easy tasks, SCOPE (Full) achieves the best result with 42/43 solved (97.7%), improving over Reflexion and Self-Refine, both at 39/43 (90.7%), and over the coderonly baseline at 26/43 (60.5%). On Medium tasks, SCOPE again obtains the strongest result with 18/52 solved (34.6%), compared with 16/52 (30.8%) for Reflexion and Self-Refine and 8/52 (15.4%) for the baseline. On Hard tasks, SCOPE reaches 9/80 (11.2%), matching Reflexion and clearly outperforming Self-Refine at 3/80 (3.8%) and the baseline at 2/80 (2.5%). This pattern suggests that SCOPE consistently improves reliability up to the medium range and remains strong on hard tasks, while more exploratory feedback can still sometimes rescue especially difficult cases. In Table II, the category breakdown clarifies where SCOPE’s gains come from. SCOPE (Full) is the strongest in most of the reported categories. On array tasks, the baseline solves none of the tasks (0.000), whereas all feedbackbased methods, including SCOPE, reach 0.455. On dynamic programming, SCOPE reaches 0.250, exceeding Reflexion at 0.167 and both the baseline and Self-Refine at 0.000. It fits the intuition that dynamic programming requires preserving intermediate invariants and state relationships that benefit from explicit subgoal decomposition. SCOPE is also strong on categories where hidden constraints are global rather than purely local. On hash-map

TABLE II PASS @1 BY A LGORITHMIC C ATEGORY ON L IVE C ODE B ENCH V6. B EST PER CATEGORY COLUMN IN BOLD .

Approach

Array

DP

Graph

Hash Map

Math

Simulation

String

Coder-only Reflexion Self-Refine SCOPE (Untrained) SCOPE (SFT) SCOPE (Full)

0.000 0.455 0.455 0.455 0.455 0.455

0.000 0.167 0.000 0.250 0.167 0.250

0.063 0.375 0.313 0.250 0.250 0.375

0.385 0.692 0.615 0.692 0.615 0.692

0.262 0.381 0.333 0.405 0.381 0.405

0.214 0.286 0.214 0.214 0.286 0.357

0.333 0.500 0.500 0.500 0.444 0.444

TABLE III C OMPARISON OF CODER - ONLY, R EFLEXION , SCOPE-SFT, AND SCOPE ON B IG C ODE B ENCH . S OLVED AND PASS @1 REPORT OVERALL PERFORMANCE . “SCOPE W INS ” AND “SCOPE R EGR .” ARE MEASURED RELATIVE TO SCOPE ( OURS ). FAILURE CATEGORIES SUMMARIZE THE REMAINING UNSOLVED CASES .

Method

Solved

pass@1

SCOPE Wins

SCOPE Regr.

Fail-Crash

Fail-AssertionOnly

Fail-Mixed

Coder-only Reflexion SCOPE (SFT) SCOPE (Full)

51/148 54/148 62/148 63/148

0.3446 0.3649 0.4189 0.4257

19 16 4 –

7 7 3 –

30 33 23 21

53 50 51 52

14 10 11 11

TABLE IV C ODER - ONLY- ANCHORED LOCALIZATION COMPARISON ON B IG C ODE B ENCH -C OMPLETE (H ARD ). E ACH ROW USES THE SAME CODER - ONLY CODER - ONLY BASELINE AS THE ANCHOR . W E CONSIDER TASKS WHERE THE CODER - ONLY SOLUTION FAILS AND THE TARGET METHOD SUCCEEDS . H IGHER IS BETTER FOR RECOVERY AND LOCALIZATION METRICS ; LOWER IS BETTER FOR EDIT- SIZE METRICS . B EST VALUES ARE SHOWN IN BOLD .

coder-only → Target Coder-only → Reflexion Coder-only → SCOPE

N Recovery Trigger+Fix Localized Localized Share Median Changed Median Changed Wins Rate Coverage Wins @20 Among Covered Lines ↓ Ratio ↓ 16 19

16.5% 19.6%

37.5% 47.4%

31.3% 42.1%

tasks, SCOPE reaches 0.692, tying Reflexion for the best result and improving over the baseline at 0.385. On math tasks, SCOPE achieves the best score at 0.405, compared with 0.381 for Reflexion and 0.262 for the baseline. On simulation, SCOPE attains 0.357, again the highest value in the table, improving over Reflexion at 0.286 and the baseline at 0.214. These gains are consistent with the intended role of SCOPE: making latent semantic requirements explicit enough that the coder can repair them systematically rather than relying only on free-form critique. On graph problems, SCOPE reaches 0.375, tying Reflexion for the best result and outperforming Self-Refine at 0.313 and the baseline at 0.063. Graph problems are often structurally complex. They can also admit multiple plausible solution paths. As a result, SCOPE’s advantage is smaller on these tasks. Success often depends more on exploring alternative strategies than on correcting a specific semantic error. SCOPE improves over Reflexion on dynamic programming (0.250 vs. 0.167), math (0.405 vs. 0.381), and simulation (0.357 vs. 0.286), while tying Reflexion on graph and hashmap tasks. These are categories where failures often come from violating a recurrence, numeric invariant, uniqueness condition, or state-transition rule. The gains are smaller where the main challenge is broad strategy exploration rather than fixing a specific violated obligation. SCOPE is most useful

83.3% 88.9%

35.0 28.0

0.703 0.577

when a draft is close enough to repair and the missing behavior can be expressed as a small number of explicit obligations. C. RQ3: What Explains SCOPE’s Advantage Over Baselines in Localization and Revision Behavior? Table III combines three complementary views of performance: overall pass@1, pairwise win/loss decomposition against each baseline, and failure-mode shift on the remaining unsolved tasks. Under this view, SCOPE achieves the strongest overall result on BigCodeBench-Complete (Hard), solving 63/148 tasks (42.6% pass@1), compared with 54/148 (36.5%) for Reflexion and 51/148 (34.5%) for coder-only generation. Relative to Reflexion, this corresponds to a net gain of +9 tasks (16 SCOPE wins vs. 7 regressions); relative to coder-only generation, the gain is +12 tasks (19 wins vs. 7 regressions). The same table also shows that SCOPE produces the fewest crash-like failures among the compared methods. In particular, Fail-Crash cases decrease from 33 under Reflexion to 21 under SCOPE, and from 30 under coder-only generation to 21. Crash failures are qualitatively different from pure assertion failures: they often indicate unresolved semantic mismatches, such as incorrect exception behavior, wrong API usage, or failure to satisfy hidden structural constraints in the harness. SCOPE is more often repairing the semantic

conditions that prevent the program from executing correctly in the first place. Table IV demonstrates the localization comparison on the same coder-only baseline for both Reflexion and SCOPE. Under this shared baseline, SCOPE rescues more coder-only failures than Reflexion, improving from 16 wins to 19 wins, or from 16.5% to 19.6% recovery on the 97 coder-only non-pass tasks. SCOPE also yields higher trigger+fix coverage (47.4% vs. 37.5%), which means a larger fraction of its successful repairs can be aligned to a concrete bug trigger and a concrete fix location. The difference also appears in localized rescue behavior. SCOPE achieves 8 localized wins within a 20line neighborhood of the coder-only trigger, compared with 5 for Reflexion; as a rate over all wins, this is 42.1% for SCOPE versus 31.3% for Reflexion. Even after restricting to cases where both trigger and fix can be identified, SCOPE remains better (88.9% vs. 83.3%). At the same time, SCOPE is more surgical: its median changed-line count is smaller (28.0 vs. 35.0), and its median changed-line ratio is also lower (0.577 vs. 0.703). Taken together, these results support a clearer mechanistic claim: SCOPE does not only solve more coder-only failures than Reflexion; it also repairs them more consistently near the same baseline bug signal, while requiring smaller code changes. SCOPE helps apply compact repairs near the actual fault location when revision is needed. These repairs concentrate on semantic-contract regions rather than on broad structural rewrites. VIII. D ISCUSSION Our results show that the main value of SCOPE is introducing a prover-initialized critic that makes semantic obligations explicit for revision. This suggests that feedback-based code generation can benefit from structured intermediate reasoning, especially when the main errors are semantic. A. Implications and Future Work Reduction of Search Space. A key implication of SCOPE is that structured obligations reduce the repair search space. The implementation does not execute Lean tactics, but it borrows the prover-style habit of decomposing a large goal into smaller obligations. Once a programming task is rewritten as concrete obligations, many semantically irrelevant revisions can be ruled out early. The coder is therefore not searching broadly for any program that might pass hidden tests, but revising within a smaller space of edits consistent with the identified obligations. This helps explain why SCOPE tends to produce compact, localized repairs rather than broad rewriting. As future work, this perspective suggests promising directions. One is to integrate subgoal-guided search more directly into decoding, allowing the coder to plan revisions around partially satisfied obligations instead of relying only on post hoc repair. Implications for Agentic Coding Systems. Our results also suggest a broader implication for agentic software engineering systems. Future coding agents may benefit from maintaining an explicit obligation state between task understanding and

code editing. Such a state can help determine which constraint is violated, where the likely fault lies, and whether the next revision should be local or global. Our findings also provide evidence for role specialization in multi-agent code generation. In SCOPE, a smaller, specialized critic improves a larger coder not by generating better code directly, but by providing a stronger semantic representation of what the draft is missing. This suggests that future agentic systems may be most effective when large coders are paired with smaller expert critics for semantics, localization, and repair planning. B. Threats to Validity and Limitations Our study has several limitations. First, the evaluation scope is still narrow. SCOPE is trained and tested only on Python code-generation benchmarks, and the tasks are closer to code snippet level programming problems than to full repository scale software engineering workflows. To reduce the risk of overfitting to a single benchmark, we evaluate not only on LiveCodeBench V6 but also on BigCodeBench (Hard), which differs in task composition and execution setup. Even so, broader validation across languages, real repositories, and longer-horizon agentic coding tasks remains future work. Second, SCOPE is not a full formal verification system. We do not prove that the final Python program satisfies a complete formal specification, and the semantic obligations generated by the critic may themselves be incomplete, approximate, or occasionally misaligned with the true intent of the task. Our goal is therefore more practical than end-to-end certification: we use a prover-initialized model as a structured semantic critic that makes intent more explicit before revision. To reduce the risk that the critic produces merely plausible but unhelpful obligations, we train it with both dense rewards for structured semantic quality and sparse rewards based on downstream execution improvement. IX. C ONCLUSION We present SCOPE, a prover-initialized subgoal critic for Python code generation. By translating natural-language tasks into explicit repair obligations and comparing them against draft programs, SCOPE provides structured feedback that guides targeted repair. Through a three-stage design: execution-grounded data construction, supervised fine-tuning, and process-aligned reinforcement learning with dense semantic reward and sparse execution reward, we show that proverstyle subgoal decomposition can be adapted from formal reasoning to practical code generation without claiming full formal verification. Through evaluation on LiveCodeBench and BigCodeBench, SCOPE achieves the strongest overall performance among the compared baselines, improving over coder-only generation and feedback-based methods such as Reflexion and Self-Refine under the same coder setting. Our analysis further shows that SCOPE helps most on tasks with stronger semantic structure, reduces crash-like failures, and produces more localized repairs rather than broad rewriting. These findings suggest that the main value of the prover-initialized critic in this setting is

not end-to-end verification, but making natural-language intent explicit enough to guide reliable revision. R EFERENCES [1] D. Nam, A. Macvean, V. Hellendoorn, B. Vasilescu, and B. Myers, “Using an LLM to help with code understanding,” in Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. ACM, 2024, pp. 1–13. [2] S. Joel, J. Wu, and F. Fard, “A survey on LLM-based code generation for low-resource and domain-specific programming languages,” ACM Transactions on Software Engineering and Methodology, 2025. [3] M. Kazemitabaar, X. Hou, A. Henley, B. J. Ericson, D. Weintrop, and T. Grossman, “How novices use LLM-based code generators to solve CS1 coding tasks in a self-paced learning environment,” in Proceedings of the 23rd Koli Calling International Conference on Computing Education Research. ACM, 2023, pp. 1–12. [4] S. Zhao, A. Zhu, H. Mozannar, D. Sontag, A. Talwalkar, and V. Chen, “CodingGenie: A proactive LLM-powered programming assistant,” in Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering. ACM, 2025, pp. 1168–1172. [5] A. S. Shethiya, “AI-assisted code generation and optimization in .NET web development,” Annals of Applied Sciences, vol. 6, no. 1, pp. 1–7, 2025, short article; verify venue suitability before submission. [Online]. Available: https://annalsofappliedsciences.com/index.php/aas/ article/view/15 [6] Z. Zhang, C. Wang, Y. Wang, E. Shi, Y. Ma, W. Zhong, J. Chen, M. Mao, and Z. Zheng, “LLM hallucinations in practical code generation: Phenomena, mechanism, and mitigation,” Proceedings of the ACM on Software Engineering, vol. 2, no. ISSTA, pp. 481–503, 2025. [7] X. Chen, C. Gao, C. Chen, G. Zhang, and Y. Liu, “An empirical study on challenges for LLM application developers,” ACM Transactions on Software Engineering and Methodology, vol. 34, no. 7, pp. 1–37, 2025. [8] C. Wang, K. Huang, J. Zhang, Y. Feng, L. Zhang, Y. Liu, and X. Peng, “LLMs meet library evolution: Evaluating deprecated API usage in LLM-based code completion,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 885– 897. [9] M. Sch”afer, S. Nadi, A. Eghbali, and F. Tip, “An empirical evaluation of using large language models for automated unit test generation,” IEEE Transactions on Software Engineering, vol. 50, no. 1, pp. 85–105, 2024. [10] J. Wang, Y. Huang, C. Chen, Z. Liu, S. Wang, and Q. Wang, “Software testing with large language models: Survey, landscape, and vision,” IEEE Transactions on Software Engineering, vol. 50, no. 4, pp. 911–936, 2024. [11] J. Liu, K. Wang, Y. Chen, X. Peng, Z. Chen, L. Zhang, and Y. Lou, “Large language model-based agents for software engineering: A survey,” 2024, the previously claimed TOSEM publication could not be verified as of 2026-06-30. [Online]. Available: https://arxiv.org/abs/2409.02977 [12] L. Yang, C. Yang, S. Gao, W. Wang, B. Wang, Q. Zhu, X. Chu, J. Zhou, G. Liang, Q. Wang, and J. Chen, “On the evaluation of large language models in unit test generation,” in Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. ACM, 2024, pp. 1607–1619. [13] E. First, M. N. Rabe, T. Ringer, and Y. Brun, “Baldur: Whole-proof generation and repair with large language models,” in Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM, 2023, pp. 1229–1241. [14] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “seL4: Formal verification of an OS kernel,” in Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. ACM, 2009, pp. 207–220. [15] L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340. [16] C. Loughridge, Q. Sun, S. Ahrenbach, F. Cassano, C. Sun, Y. Sheng, A. Mudide, M. R. H. Misu, N. Amin, and M. Tegmark, “DafnyBench: A benchmark for formal software verification,” 2024. [Online]. Available: https://arxiv.org/abs/2406.08467

[17] A. Thakur, J. C. H. Lee, G. Tsoukalas, M. Sistla, M. Zhao, S. Zetzsche, G. Durrett, Y. Yue, and S. Chaudhuri, “CLEVER: A curated benchmark for formally verified code generation,” in Advances in Neural Information Processing Systems, vol. 38, 2025, datasets and Benchmarks Track. [Online]. Available: https://papers.nips.cc/paper files/paper/ 2025/hash/a7f67788f7b4d77fa7cd6887de3dcbe7-Abstract-Datasets and Benchmarks Track.html [18] R. Wang, J. Zhang, Y. Jia, R. Pan, S. Diao, R. Pi, and T. Zhang, “TheoremLlama: Transforming general-purpose LLMs into Lean4 experts,” in Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, 2024, pp. 11 953–11 974. [19] J. Zhang, Q. Wang, X. Ji, Y. Liu, Y. Yue, F. Zhang, D. Zhang, G. Zhou, and K. Gai, “Leanabell-Prover: Posttraining scaling in formal reasoning,” 2025. [Online]. Available: https://arxiv.org/abs/2504.06122 [20] L. de Moura and S. Ullrich, “The Lean 4 theorem prover and programming language,” in Automated Deduction – CADE 28. Springer, 2021, pp. 625–635. [21] K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “LeanDojo: Theorem proving with retrieval-augmented language models,” in Advances in Neural Information Processing Systems, vol. 36, 2023, pp. 21 573–21 612, datasets and Benchmarks Track. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/ 2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets and Benchmarks.html [22] T. Hubert, R. Mehta, L. Sartran, M. Z. Horváth, G. Žužić, E. Wieser, A. Huang, J. Schrittwieser, Y. Schroecker, H. Masoom et al., “Olympiadlevel formal mathematical reasoning with reinforcement learning,” Nature, vol. 651, no. 8106, pp. 607–613, 2025. [23] Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang et al., “DeepSeek-ProverV2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,” 2025. [Online]. Available: https://arxiv.org/abs/2504.21801 [24] Y. Lin, S. Tang, B. Lyu, Z. Yang, J.-H. Chung, H. Zhao, L. Jiang, Y. Geng, J. Ge, J. Sun et al., “Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction,” 2025. [Online]. Available: https://arxiv.org/abs/2508.03613 [25] K. Yang, G. Poesia, J. He, W. Li, K. E. Lauter, S. Chaudhuri, and D. Song, “Position: Formal mathematical reasoning—a new frontier in AI,” in Proceedings of the 42nd International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, vol. 267. PMLR, 2025, pp. 82 384–82 398. [Online]. Available: https://proceedings.mlr.press/v267/yang25az.html [26] N. Shinn, F. Cassano, E. Berman, A. Gopinath, K. Narasimhan, and S. Yao, “Reflexion: Language agents with verbal reinforcement learning,” in Advances in Neural Information Processing Systems, vol. 36, 2023, pp. 8634–8652. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/2023/hash/ 1b44b878bb782e6954cd888628510e90-Abstract-Conference.html [27] B. Rozière, J. Gehring, F. Gloeckle, S. Sootla, I. Gat, X. E. Tan, Y. Adi, J. Liu, R. Sauvestre, T. Remez et al., “Code Llama: Open foundation models for code,” 2023. [Online]. Available: https://arxiv.org/abs/2308.12950 [28] R. Li, L. B. Allal, Y. Zi, N. Muennighoff, D. Kocetkov, C. Mou, M. Marone, C. Akiki, J. Li, J. Chim et al., “StarCoder: May the source be with you!” Transactions on Machine Learning Research, 2023. [Online]. Available: https://openreview.net/forum?id=KoFOg41haE [29] F. Liu, Y. Liu, L. Shi, Z. Yang, L. Zhang, X. Lian, Z. Li, and Y. Ma, “Beyond functional correctness: Exploring hallucinations in LLM-generated code,” IEEE Transactions on Software Engineering, vol. 52, no. 3, pp. 1037–1055, 2026. [30] Y. Tian, W. Yan, Q. Yang, X. Zhao, Q. Chen, W. Wang, Z. Luo, L. Ma, and D. Song, “CodeHalu: Investigating code hallucinations in LLMs via execution-based verification,” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 39, no. 24, pp. 25 300–25 308, 2025. [31] J. Spracklen, R. Wijewickrama, A. H. M. N. Sakib, A. Maiti, B. Viswanath, and M. Jadliwala, “We have a package for you! a comprehensive analysis of package hallucinations by code-generating LLMs,” in 34th USENIX Security Symposium (USENIX Security 25). USENIX Association, 2025, pp. 3687–3706. [Online]. Available: https: //www.usenix.org/conference/usenixsecurity25/presentation/spracklen

[32] A. Eghbali and M. Pradel, “De-hallucinator: Mitigating LLM hallucinations in code generation tasks via iterative grounding,” 2024. [Online]. Available: https://arxiv.org/abs/2401.01701 [33] A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe, U. Alon, N. Dziri, S. Prabhumoye, Y. Yang et al., “Self-refine: Iterative refinement with self-feedback,” in Advances in Neural Information Processing Systems, vol. 36, 2023, pp. 46 534–46 594. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/2023/hash/ 91edff07232fb1b55a505a9e9f6c0ff3-Abstract-Conference.html [34] X. Chen, M. Lin, N. Sch”arli, and D. Zhou, “Teaching large language models to self-debug,” in The Twelfth International Conference on Learning Representations, 2024. [Online]. Available: https://openreview.net/forum?id=KuPixIqPiq [35] Z. Liu, X. Bai, K. Chen, X. Chen, X. Li, Y. Xiang, J. Liu, H.-D. Li, Y. Wang, L. Nie et al., “A survey on the feedback mechanism of llmbased ai agents,” in Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence, 2025, pp. 10 582–10 592. [36] J. Stamper, R. Xiao, and X. Hou, “Enhancing llm-based feedback: Insights from intelligent tutoring systems and the learning sciences,” in International Conference on Artificial Intelligence in Education. Springer, 2024, pp. 32–43. [37] H. Le, Y. Wang, A. D. Gotmare, S. Savarese, and S. C. H. Hoi, “CodeRL: Mastering code generation through pretrained models and deep reinforcement learning,” in Advances in Neural Information Processing Systems, vol. 35, 2022. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/2022/hash/ 8636419dea1aa9fbd25fc4248e702da4-Abstract-Conference.html [38] M. Yuksekgonul, F. Bianchi, J. Boen, S. Liu, P. Lu, Z. Huang, C. Guestrin, and J. Zou, “Optimizing generative AI by backpropagating language model feedback,” Nature, vol. 639, no. 8055, pp. 609–616, 2025. [39] I. Bouzenia, P. Devanbu, and M. Pradel, “Repairagent: An autonomous, LLM-based agent for program repair,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 2188–2200. [40] H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang, “DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data,” 2024. [Online]. Available: https://arxiv.org/abs/2405.14333