Pith. sign in

REVIEW 4 major objections 4 minor 3 cited by

CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement

T0 review · 4 major / 4 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read CodeGrad claims a proof-gated pseudo-gradient loop can turn a weak code model into a much stronger one, with pass@1 gains up to 27% on HumanEval and 40.6% relative on LiveCodeBench V6.

desk verdict Real empirical lift from a stronger critic, but the 'formal verification' framing is unsupported and the baseline comparisons are missing; this is a revisable reject, not a waste of time. read the letter →

arxiv 2508.10059 v2 pith:EHE7RJQG submitted 2025-08-12 cs.SE

Yueke Zhang , Yifan Zhang , Kevin Leach , Yu Huang This is my paper
classification cs.SE
keywords codegenerationLLMrefinementtextualpseudo-gradientformalverificationiterativeself-critiquepass@1HumanEvalLiveBench
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper introduces CodeGrad, an iterative loop for LLM-based code generation in which one model writes or revises a program, a second model critiques it along correctness, input-output behavior, efficiency, and completeness, and a formal optimizer accepts a revision only when the writer also produces a natural-language proof that the program satisfies specified invariants. The central claim is that converting the critique into a list of concrete edits — a textual pseudo-gradient — and treating code as a differentiable text variable steers revisions toward solutions that are not just passing tests but formally justified. If correct, the framework would give a practical bridge between LLM flexibility and the verifiability usually associated with formal methods, on exactly the high-stakes problems where unconstrained generation is unreliable. The paper reports gains of up to 27.2% on HumanEval and 40.6% relative on LiveCodeBench V6 over a no-loop baseline, with the largest gains on medium and hard algorithmic problems.

What carries the argument

Two linked objects carry the argument. The textual pseudo-gradient $g^{(t)} = \mathrm{Parse}(F^{(t)})$ converts the critic's structured feedback into an ordered list of concrete edit instructions, playing the role of a gradient on the discrete space of code. The formal gate is the acceptance rule $\text{VERIFY}(P^{(t+1)}, \Pi^{(t+1)}, I) = \text{true}$, where $\Pi^{(t+1)}$ is an LLM-generated natural-language proof that each invariant holds. Jointly they implement the paper's announced constrained optimization: descend along the gradient while ensuring the program satisfies all stated invariants.

What would settle it

Run the same loop but drop the proof requirement — accept every revision that descends along the pseudo-gradient without demanding $\Pi^{(t+1)}$ or $\text{VERIFY}$ — and compare pass@1 on HumanEval and LiveCodeBench V6. If scores stay within a few points, the verification gate is not carrying the improvement; if they collapse, it is. A second check is to log how often VERIFY returns false across the 339 problems; if it never rejects under the two-iteration cap, the gate is inert.

Watch

Extended reading notes

Core claim

On its own terms, the paper's central claim is that a code-generation loop can be organized as a constrained optimization over text in which constraints are enforced by a proof-carrying acceptance rule. Each iteration proposes a candidate $P^{(t+1)}$ that descends along the parsed pseudo-gradient, and the update is kept only if $\text{VERIFY}(P^{(t+1)}, \Pi^{(t+1)}, I) = \text{true}$, where $\Pi^{(t+1)}$ is a natural-language proof generated by the forward model from the invariants $I$. CodeGrad thus approximates projected gradient descent: pseudo-gradient proposals are soft updates and verification is the hard projection. The paper's evidence is a pass@1 comparison on HumanEval, HumanEval+,

Load-bearing premise

The framework's guarantee rests on the premise that a natural-language proof written and then judged by the LLMs is genuine evidence that the program satisfies the invariants; if that premise fails, the verification gate adds nothing beyond the critique loop.

Editorial extensions

