Pith. sign in

REVIEW 3 major objections 8 minor 41 references

Reviewed by Pith at T0; open to challenge.

T0 means a machine referee read the full paper against a public rubric. The mark states how deep the mechanical check went, never who wrote it. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · glm-5.2

Prover-trained critic makes code repairs surgical, not scattergun

2026-07-08 23:22 UTC pith:FZOGJOKH

load-bearing objection Novel idea (prover-as-critic), but the headline numbers are not statistically distinguishable from noise. the 3 major comments →

arxiv 2607.05810 v1 pith:FZOGJOKH submitted 2026-07-07 cs.SE

SCOPE: Leveraging Subgoal Critiques for Code Generation

Yueke Zhang , Yifan Zhang , Zihan Fang , Kevin Leach , Wei Zhang , Yu Huang This is my paper
classification cs.SE
keywords codegenerationscopecoder-onlycritiquereflexionanalysiscompared
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper claims that a language model trained for formal theorem proving (in Lean) can be repurposed as a critic for general-purpose code generation. The critic does not run formal verification; instead, it uses its training in step-by-step decomposition to read a programming task and a draft solution, then emit three structured fields: subgoals the code must satisfy, an analysis of where the draft falls short, and a robustness checklist for edge cases. When this structured feedback is fed back to a code-generating model, the model makes smaller, more targeted repairs than it does under free-form critique. The paper supports this with a two-stage training pipeline: supervised fine-tuning to teach the prover model the critic interface, and reinforcement learning with a dense reward for matching teacher-generated critique style and a sparse reward for whether the critique actually improves the code's execution results. The central claim is that the value of the prover model lies not in end-to-end certification but in converting vague natural-language intent into explicit, localized repair obligations, thereby shrinking the search space for code revision.

Core claim

The core discovery is that the subgoal-decomposition behavior learned by a formal theorem-proving model (DeepSeek-Prover-V2, trained on Lean) transfers productively to Python code generation when used as a structured critic. The paper shows that this transfer yields concrete improvements: on LiveCodeBench V6, pass@1 rises to 39.4% from Reflexion's 36.6%, and on BigCodeBench Hard, it reaches 42.6% from 36.5%. The mechanism behind the gain is more precise localization: when the prover-initialized critic identifies a violated semantic obligation, the coder's fix lands closer to the actual bug (42.1% of recovered fixes within 20 lines of the fault, vs. 31.3% for Reflexion) and involves fewer sp3

What carries the argument

The central object is the structured critique y = (s, g, c), consisting of subgoals, gap analysis, and a robustness checklist, produced by a prover-initialized critic model (DeepSeek-Prover-V2-7B) after supervised fine-tuning and GRPO-based reinforcement learning with combined dense (embedding-similarity + judge-quality) and sparse (execution-improvement) rewards.

Load-bearing premise

The dense reward during reinforcement learning measures how similar the critic's output is to teacher-generated critiques, using embedding similarity. The teacher critiques come from a single model on only 528 training examples. If the teacher's critique style is suboptimal or the examples are not representative, the dense reward anchors the critic to a potentially poor local optimum, and the paper does not test sensitivity to teacher quality or training-set size.

What would settle it

If the dense reward term is removed and the critic is trained with only the sparse execution-improvement reward, and the resulting system performs comparably, then the structured semantic alignment provided by the teacher is not load-bearing and the gains reduce to execution-guided search.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Code generation systems could adopt explicit obligation-state tracking as a standard intermediate representation between task understanding and code editing, making repair a targeted operation rather than a resampling exercise.
  • The role specialization demonstrated here (a smaller specialized critic guiding a larger general coder) suggests a design pattern for agentic systems where expert models handle semantic analysis and repair planning rather than direct generation.
  • If the subgoal-decomposition prior generalizes beyond Python to typed or partially-specified languages, it could bridge the gap between informal natural-language requirements and lightweight formal reasoning without requiring full manual specification.
  • The localization metrics (trigger-to-fix distance, changed-line count) provide a concrete evaluation protocol for future repair systems to demonstrate surgical precision rather than relying solely on pass/fail rates.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 8 minor