If this is right

  • With a fixed two-iteration budget, the loop lifts pass@1 by up to 27% relative on HumanEval and 40.6% relative on LiveCodeBench V6 compared with the same forward model run without a loop.
  • The gains are not uniform: categories where the baseline scores zero (DP, Graph, Greedy) become solvable, and Medium difficulty LiveCodeBench problems improve by over 600% relative.
  • Enabling code execution in the critic helps on HumanEval and HumanEval+ for a strong reviewer but hurts on LiveCodeBench, indicating that sandboxed probes can mislead when problems use stdin/stdout and strict efficiency constraints.
  • The framework's gains track critic capability: a stronger reviewer yields larger improvements on HumanEval, while the lighter reviewer yields smaller gains.
  • Every accepted revision carries a natural-language proof tied to the invariants, which is the paper's stated basis for calling the output formally justified.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: because the acceptance gate is an LLM judging an LLM-generated proof in the reported setup, a direct ablation that deletes the proof requirement while keeping the same critic and pseudo-gradient would isolate how much of the gain comes from the formal step. The paper does not run that ablation, but the setup makes it easy.
  • Beyond the paper: the invariants and pseudo-gradient machinery are not Python-specific, so the same loop should transfer to other structured artifacts — configurations, test suites, or natural-language specifications — with the same proof-carrying acceptance rule.
  • Beyond the paper: with only two iterations allowed, most of the reported gains may come from the first critique; running more iterations would show whether the verification gate's role grows, saturates, or reverses.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 4 minor

Summary. The paper introduces CodeGrad (also called StructuredGrad/FGCG), an iterative LLM-based code-refinement framework. At each iteration a forward LLM proposes a program, a backward LLM critiques it along correctness, I/O, efficiency, and completeness axes, the critique is converted into a textual pseudo-gradient, and a second forward step generates a revised program together with a natural-language proof Π(t+1) that the program satisfies a fixed invariant set I. The update is accepted only if VERIFY(P(t+1), Π(t+1), I) = true. The loop terminates when the backward model reports no violations or after a fixed N=2 iterations. The authors evaluate on HumanEval, HumanEval+, and LiveCodeBench V6, using Qwen2.5Coder-3B as the forward model and Qwen3-1.7B or GPT4.1-mini as the backward model, and report gains of up to 27.2% absolute on HumanEval and 40.6% relative on LiveCodeBench V6 over a forward-only 'Null' baseline.

Significance. If the formal-guarantee claim were substantiated, the paper would describe a meaningful step toward combining LLM code generation with verifiable constraints, and the reported empirical gains would make it a useful reference for the community. The paper also ships a concrete, easy-to-replicate experimental setup, and the +Code ablation (sandboxed execution for the backward model) is an interesting practical finding. However, the central claims as stated are not supported: the verification step is not an external sound procedure, the comparison baseline excludes the direct predecessor TextGrad, and the fixed two-iteration budget makes it impossible to attribute gains to the formal gate. The contribution is therefore closer to an incremental TextGrad-style critique loop than to a framework that produces 'formally justified' code.

major comments (4)
  1. [Section III-B, Eq. (3) and acceptance rule before Eq. (4)] The load-bearing 'rigorous verification' claim is not backed by any specification of VERIFY. The proof Π(t+1) is generated by the same forward LLM used to write the code (Eq. 3), and the acceptance rule evaluates it via an unspecified procedure. No theorem prover, type checker, model checker, or other sound external checker is named; the scare quotes around 'proof' in Section I underline the gap. Consequently Eq. (4)'s 'hard constraints' are implemented as LLM self-assessment of an LLM-written proof. The abstract's claim that the output is 'formally justified' is therefore unsupported. The authors must either identify a sound external verifier, or explicitly restrict the claim to 'critique-based refinement,' which would make the paper's novelty claim much weaker.
  2. [Table I (Section IV-A)] The abstract states that CodeGrad 'outperforms strong baselines,' but Table I only compares CodeGrad configurations against a forward-only Null model. TextGrad, the direct predecessor whose gradient mechanism the paper explicitly builds on (Section II, Eq. 2), is never run. Also missing are other iterative refinement methods such as Reflexion, Self-Debugging, or CODET. Without these comparisons the headline gains cannot be attributed to CodeGrad's specific components, and the contribution relative to existing work is not demonstrated. At minimum, TextGrad must be evaluated under the same forward/backward model combinations and iteration budget.
  3. [Section III-C and Section IV-A] The fixed maximum of N=2 iterations means the formal VERIFY gate can rarely be the deciding factor: most loops terminate by the iteration budget rather than by successful verification. The paper reports no acceptance/rejection logs and no per-iteration success rates, so the reader cannot determine whether the reported improvements come from the verification gate, from the backward critique, or simply from running the loop twice. An ablation that removes the VERIFY gate while keeping the same critic and the same two-iteration budget is essential; without it, the claim that formal verification drives the gains is untestable.
  4. [Tables II and III] The difficulty-level and category analyses contain several statements that are not supported by the data. For example, Table III reports relative increases of 305%, 505%, and 611% for 'Medium' problems, but the underlying base rates are 0.019 or 0.058, and no confidence intervals or sample sizes are given. Table II reports '0.083' for DP and Graph and '0.062' for Greedy, which correspond to fewer than 5 solved problems in a typical LiveCodeBench split; calling these 'successfully solves problems in these areas' overstates the evidence. The paper should report raw counts, standard errors, and the number of problems per category.
minor comments (4)
  1. [Abstract and Section IV-A] The two headline metrics are presented inconsistently: the Abstract says '27% on HumanEval and 41% relative improvement on LiveCodeBench V6,' but Section IV-A reports 27.2% and 40.6%. Also, for LiveCodeBench the best configuration is GPT4.1-mini Base (0.251), while GPT4.1-mini +Code is lower (0.201); the paper should specify which configuration is used for the headline number.
  2. [Section II] The related-work discussion cites TextGrad but does not compare against it, and it incorrectly states 'Textgrad use the model toward a correct solution' — should be 'uses.' There are also typos in Section IV ('lastest'), Section III-B ('V ERIFY'), and the Abstract ('a improvement').
  3. [Section III-A and throughout] The phrase 'treats code as a differentiable variable' is metaphorical; no differentiation or numerical gradient is involved. The authors should either formalize the analogy or clearly state that it is an analogy, otherwise the contribution may be misread as a differentiable-programming method.
  4. [Reproducibility] No code, prompts, or hyperparameter details are released. The prompt templates, the 'gradient format,' and the exact definition of the invariant set I are part of the method's free parameters and are not specified, making it difficult to reproduce or ablate the approach.

Circularity Check

1 steps flagged · score 6.0 of 10

Formal-justification claim is self-referential: the proof Π is written by the same forward LLM that writes the code, and VERIFY is never specified as an external checker, so 'rigorously verified' reduces to the model's own self-assessment.

  1. self definitional [Section III-B (Formal Optimization), Eq. (3) and acceptance rule; cf. Section I scare-quoted 'proof']
    "Π(t+1) = LM fwd(P(t), ∇P(t), I). (3). The update is accepted if VERIFY(P(t+1), Π(t+1), I) = true, else it is discarded. ... Crucially, it requires each revision to have a natural language 'proof' of its correctness."

    The putative evidence of correctness, Π(t+1), is generated by LM_fwd, the same forward model that produces the candidate program P(t+1). The acceptance rule then defines 'formally justified' as passing an uncharacterized VERIFY on that self-generated, natural-language proof. The paper never names an external theorem prover, type checker, model checker, or other sound procedure; with the proof itself placed in scare quotes in Section I, the formal-guarantee claim is operationally equivalent to the model's own assertion that its code satisfies the invariants. The loop therefore certifies itself: the label 'rigorously verified' is a function of the same LM's output, not an independent check.

full rationale