Summary. This paper presents SCOPE, a prover-initialized subgoal critic for code generation. The core idea is to adapt a Lean-oriented prover model (DeepSeek-Prover-V2-7B) into a structured critic that emits three fields—subgoals, gap analysis, and a robustness checklist—to guide a frozen coder (Qwen3-Coder-30B) in revising draft programs. The critic is trained in three stages: (1) data construction using a teacher model (DeepSeek-V3) to generate 528 critique traces from LiveCodeBench V1–V3, (2) supervised fine-tuning (SFT) for role alignment, and (3) process-aligned reinforcement learning via GRPO with a dense semantic reward (embedding similarity to teacher critiques plus a GPT-5.2 quality judge) and a sparse execution-based reward. Evaluation on LiveCodeBench V6 (175 tasks) and BigCodeBench Hard (148 tasks) shows SCOPE achieving 39.4% and 42.6% pass@1, respectively, compared to Reflexion at 36.6% and 36.5%. Additional analysis examines difficulty/category breakdowns and repair localization metrics.

Significance. The paper's core idea—repurposing a prover-trained model as a structured semantic critic for code repair rather than as a runtime verifier—is creative and well-motivated. The three-field critique format (subgoals, gap analysis, checklist) is a clean interface design, and the process-aligned RL reward that optimizes the critic for downstream coder improvement rather than critique quality alone is a sensible formulation. The repair localization analysis (Table IV) provides useful mechanistic evidence beyond raw pass@1 numbers. However, the empirical evidence supporting the central claims is thin: single-run evaluations with small absolute gains, no significance testing, and an RL contribution that appears inconsistent across benchmarks. These issues are load-bearing for the paper's claims and need to be addressed.

major comments (3)
  1. §VII-A, Table I: The headline gain over Reflexion on LiveCodeBench V6 is 69/175 vs 64/175 (+5 tasks), and on BigCodeBench Hard (Table III) it is 63/148 vs 54/148 (+9 tasks net, 16 wins vs 7 regressions). Neither difference reaches conventional statistical significance under a two-proportion test (z≈0.54, p≈0.59 for LiveCodeBench; z≈1.07, p≈0.28 for BigCodeBench). The paper reports no confidence intervals, no multiple random seeds, and no paired test (e.g., McNemar's). Since the central claim is that SCOPE improves pass@1 over Reflexion, this is load-bearing: without significance testing or multiple seeds, the reported gains cannot be distinguished from sampling noise. The authors should either run multiple seeds and report variance, or at minimum provide a paired statistical test (McNemar's or similar) on the per-task outcomes.
  2. §VII-A, Tables I and III: The contribution of the RL stage is inconsistent across benchmarks. On LiveCodeBench V6, SCOPE (Full) at 69/175 (39.4%) improves over SCOPE (SFT) at 62/175 (35.4%) by +7 tasks (+4.0 points). On BigCodeBench Hard, SCOPE (Full) at 63/148 (42.6%) improves over SCOPE (SFT) at 62/148 (41.9%) by only +1 task (+0.7 points). Since the RL reward design (dense + sparse, Eqs. 5–8) is a central contribution, the authors should explain why the RL stage's benefit varies so substantially across benchmarks, or provide an ablation isolating the dense vs. sparse reward components to clarify which part of the RL design is responsible for the gains.
  3. §V-C, Eq. 6: The dense reward R_emb measures embedding similarity between generated critiques and teacher-generated targets from only 528 training tuples (§V-A). This means the RL optimizer is partly rewarded for reproducing the teacher's critique style. The paper does not ablate teacher quality, training set size sensitivity, or the effect of removing R_emb from the reward. Given that R_emb is one of two dense reward terms and the training set is small, an ablation showing the effect of w_dense (or R_emb specifically) on final performance would strengthen the claim that the dense reward is necessary and not merely anchoring the critic to a potentially suboptimal teacher distribution.
minor comments (8)
  1. §V-A: The 528 training tuples are described as coming from LiveCodeBench V1–V3, but the number of source tasks and the yield rate (how many tasks produced usable tuples) are not reported. Adding these details would help readers assess data coverage.
  2. §V-C, Eq. 6: The embedding similarity function sim(·) is not specified (which embedding model, dimensionality, or normalization). This should be stated for reproducibility.
  3. §V-C: The reward weights (λ_emb, λ_qual, w_dense, w_sparse, β, α_s, α_g, α_c) are listed as free parameters but their values are not reported in the paper. These should be specified, at least in an appendix or supplementary material.
  4. §V-C: The GPT-5.2 judge for R_qual introduces a dependency on a proprietary model. The paper should discuss whether this creates reproducibility concerns and whether an open-source judge was considered as an alternative.
  5. Table II: Some categories have very few tasks (e.g., Array has 11 tasks at 0.455 for all methods). The small sample sizes make category-level comparisons unreliable; reporting task counts per category would help readers interpret these results.
  6. §VIII-B: The threats to validity section mentions that SCOPE is trained and tested only on Python, but does not discuss the statistical fragility of the evaluation (single-run, small n). This should be acknowledged.
  7. Reference [5] includes an unusual note ('short article; verify venue suitability before submission') and reference [11] includes a note about unverifiable publication status. These should be cleaned up.
  8. Abstract: The final sentence is grammatically incomplete ('its localized code corrections than Reflexion's').

Simulated Author's Rebuttal

3 responses · 1 unresolved

We thank the referee for a careful and constructive review. The referee raises three major concerns: (1) lack of significance testing or multiple seeds for the headline pass@1 comparisons, (2) inconsistent RL contribution across benchmarks without a dense/sparse reward ablation, and (3) no ablation isolating R_emb or teacher-quality sensitivity given the small 528-tuple training set. We agree that all three points are valid and will address them in revision. For (1), we will run multiple seeds and report McNemar's test on per-task paired outcomes. For (2) and (3), we will add ablations decomposing the dense and sparse reward components and isolating R_emb. We cannot fully resolve the concern that absolute gains are modest, but the paired analysis and mechanistic evidence (Table IV) provide complementary support for the method's contribution.

read point-by-point responses

  1. Referee: §VII-A, Table I: The headline gain over Reflexion on LiveCodeBench V6 is 69/175 vs 64/175 (+5 tasks), and on BigCodeBench Hard (Table III) it is 63/148 vs 54/148 (+9 tasks net, 16 wins vs 7 regressions). Neither difference reaches conventional statistical significance under a two-proportion test (z≈0.54, p≈0.59 for LiveCodeBench; z≈1.07, p≈0.28 for BigCodeBench). The paper reports no confidence intervals, no multiple random seeds, and no paired test (e.g., McNemar's). Since the central claim is that SCOPE improves pass@1 over Reflexion, this is load-bearing: without significance testing or multiple seeds, the reported gains cannot be distinguished from sampling noise. The authors should either run multiple seeds and report variance, or at minimum provide a paired statistical test (McNemar's or similar) on the per-task outcomes.

    Authors: The referee is correct that the current manuscript does not report significance testing, confidence intervals, or multiple seeds, and we agree this is a load-bearing gap. We will address this in revision by running SCOPE (Full) and Reflexion across at least 3 random seeds on both benchmarks and reporting mean pass@1 with standard deviation. Additionally, we will compute McNemar's test on the per-task paired outcomes (tasks solved by one method but not the other) for the primary seed, which is the appropriate paired test for this experimental design. We acknowledge that the absolute gains are modest (+5 tasks on LiveCodeBench V6, +9 net on BigCodeBench Hard), and the two-proportion z-tests the referee computed are indeed not significant at conventional thresholds. The paired McNemar's test may or may not reach significance depending on the discordant pair counts; we will report whatever the data shows honestly. If the paired test does not reach significance, we will adjust the framing of our claims accordingly, noting that the gains are directionally consistent but not statistically significant at standard thresholds on these benchmark sizes. We will also expand the discussion of the mechanistic evidence (Table IV localization analysis) as complementary support, while being transparent that this does not substitute for statistical significance on the primary metric. revision: yes

  2. Referee: §VII-A, Tables I and III: The contribution of the RL stage is inconsistent across benchmarks. On LiveCodeBench V6, SCOPE (Full) at 69/175 (39.4%) improves over SCOPE (SFT) at 62/175 (35.4%) by +7 tasks (+4.0 points). On BigCodeBench Hard, SCOPE (Full) at 63/148 (42.6%) improves over SCOPE (SFT) at 62/148 (41.9%) by only +1 task (+0.7 points). Since the RL reward design (dense + sparse, Eqs. 5–8) is a central contribution, the authors should explain why the RL stage's benefit varies so substantially across benchmarks, or provide an ablation isolating the dense vs. sparse reward components to clarify which part of the RL design is responsible for the gains.

    Authors: The referee correctly identifies an inconsistency in the RL stage's contribution across benchmarks that the current manuscript does not adequately address. We agree that this needs explanation and additional ablation evidence. In revision, we will add an ablation decomposing the RL reward into its constituent components: (a) dense reward only (R_dense), (b) sparse reward only (R_sparse), and (c) the full combined reward, evaluated on both benchmarks. This will clarify which component drives the gains on each benchmark. Regarding the cross-benchmark inconsistency: our current hypothesis is that the RL stage's sparse execution reward provides more signal on LiveCodeBench V6 because the training data (LiveCodeBench V1–V3) shares task structure and difficulty distribution with V6, making the execution-based reward more informative for the policy gradient. BigCodeBench Hard, by contrast, has a different task composition and execution setup, so the sparse reward signal may transfer less effectively, leaving the SFT checkpoint already near a local ceiling. However, this is a post-hoc explanation and we will frame it as such, presenting the ablation data to let readers judge. If the ablation shows that neither reward component produces consistent gains across both benchmarks, we will revise our claims about the RL contribution accordingly, potentially narrowing the claim to the in-distribution setting. revision: yes

  3. Referee: §V-C, Eq. 6: The dense reward R_emb measures embedding similarity between generated critiques and teacher-generated targets from only 528 training tuples (§V-A). This means the RL optimizer is partly rewarded for reproducing the teacher's critique style. The paper does not ablate teacher quality, training set size sensitivity, or the effect of removing R_emb from the reward. Given that R_emb is one of two dense reward terms and the training set is small, an ablation showing the effect of w_dense (or R_emb specifically) on final performance would strengthen the claim that the dense reward is necessary and not merely anchoring the critic to a potentially suboptimal teacher distribution.

    Authors: This is a fair concern. The R_emb term does anchor the critic to the teacher distribution, and with only 528 training tuples, the risk of anchoring to a suboptimal teacher is real. The current manuscript does not ablate this, and we agree it should. In revision, we will add the following ablations: (1) R_emb removed from the dense reward (keeping only R_qual), (2) the full dense reward removed entirely (sparse reward only), and (3) a training set size sensitivity analysis using subsets of the 528 tuples (e.g., 50%, 75%) to show whether performance degrades with fewer teacher examples. We will also add a brief discussion of teacher quality limitations, noting that the teacher critiques are generated by DeepSeek-V3 and are not ground truth. The design intent is that R_emb provides format and content regularization during early RL training to prevent the critic from drifting into unstructured text, while the sparse execution reward provides the ultimate task signal. If the ablation shows that removing R_emb does not hurt or even improves performance, we will revise the framing to acknowledge that the embedding similarity term may not be necessary, and that the sparse reward and quality judge alone may suffice. We are committed to reporting the ablation results honestly regardless of whether they support the original design rationale. revision: yes

standing simulated objections not resolved
  • The absolute gains over Reflexion are modest (+5 tasks on LiveCodeBench V6, +9 net on BigCodeBench Hard), and even with multiple seeds and paired tests, the effect sizes may remain small. If the paired tests do not reach significance, we cannot honestly claim a statistically significant improvement; we can only report directional consistency and mechanistic evidence. The referee is right that this is load-bearing, and we cannot resolve it by argument alone—the data must back it up.

Circularity Check

0 steps flagged

No significant circularity found; dense reward R_emb anchors to teacher data but is not a claimed prediction, and evaluation is execution-based on held-out benchmarks.

full rationale

The paper's central claims are empirical pass@1 results on LiveCodeBench V6 and BigCodeBench Hard, measured via execution harnesses independent of the training pipeline. The dense reward R_emb (Eq. 6) does reward the critic for matching teacher-generated critiques from the 528 training tuples, which is a fitted quantity. However, this is a training signal component, not a claimed derivation or prediction. It is combined with R_sparse (Eq. 7), which is purely execution-based and independent of the teacher. The paper does not present R_emb as a 'first-principles result' or 'prediction' — it is a reward design choice. No self-citation chain is load-bearing: DeepSeek-Prover-V2 [23] is an external model by different authors, and the evaluation benchmarks (V6, BigCodeBench) differ from training data (V1–V3). The statistical significance concerns raised by the skeptic (small sample sizes, no paired tests) are correctness risks, not circularity. The one minor concern is that R_emb partially anchors the RL critic to teacher-fitted data, but this does not make any reported result equivalent to its inputs by construction, since the final evaluation is independent execution-based pass@1 on held-out tasks.

Axiom & Free-Parameter Ledger

7 free parameters · 4 axioms · 0 invented entities

The paper introduces no new formal entities, particles, forces, or mathematical objects. The 'subgoal,' 'gap analysis,' and 'checklist' fields are natural-language output categories, not formal constructs. The prover-initialized critic is a repurposed existing model (DeepSeek-Prover-V2-7B), not a new architecture. The free parameters are reward weights and similarity function choices that are used but not individually reported.

free parameters (7)
  • λ_emb = not specified
    Weight for embedding similarity reward in R_dense (Eq. 5). Value not reported in the paper.
  • λ_qual = not specified
    Weight for quality reward in R_dense (Eq. 5). Value not reported.
  • α_s, α_g, α_c = sum to 1, individual values not specified
    Weights for subgoal, gap analysis, and checklist similarity in R_emb (Eq. 6). Individual values not reported.
  • w_dense = not specified
    Weight for dense reward in final reward R(y) (Eq. 8). Value not reported.
  • w_sparse = not specified
    Weight for sparse reward in final reward R(y) (Eq. 8). Value not reported.
  • β = not specified
    KL regularization strength in GRPO (Eq. 4). Value not reported.
  • sim(·) = not specified
    Embedding-based similarity function used in R_emb (Eq. 6). Specific embedding model or metric not reported.
axioms (4)
  • domain assumption Prover-trained LLMs (DeepSeek-Prover-V2) retain a decomposition habit that transfers to natural-language code critique without runtime Lean verification.
    Section II and Figure 2 argue this transfer is plausible because prover models learn to decompose goals into subgoals. The paper provides empirical evidence (SCOPE Untrained matches Reflexion at 36.6%) but no mechanistic proof of transfer.
  • domain assumption Teacher-generated critiques from DeepSeek-V3 on 528 examples provide sufficient supervision for the dense reward signal.
    Section V-A describes the data construction pipeline. The 528 tuples are treated as adequate for SFT warm-start and as embedding targets for R_dense. No sensitivity analysis on teacher quality or dataset size is provided.
  • domain assumption GPT-5.2 can serve as a frozen judge for critique quality (R_qual) without introducing bias or circularity.
    Section V-C states R_qual is 'provided by a frozen GPT-5.2 judge.' The judge prompt and evaluation criteria are not specified, and the dependency on a proprietary model is not discussed as a threat to validity.
  • domain assumption LiveCodeBench V6 is a valid evaluation benchmark despite training on V1–V3 from the same benchmark family.
    Section VI-C acknowledges V6 is 'in-family repair evaluation' and uses BigCodeBench as a cross-benchmark check. The paper treats this as adequate but does not quantify potential data leakage or distribution overlap between V1–V3 and V6.

pith-pipeline@v1.1.0-glm · 20320 in / 3505 out tokens · 220339 ms · 2026-07-08T23:22:53.333048+00:00 · methodology

0 comments
read the original abstract

Code generation with large language models (LLMs) remains unreliable because generated programs can appear correct while still violating key semantic requirements in the natural language 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 prover-initialized 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 code corrections are more localized than Reflexion's.

Figures

Figures reproduced from arXiv: 2607.05810 by Kevin Leach, Wei Zhang, Yifan Zhang, Yueke Zhang, Yu Huang, Zihan Fang.

Figure 1
Figure 1. Figure 1: A natural-language task usually contains latent semantic requirements [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustration of the subgoal-decomposition prior that motivates SCOPE. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The figure contrasts Reflexion’s broad natural-language reasoning with SCOPE’s subgoal-guided analysis, which exposes the missing invariant and [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: SCOPE couples a coder with a prover-initialized critic that receives the problem and draft code, then emits structured subgoals, gap analysis, and [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages · 8 internal anchors

  1. [1]

    Using an LLM to help with code understanding,

    D. Nam, A. Macvean, V . Hellendoorn, B. Vasilescu, and B. Myers, “Using an LLM to help with code understanding,” inProceedings of the IEEE/ACM 46th International Conference on Software Engineering. ACM, 2024, pp. 1–13

    work page 2024

  2. [2]

    A survey on LLM-based code generation for low-resource and domain-specific programming languages,

    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

    work page 2025

  3. [3]

    How novices use LLM-based code generators to solve CS1 coding tasks in a self-paced learning environment,

    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,” inProceed- ings of the 23rd Koli Calling International Conference on Computing Education Research. ACM, 2023, pp. 1–12

    work page 2023

  4. [4]

    CodingGenie: A proactive LLM-powered programming assistant,

    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 Founda- tions of Software Engineering. ACM, 2025, pp. 1168–1172

    work page 2025

  5. [5]

    AI-assisted code generation and optimization in .NET web development,

    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

    work page 2025

  6. [6]

    LLM hallucinations in practical code gen- eration: Phenomena, mechanism, and mitigation,

    Z. Zhang, C. Wang, Y . Wang, E. Shi, Y . Ma, W. Zhong, J. Chen, M. Mao, and Z. Zheng, “LLM hallucinations in practical code gen- eration: Phenomena, mechanism, and mitigation,”Proceedings of the ACM on Software Engineering, vol. 2, no. ISSTA, pp. 481–503, 2025

    work page 2025

  7. [7]

    An empirical study on challenges for LLM application developers,

    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

    work page 2025

  8. [8]

    LLMs meet library evolution: Evaluating deprecated API usage in LLM-based code completion,

    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,” in2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 885– 897

    work page 2025

  9. [9]

    An empirical evaluation of using large language models for automated unit test generation,

    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

    work page 2024

  10. [10]

    Software testing with large language models: Survey, landscape, and vision,

    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

    work page 2024

  11. [11]

    Large Language Model-Based Agents for Software Engineering: A Survey

    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

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  12. [12]

    On the evaluation of large language models in unit test generation,

    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,” inProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. ACM, 2024, pp. 1607–1619

    work page 2024

  13. [13]

    Baldur: Whole-proof generation and repair with large language models,

    E. First, M. N. Rabe, T. Ringer, and Y . Brun, “Baldur: Whole-proof generation and repair with large language models,” inProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM, 2023, pp. 1229–1241

    work page 2023

  14. [14]

    seL4: Formal verification of an OS kernel,

    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,” inProceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. ACM, 2009, pp. 207–220

    work page 2009

  15. [15]

    Z3: An efficient SMT solver,

    L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” inTools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340

    work page 2008

  16. [16]

    DafnyBench: A Benchmark for Formal Software Verification

    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

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  17. [17]

    CLEVER: A curated benchmark for formally verified code generation,

    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,” inAdvances in Neural Information Processing Systems, vol. 38, 2025, datasets and Benchmarks Track. [Online]. Available: https://papers.nips.cc/paper files/paper/ 2025/hash/a7f67...

    work page 2025

  18. [18]

    Theo- remLlama: Transforming general-purpose LLMs into Lean4 experts,

    R. Wang, J. Zhang, Y . Jia, R. Pan, S. Diao, R. Pi, and T. Zhang, “Theo- remLlama: 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

    work page 2024

  19. [19]

    Leanabell-Prover: Posttraining Scaling in Formal Reasoning

    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

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  20. [20]

    The Lean 4 theorem prover and program- ming language,

    L. de Moura and S. Ullrich, “The Lean 4 theorem prover and program- ming language,” inAutomated Deduction – CADE 28. Springer, 2021, pp. 625–635

    work page 2021

  21. [21]

    LeanDojo: Theorem proving with retrieval-augmented language models,

    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/pape...

    work page arXiv 2023

  22. [22]

    Olympiad- level formal mathematical reasoning with reinforcement learning,

    T. Hubert, R. Mehta, L. Sartran, M. Z. Horv ´ath, G. ˇZuˇzi´c, E. Wieser, A. Huang, J. Schrittwieser, Y . Schroecker, H. Masoomet al., “Olympiad- level formal mathematical reasoning with reinforcement learning,”Na- ture, vol. 651, no. 8106, pp. 607–613, 2025

    work page 2025

  23. [23]

    DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

    Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yanget al., “DeepSeek-Prover- V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,” 2025. [Online]. Available: https://arxiv.org/abs/2504.21801

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  24. [24]

    Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction,

    Y . Lin, S. Tang, B. Lyu, Z. Yang, J.-H. Chung, H. Zhao, L. Jiang, Y . Geng, J. Ge, J. Sunet al., “Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction,”

    work page

  25. [25]

    Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

    [Online]. Available: https://arxiv.org/abs/2508.03613

    work page internal anchor Pith review Pith/arXiv arXiv

  26. [26]

    Position: Formal mathematical reasoning—a new frontier in AI,

    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,” inProceedings 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/ya...

    work page 2025

  27. [27]

    Reflexion: Language agents with verbal reinforcement learning,

    N. Shinn, F. Cassano, E. Berman, A. Gopinath, K. Narasimhan, and S. Yao, “Reflexion: Language agents with verbal reinforcement learning,” inAdvances 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

    work page 2023

  28. [28]

    Code Llama: Open Foundation Models for Code

    B. Rozi `ere, J. Gehring, F. Gloeckle, S. Sootla, I. Gat, X. E. Tan, Y . Adi, J. Liu, R. Sauvestre, T. Remezet al., “Code Llama: Open foundation models for code,” 2023. [Online]. Available: https://arxiv.org/abs/2308.12950

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  29. [29]

    StarCoder: May the source be with you!

    R. Li, L. B. Allal, Y . Zi, N. Muennighoff, D. Kocetkov, C. Mou, M. Marone, C. Akiki, J. Li, J. Chimet al., “StarCoder: May the source be with you!”Transactions on Machine Learning Research, 2023. [Online]. Available: https://openreview.net/forum?id=KoFOg41haE

    work page 2023

  30. [30]

    Beyond functional correctness: Exploring hallucinations in LLM-generated code,

    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

    work page 2026

  31. [31]

    CodeHalu: Investigating code hallucinations in LLMs via execution-based verification,

    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

    work page 2025

  32. [32]

    We have a package for you! a comprehensive analysis of package hallucinations by code-generating LLMs,

    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,” in34th USENIX Security Symposium (USENIX Security 25). USENIX Association, 2025, pp. 3687–3706. [Online]. Available: https: //www.usenix.org/conference/usenixse...

    work page 2025

  33. [33]

    De-Hallucinator: Mitigating LLM Hallucinations in Code Generation Tasks via Iterative Grounding

    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

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  34. [34]

    Self-refine: Iterative refinement with self-feedback,

    A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe, U. Alon, N. Dziri, S. Prabhumoye, Y . Yanget al., “Self-refine: Iterative refinement with self-feedback,” inAdvances in Neural Information Processing Systems, vol. 36, 2023, pp. 46 534–46 594. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/2023/hash/ 91edff07232fb1b5...

    work page 2023

  35. [35]

    Teaching large language models to self-debug,

    X. Chen, M. Lin, N. Sch”arli, and D. Zhou, “Teaching large language models to self-debug,” inThe Twelfth International Conference on Learning Representations, 2024. [Online]. Available: https://openreview.net/forum?id=KuPixIqPiq

    work page 2024

  36. [36]

    A survey on the feedback mechanism of llm- based ai agents,

    Z. Liu, X. Bai, K. Chen, X. Chen, X. Li, Y . Xiang, J. Liu, H.-D. Li, Y . Wang, L. Nieet al., “A survey on the feedback mechanism of llm- based ai agents,” inProceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence, 2025, pp. 10 582–10 592

    work page 2025

  37. [37]

    Enhancing llm-based feedback: Insights from intelligent tutoring systems and the learning sciences,

    J. Stamper, R. Xiao, and X. Hou, “Enhancing llm-based feedback: Insights from intelligent tutoring systems and the learning sciences,” inInternational Conference on Artificial Intelligence in Education. Springer, 2024, pp. 32–43

    work page 2024

  38. [38]

    CodeRL: Mastering code generation through pretrained models and deep reinforcement learning,

    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,” inAdvances in Neural Information Processing Systems, vol. 35, 2022. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/2022/hash/ 8636419dea1aa9fbd25fc4248e702da4-Abstract-Conference.html

    work page 2022

  39. [39]

    Optimizing generative AI by backpropagating language model feedback,

    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

    work page 2025

  40. [40]

    Repairagent: An autonomous, LLM-based agent for program repair,

    I. Bouzenia, P. Devanbu, and M. Pradel, “Repairagent: An autonomous, LLM-based agent for program repair,” in2025 IEEE/ACM 47th Inter- national Conference on Software Engineering (ICSE). IEEE, 2025, pp. 2188–2200

    work page 2025

  41. [41]

    DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

    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

    work page internal anchor Pith review Pith/arXiv arXiv 2024