The empirical pass@1 gains in Table I are evaluated against external hidden tests (HumanEval, HumanEval+, LiveCodeBench), so those specific numbers are not circular. The circularity is confined to the paper's stronger, load-bearing claim—that the pipeline yields 'robust and formally justified' code via 'rigorous verification.' As specified in Section III-B, the proof Π is produced by the same LM_fwd that writes the code, and the acceptance gate VERIFY is never defined as an external sound checker; the paper even places 'proof' in scare quotes in Section I. Thus the formal guarantee reduces to self-assessment by construction of Eq. (3) and the acceptance rule. The fixed N=2 budget (Section III-C) further means the verification gate cannot be shown to drive the reported improvements, though that is an attribution problem rather than a circularity. No load-bearing self-citation, uniqueness import, or fitted-input-as-prediction pattern was found. Score 6 reflects partial circularity: the central formal-justification claim is self-referential, while the benchmark improvements remain independent.

Assumptions & free parameters 4 free parameters · 4 assumptions · 2 invented entities

The framework's distinct contribution, formal-gated refinement, rests on an uncharged premise: that an LLM-written natural-language proof judged by an LLM constitutes verification. The performance claims additionally rest on hand-chosen iteration caps and per-benchmark selection of the critic model and code-execution toggle. The one genuinely new entity named in the paper, StructuredGrad, appears only in the abstract and is never defined. No physical or mathematical entity is invented; the 'formal optimizer' is a re-labeling of LLM prompting.

free parameters (4)
  • max_refinement_iterations (N) = 2
    Hand-chosen cap on refinement rounds; no sensitivity analysis, and the natural-language proof gate is rarely reported as the terminating condition.
  • invariant set I = I/O format, completeness, efficiency, Python syntax
    Author-defined, unquantified constraints; 'efficiency' is never measured or formally checked, only asserted in the generated proof.
  • backward model and code-execution flag = Qwen3-1.7B or GPT4.1-mini, with/without +Code
    Selected per benchmark; the abstract's headline numbers use the +Code configuration for both benchmarks even though the non-code GPT4.1-mini is better on LiveCodeBench, so the configuration is effectively tuned to the headline.
  • prompt templates and gradient format = not provided
    The Parse() mapping in Eq. (2), the critic axes, and the VERIFY prompt are unspecified, so the method's core engineering detail is a free choice of the authors.
assumptions (4)
  • ad hoc to paper An LLM-generated natural-language proof, accepted by an LLM-based VERIFY, establishes that the program satisfies the invariants I.
    Central premise of the 'formal optimization' step (Section III-B, Eq. (3)); no external verifier is specified, so the guarantee is the LLM's own judgment.
  • domain assumption The backward model's structured critique F(t) is an accurate estimate of the gradient direction, i.e., following it increases the probability of a correct program.
    The whole refinement loop depends on critic accuracy; the paper reports critic-dependent swings (e.g., Qwen3-1.7B pushes Array pass@1 down from 0.412 to 0.294), so the assumption fails for some critics.
  • domain assumption The forward model can reliably consume textual pseudo-gradients and produce improved programs in one shot.
    Standard assumption of TextGrad-style loops (cited [32]); the paper provides no per-iteration success decomposition to verify gradients cause the gains.
  • domain assumption Pass@1 against HumanEval/HE+/LCB test suites measures the property the paper claims to improve.
    Benchmarks are external and standard (Section III-C); this assumption is reasonable but means 'robust and efficient' claims are only tested as unit-test correctness.
invented entities (2)
  • StructuredGrad
    purpose: Named in the abstract as the system that 'generates mathematically justified code'; never defined or used in the body.
    Appears once in the abstract as a probable leftover of an earlier draft; its undefined presence is a signal of unfinished revision, not a working artifact.
  • Formal optimizer / formal critic
    purpose: Role names for LLM calls that emit and judge natural-language proofs.
    Re-branding of LLM prompting as formal optimization; no actual formal method such as SMT, Lean, Coq, or model checking is invoked anywhere in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement." pith.science (2026). https://pith.science/paper/EHE7RJQG

@misc{pith2026250810059,
  author       = {Pith},
  title        = {Pith review of: CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EHE7RJQG}},
  note         = {Machine review of arXiv:2508.10059}
}
read the original abstract

While Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, they often produce solutions that lack guarantees of correctness, robustness, and efficiency. This limitation is particularly acute in domains requiring strict constraints. CodeGrad introduces a principled framework that integrates rigorous verification techniques directly into an iterative LLM-based generation loop. It uniquely treats code as a differentiable variable, converting structured feedback and mathematical constraints into a textual pseudo-gradient. This gradient guides the model to iteratively refine solutions, ensuring they are not only functional but also robust and mathematically justified. We evaluate CodeGrad on the HumanEval, HumanEval+, and LiveCodeBench benchmarks. Our implementation outperforms strong baselines, achieving an absolute improvement of up to 27% on HumanEval and a 41% relative improvement on the challenging LiveCodeBench V6. StructuredGrad generates mathematically justified code that is robust and efficient, paving the way for reliable AI-assisted software development in high-stakes applications.

Figures

Figures reproduced from arXiv: 2508.10059 by the authors.

Figure 1
Figure 1. Overview of the Formal-Gradient Code Generation loop on the “maximum-subarray” task. First, the forward model proposes an [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. SynthFix: Adaptive Neuro-Symbolic Code Vulnerability Repair

    cs.SE 2026-04 unverdicted novelty 7.0 of 10

    SynthFix adaptively routes LLM code repairs to supervised fine-tuning or symbolic-reward fine-tuning, yielding up to 32% higher exact match on JavaScript and C vulnerability benchmarks.

  2. Overcoming the Weakest-Link Effect in LLM-Driven Program Optimization via Heterogeneous Edit Recombination

    cs.LG 2026-07 conditional novelty 6.0 of 10

    HERO optimizes programs by generating atomic edits without score feedback and selecting the highest-scoring subset of those edits, avoiding the 'weakest-link' failure of accepting or rejecting whole edit bundles.

  3. SynthFix: Adaptive Neuro-Symbolic Code Vulnerability Repair

    cs.SE 2026-04 unverdicted novelty 5.0 of 10

    A router mixes supervised and reward fine-tuning with compiler/security feedback so small code LLMs produce more functionally correct and security-cleared vulnerability patches on three repair benchmarks.

Reference graph

Works this paper leans on

40 extracted references · 20 canonical work pages · cited by 2 Pith papers

  1. [1]

    Intellicode compose: Code generation using transformer,

    A. Svyatkovskiy, S. K. Deng, S. Fu, and N. Sundaresan, “Intellicode compose: Code generation using transformer,” in Proceedings of the 28th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering , 2020, pp. 1433–1443

    work page 2020

  2. [2]

    Programming is hard-or at least it used to be: Educational opportunities and challenges of ai code generation,

    B. A. Becker, P. Denny, J. Finnie-Ansley, A. Luxton-Reilly, J. Prather, and E. A. Santos, “Programming is hard-or at least it used to be: Educational opportunities and challenges of ai code generation,” in Proceedings of the 54th ACM Technical Symposium on Computer Science Education V . 1, 2023, pp. 500–506

    2023

  3. [3]

    Competition- level code generation with alphacode,

    Y . Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. Dal Lago et al. , “Competition- level code generation with alphacode,” Science, vol. 378, no. 6624, pp. 1092–1097, 2022

    2022

  4. [4]

    Llm-based code generation method for golang compiler testing,

    Q. Gu, “Llm-based code generation method for golang compiler testing,” in Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023, pp. 2201–2203

    work page 2023

  5. [5]

    A review on code generation with llms: Application and evaluation,

    J. Wang and Y . Chen, “A review on code generation with llms: Application and evaluation,” in 2023 IEEE International Conference on Medical Artificial Intelligence (MedAI) . IEEE, 2023, pp. 284–289

    2023

  6. [6]

    Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation,

    J. Liu, C. S. Xia, Y . Wang, and L. Zhang, “Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation,” Advances in Neural Information Processing Systems , vol. 36, pp. 21 558–21 572, 2023

    work page 2023

  7. [7]

    Hlspilot: Llm-based high- level synthesis,

    C. Xiong, C. Liu, H. Li, and X. Li, “Hlspilot: Llm-based high- level synthesis,” in Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design , 2024, pp. 1–9

    work page 2024

  8. [8]

    Uncovering llm-generated code: A zero-shot synthetic code detector via code rewrit- ing,

    T. Ye, Y . Du, T. Ma, L. Wu, X. Zhang, S. Ji, and W. Wang, “Uncovering llm-generated code: A zero-shot synthetic code detector via code rewrit- ing,” in Proceedings of the AAAI Conference on Artificial Intelligence , vol. 39, no. 1, 2025, pp. 968–976

    work page 2025

Show all 40 references
  1. [9]

    Methodology for code synthesis evaluation of llms presented by a case study of chatgpt and copilot,

    Z. S ´agodi, I. Siket, and R. Ferenc, “Methodology for code synthesis evaluation of llms presented by a case study of chatgpt and copilot,” Ieee Access, 2024

    2024

  2. [10]

    Policy filtration in rlhf to fine-tune llm for code generation,

    W. Shen and C. Zhang, “Policy filtration in rlhf to fine-tune llm for code generation,” arXiv preprint arXiv:2409.06957 , 2024

    2024 arXiv

  3. [11]

    Rlef: Grounding code llms in execution feedback with reinforcement learning,

    J. Gehring, K. Zheng, J. Copet, V . Mella, Q. Carbonneaux, T. Cohen, and G. Synnaeve, “Rlef: Grounding code llms in execution feedback with reinforcement learning,” arXiv preprint arXiv:2410.02089 , 2024

    2024 arXiv

  4. [12]

    Exploring and evaluating hallucinations in llm-powered code generation,

    F. Liu, Y . Liu, L. Shi, H. Huang, R. Wang, Z. Yang, L. Zhang, Z. Li, and Y . Ma, “Exploring and evaluating hallucinations in llm-powered code generation,” arXiv preprint arXiv:2404.00971 , 2024

    2024

  5. [13]

    Llm hallucinations in practical code generation: 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 generation: Phenomena, mechanism, and mitigation,” Proceedings of the ACM on Software Engineering, vol. 2, no. ISSTA, pp. 481–503, 2025

    2025

  6. [14]

    Llm is like a box of chocolates: the non-determinism of chatgpt in code generation,

    S. Ouyang, J. M. Zhang, M. Harman, and M. Wang, “Llm is like a box of chocolates: the non-determinism of chatgpt in code generation,” arXiv e-prints, pp. arXiv–2308, 2023

    2023

  7. [15]

    Limitations of formal methods and an approach to improvement,

    S. Liu and R. Adams, “Limitations of formal methods and an approach to improvement,” in Proceedings 1995 Asia Pacific Software Engineering Conference. IEEE, 1995, pp. 498–507

    1995

  8. [16]

    Formal methods: Practice and experience,

    J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald, “Formal methods: Practice and experience,” ACM computing surveys (CSUR) , vol. 41, no. 4, pp. 1–36, 2009

    2009

  9. [17]

    Copilot evaluation harness: Evaluating llm-guided software programming,

    A. Agarwal, A. Chan, S. Chandel, J. Jang, S. Miller, R. Z. Moghaddam, Y . Mohylevskyy, N. Sundaresan, and M. Tufano, “Copilot evaluation harness: Evaluating llm-guided software programming,” arXiv preprint arXiv:2402.14261, 2024

    2024 arXiv

  10. [18]

    Llm- based test-driven interactive code generation: User study and empirical evaluation,

    S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, and S. K. Lahiri, “Llm- based test-driven interactive code generation: User study and empirical evaluation,” IEEE Transactions on Software Engineering , 2024

    2024

  11. [19]

    The fusion of large language models and formal methods for trustworthy ai agents: A roadmap,

    Y . Zhang, Y . Cai, X. Zuo, X. Luan, K. Wang, Z. Hou, Y . Zhang, Z. Wei, M. Sun, J. Sun et al., “The fusion of large language models and formal methods for trustworthy ai agents: A roadmap,” arXiv preprint arXiv:2412.06512, 2024

    2024 arXiv

  12. [20]

    From informal to formal–incorporating and evaluating llms on natural language requirements to verifiable formal proofs,

    J. Cao, Y . Lu, M. Li, H. Ma, H. Li, M. He, C. Wen, L. Sun, H. Zhang, S. Qin et al. , “From informal to formal–incorporating and evaluating llms on natural language requirements to verifiable formal proofs,” arXiv preprint arXiv:2501.16207, 2025

    2025 arXiv

  13. [21]

    Apollo: Automated llm and lean collaboration for advanced formal reasoning,

    A. Ospanov, F. Farnia, and R. Yousefzadeh, “Apollo: Automated llm and lean collaboration for advanced formal reasoning,” arXiv preprint arXiv:2505.05758, 2025

    2025

  14. [22]

    Llm-guided formal verification coupled with mutation testing,

    M. Hassan, S. Ahmadi-Pour, K. Qayyum, C. K. Jha, and R. Drechsler, “Llm-guided formal verification coupled with mutation testing,” in 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 2024, pp. 1–2

    2024

  15. [23]

    Dehallucinating large language models using formal methods guided iterative prompting,

    S. Jha, S. K. Jha, P. Lincoln, N. D. Bastian, A. Velasquez, and S. Neema, “Dehallucinating large language models using formal methods guided iterative prompting,” in 2023 IEEE International Conference on Assured Autonomy (ICAA). IEEE, 2023, pp. 149–152

    2023

  16. [24]

    Enhancing reasoning capabilities of llms via principled synthetic logic corpus,

    T. Morishita, G. Morio, A. Yamaguchi, and Y . Sogawa, “Enhancing reasoning capabilities of llms via principled synthetic logic corpus,” Ad- vances in Neural Information Processing Systems , vol. 37, pp. 73 572– 73 604, 2024

    2024

  17. [25]

    Llm reasoners: New evaluation, library, and analysis of step-by-step reasoning with large language models,

    S. Hao, Y . Gu, H. Luo, T. Liu, X. Shao, X. Wang, S. Xie, H. Ma, A. Samavedhi, Q. Gao et al., “Llm reasoners: New evaluation, library, and analysis of step-by-step reasoning with large language models,” arXiv preprint arXiv:2404.05221 , 2024

    2024 arXiv

  18. [26]

    Llm as a mastermind: A survey of strategic reasoning with large language models,

    Y . Zhang, S. Mao, T. Ge, X. Wang, A. de Wynter, Y . Xia, W. Wu, T. Song, M. Lan, and F. Wei, “Llm as a mastermind: A survey of strategic reasoning with large language models,” arXiv preprint arXiv:2404.01230, 2024

    2024 arXiv

  19. [27]

    Isr-llm: Iterative self- refined large language model for long-horizon sequential task planning,

    Z. Zhou, J. Song, K. Yao, Z. Shu, and L. Ma, “Isr-llm: Iterative self- refined large language model for long-horizon sequential task planning,” in 2024 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2024, pp. 2081–2088

    2024

  20. [28]

    To believe or not to believe your llm: Iterative prompting for estimating epistemic uncertainty,

    Y . Abbasi Yadkori, I. Kuzborskij, A. Gy ¨orgy, and C. Szepesvari, “To believe or not to believe your llm: Iterative prompting for estimating epistemic uncertainty,” Advances in Neural Information Processing Systems, vol. 37, pp. 58 077–58 117, 2024

    2024

  21. [29]

    Reflex- ion: Language agents with verbal reinforcement learning,

    N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao, “Reflex- ion: Language agents with verbal reinforcement learning,” Advances in Neural Information Processing Systems , vol. 36, pp. 8634–8652, 2023

    2023

  22. [30]

    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,” Advances in Neural Information Processing Systems, vol. 35, pp. 21 314–21 328, 2022

    2022

  23. [31]

    Codet: Code generation with generated tests,

    B. Chen, F. Zhang, A. Nguyen, D. Zan, Z. Lin, J.-G. Lou, and W. Chen, “Codet: Code generation with generated tests,” arXiv preprint arXiv:2207.10397, 2022

    2022 arXiv

  24. [32]

    Textgrad: Automatic

    M. Yuksekgonul, F. Bianchi, J. Boen, S. Liu, Z. Huang, C. Guestrin, and J. Zou, “Textgrad: Automatic” differentiation” via text,” arXiv preprint arXiv:2406.07496, 2024

    2024 arXiv

  25. [33]

    Formal-llm: Integrating formal language and natural language for controllable llm-based agents,

    Z. Li, W. Hua, H. Wang, H. Zhu, and Y . Zhang, “Formal-llm: Integrating formal language and natural language for controllable llm-based agents,” arXiv preprint arXiv:2402.00798 , 2024

    2024 arXiv

  26. [34]

    Qwen2. 5-coder technical report,

    B. Hui, J. Yang, Z. Cui, J. Yang, D. Liu, L. Zhang, T. Liu, J. Zhang, B. Yu, K. Lu et al. , “Qwen2. 5-coder technical report,” arXiv preprint arXiv:2409.12186, 2024

    2024 arXiv

  27. [35]

    Qwen3 technical report,

    A. Yang, A. Li, B. Yang, B. Zhang, B. Hui, B. Zheng, B. Yu, C. Gao, C. Huang, C. Lv et al. , “Qwen3 technical report,” arXiv preprint arXiv:2505.09388, 2025

    2025 arXiv

  28. [36]

    Introducing GPT-4.1, GPT-4.1 Mini, and GPT-4.1 Nano,

    OpenAI, “Introducing GPT-4.1, GPT-4.1 Mini, and GPT-4.1 Nano,” https://openai.com/index/gpt-4-1/, 2025, accessed: July 7, 2025

    2025

  29. [37]

    Efficient memory management for large language model serving with pagedattention,

    W. Kwon, Z. Li, S. Zhuang, Y . Sheng, L. Zheng, C. H. Yu, J. E. Gonzalez, H. Zhang, and I. Stoica, “Efficient memory management for large language model serving with pagedattention,” in Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles , 2023

    2023

  30. [38]

    Evaluating large language models trained on code,

    M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. de Oliveira Pinto, J. Kaplan, H. Edwards, Y . Burda, N. Joseph, G. Brockman, A. Ray, R. Puri, G. Krueger, M. Petrov, H. Khlaaf, G. Sastry, P. Mishkin, B. Chan, S. Gray, N. Ryder, M. Pavlov, A. Power, L. Kaiser, M. Bavarian, C. Winter,...

    2021

  31. [39]

    Livecodebench: Holistic and contamination free evaluation of large language models for code,

    A. G. W.-D. L. F. Y . T. Z. S. W. A. S.-L. K. S. I. S. Naman Jain, King Han, “Livecodebench: Holistic and contamination free evaluation of large language models for code,” arXiv preprint, 2024

    2024

  32. [40]

    Problemset,

    LeetCode, “Problemset,” https://leetcode.com/problemset/, 2025, ac- cessed: 2025-07-11

    2025

Pith tools

Reviewed August 5, 2026 · model on record in the stance chip above.