Pith. sign in

REVIEW 4 major objections 4 minor 34 references

Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs

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

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

Pith's one-line read The paper claims that arithmetic bugs in Dafny programs can be repaired using the formal specification as the only oracle, with Hoare-logic checks locating the true line in 89.7% of cases and GPT-4o mini yielding machine-checked fixes for…

desk verdict Worth engaging: a real Dafny APR tool with verifier-checked patches, but the headline repair rate is probably inflated by benchmark contamination. read the letter →

arxiv 2507.03659 v3 pith:EFCA7MWC submitted 2025-07-04 cs.SE cs.PL

Valentina Wu , Alexandra Mendes , Alexandre Abreu This is my paper · ORCID
classification cs.SEcs.PL
keywords automatedprogramrepairfaultlocalizationDafnyHoarelogiclargelanguagemodelsformalverificationBencharithmeticbugs
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

This paper claims that a Dafny program's formal specification can serve as the sole correctness oracle for automated repair, replacing the test suites that most program-repair tools depend on. Its pipeline first runs a static Hoare-logic analysis that computes the logical state after each statement, encodes the required entailment as a Dafny lemma, and lets the Dafny verifier decide whether the statement's state implies the specification; rejected lemmas mark suspicious lines. An LLM is then prompted to rewrite each suspicious line, and a candidate fix is accepted only if the whole program re-verifies. On 3,104 mutated programs built from DafnyBench, the localization step put the true buggy line on its list 89.7% of the time, and GPT-4o mini produced a verified patch for 74.18% of the programs, ahead of Llama 3, Mistral 7B, and Llemma 7B. If those numbers hold on unseen code, contracts rather than test suites could drive repair pipelines whose every accepted patch carries a machine-checked correctness guarantee.

What carries the argument

The carrying mechanism is entailment checking by lemma construction. At each return point and loop boundary the tool computes the post-state from the Hoare rules for the statement, forms the implication (current state implies specification) whose failure would expose a bug, and encodes that implication as a Dafny lemma whose requires clause is the state and whose ensures clause is the expected property. Because the lemma is itself a Dafny program, the built-in Z3-based verifier decides it for free; a lemma the verifier rejects marks the associated statement's state as inconsistent with the contract, which is both the fault signal and the explanation. The second half of the mechanism is prompt-based patch synthesis constrained by the verifier as a hard filter: each LLM candidate is inserted and the whole method must re-verify, so hallucinated or semantically wrong fixes are discarded automatically, with at most three queries per suspicious line.

What would settle it

Construct a fresh corpus of Dafny methods written after the chosen model's training cutoff (or never published), apply the same four mutation strategies, and rerun the pipeline; if the verified-repair rate drops well below 74%, the headline number is largely memorization. An independent check would run the tool on genuine arithmetic-bug commits from Dafny development history, where the correct fix comes from the developer rather than from a mutation, and compare localization and repair rates.

Watch

Extended reading notes

Core claim

The paper's central claim is that specification-guided localization plus LLM-generated patches forms a working repair loop for arithmetic bugs in Dafny, under the assumptions that each program contains a single bug and that the specification is correct. The localization component translates Hoare-logic entailments into Dafny lemmas and offloads the entailment checks to the Dafny verifier, so a statement whose state fails to imply the specification is flagged and ranked as suspicious. The repair component marks the buggy line with a comment, prompts an LLM to return only the corrected line, inserts the candidate, and re-runs the verifier, allowing three attempts per line before moving on. On the mutated DafnyBench corpus, GPT-4o mini produced verified patches for 71.59% of the hints-removed mutations and 74.71% of the ground-truth mutations with an average of 1.14 attempts per success, while Llama 3 (about 47%), Mistral 7B (about 46%), and Llemma 7B (below 5%) lagged; in 95.33% of accepted repairs the patch modified a line the localization step had flagged.

Load-bearing premise

The load-bearing premise is that artificially mutated bugs in public, already-verified DafnyBench programs stand in for real arithmetic bugs the LLM cannot trivially solve from memory — a premise the paper itself flags in its limitations, since the correct programs predate the models' training, so the reported repair rates may partly reflect memorized fixes rather than specification-driven reasoning.

Editorial extensions

If this is right

  • Automated repair for verification-aware languages need not depend on test suites: the specification acts as the oracle, and every accepted patch is verified, not merely test-passing.
  • LLM effort can concentrate on a short ranked list of suspect statements, because the static localization pass places the true buggy line on that list for 89.7% of mutated programs.
  • Most repairs succeed on the first attempt (81.09% on hints-removed, 77.40% on ground-truth), showing that prompt design, with a marked buggy line and an instruction to return only the fixed line, is a decisive factor.
  • LLM choice matters more than raw mathematical aptitude on this task: GPT-4o mini exceeded 70% repair success while the math-specialized Llemma 7B stayed below 5%.
  • A useful patch can still be produced when localization misses the true line, since the LLM sometimes rewrites the surrounding block.

Reading between the lines

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

  • Because the benchmark programs and their correct versions are public and predate the models' training, the 74.18% figure is best read as an upper bound on transfer performance; a replication on programs written after the models' cutoff would separate memorized fixes from specification-driven repair.
  • Under the paper's own numbers, only 80.78% of accepted ground-truth patches exactly match the original correct line, so about one in five verified repairs reaches the specification by a different route; that gap measures how much the contracts under-determine the fix, and it would widen or shrink as post-conditions are weakened or strengthened.
  • The localization gap the authors report on while loops follows from using partial-correctness entailments, so extending the lemma encoding to decreases clauses and total-correctness rules is the natural next step toward handling termination bugs, which the tool currently misses.
  • Since the machinery is language-level Hoare logic plus an SMT-backed verifier, the same loop should port to other contract-equipped languages such as F* or Why3, though the paper demonstrates it only in Dafny.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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 manuscript describes an automated program repair tool for Dafny that targets arithmetic bugs. It localizes faults statically by encoding Hoare-logic entailments as Dafny lemmas and checking them with the Dafny verifier; it then asks one of four LLMs (GPT-4o mini, Llama 3, Mistral 7B, Llemma 7B) for a replacement of each suspicious line, and accepts only patches that make the program verify. The evaluation mutates verified DafnyBench programs with arithmetic operators and reports 89.7% fault localization success and 74.18% repair success with GPT-4o mini, with all accepted patches verified by Dafny. The authors explicitly acknowledge that the LLM may have seen the correct code during training.

Significance. The approach is well-motivated and the use of formal specifications as an oracle is a valuable alternative to test-based APR. The artifact is public, the pipeline is reproducible, and Dafny verification provides a strong internal correctness check on every accepted patch. The four-model comparison is useful. However, the headline repair rate is not yet an unbiased estimate of performance on unseen Dafny bugs: the benchmark programs are public and pre-date GPT-4o mini, so the reported numbers may reflect memorization rather than specification-guided reasoning. The paper's central contribution would be convincing only after contamination-controlled experiments and stronger localization metrics.

major comments (4)
  1. [6.2 (Limitations)] The acknowledged training-data contamination is not addressed by the statement that 'the buggy versions were created by us.' Because the correct DafnyBench programs are public GitHub code collected up to the end of 2023 and GPT-4o mini was trained later, the model can recall the original line once the prompt marks a mutated line with '//buggy line'. The reported 80.78% exact-match-to-original rate for ground_truth is consistent with this alternative explanation. Please add a contamination control, e.g., repair on Dafny programs written after the model's training cutoff or on programs the authors create and do not publish until after evaluation, and report verified-but-not-exact-match repairs separately.
  2. [6.2 (Fault localization metrics)] The 'success rate' of fault localization is defined as the original buggy line being contained in the suspicious-line list, but the paper also reports that about 50% of lines are flagged in hints_removed and about 70% in ground_truth, with many programs fully flagged. Under that metric, a baseline that flags every line would already score 100%, so the 89.7% coverage figure is not evidence that the Hoare-logic localization is precise. Report precision, mean rank of the buggy line, or the percentage of lines flagged for successful cases, and compare with a random or all-lines baseline.
  3. [6.1 (Dataset and mutation)] The evaluation does not state how many of the 2657 ground_truth and 477 hints_removed mutants actually fail verification before repair. The mutations are only 'intended' to break verification; if some mutants still verify, they should not be counted as repair successes, since no bug exists to repair. Please report the number of verification-failing mutants per dataset and per mutation operator, and confirm that the repair-success denominator includes only mutants that fail Dafny verification.
  4. [4 and 6 (Ablation)] The paper does not include a baseline or ablation showing the contribution of the specification-guided fault localization to the repair outcome. To attribute the 74.18% result to the proposed pipeline rather than to the LLM's general ability to fix a marked line, report repair success when the LLM is prompted with the same marked buggy line but without the Hoare-logic suspicious-line ranking (or with a random ranking). This also helps separate memorization from the formal reasoning component.
minor comments (4)
  1. [Abstract] The abstract in the submission header says 89.6% fault localization coverage, while the full-text abstract and Section 6.2 report 89.7%; please make these numbers consistent.
  2. [Section 6.2] The phrase 'average coverage of suspicious lines' should be defined precisely: is it the mean fraction of flagged lines per program, and is it weighted by program length? Without this definition, the difference between 50% and 70% is hard to interpret.
  3. [Listing 1.2] Listing 1.2 is described as illustrating Hoare logic rules, but the listing is a code comment rather than an actual Dafny lemma encoding; a small concrete lemma example would make the localization mechanism easier to follow.
  4. [Table 2] The caption says 'for all 447 and 2657 hints_removed and ground_truth Mutations,' but the reported aggregate repair rate of 74.18% does not follow directly from the two per-dataset values in the table (71.59% and 74.71%); please show the weighted calculation or clarify the aggregate formula.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: repair success is measured by an external verifier against independent DafnyBench specifications.

full rationale

The paper's claimed chain—localize via Hoare-logic entailments checked by the Dafny verifier, synthesize candidate fixes with an LLM, and accept only patches that re-verify against the original DafnyBench specifications—does not reduce to its inputs by construction. Fault localization and repair are both scored against an external oracle (the Dafny verifier and the public DafnyBench contracts), not against quantities fitted in the paper. The headline numbers (89.7% fault localization coverage, 74.18% repair success with GPT-4o mini) are empirical measurements on mutated programs, and the paper separately reports the 80.78% exact-match rate against original correct lines rather than relabeling it as the repair criterion. The self-citations (e.g., Abreu et al. 2023; Silva et al. 2024; Carreira et al. 2025) appear as related-work context and are not used to justify the central result. The acknowledged risk that LLM training data contains the correct DafnyBench programs is an external-validity threat, not a circularity: accepting a patch only when Dafny verifies it is the stated repair criterion, and the specifications come from an independent public benchmark. No equation makes a predicted outcome equal to a fitted input, and no load-bearing claim is justified solely by a self-referential citation. Therefore no circular step is exhibited.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The reported percentages depend on several hand-chosen thresholds and on the public benchmark used for evaluation. No new physical or mathematical entities are introduced; the central claim is an empirical tool evaluation, so the ledger records the experimental choices that shape the numbers.

free parameters (3)
  • Mutation coefficient range = [-c, +c]
    Hand-chosen range for coefficient modification mutations; it determines the difficulty of the injected bugs and therefore shapes the reported repair success rates.
  • Verifier timeout = 20 seconds
    Hand-chosen limit; lemma checks that time out are counted as failures, directly affecting the fault localization and repair metrics.
  • LLM attempts per suspicious line = 3
    Hand-chosen cap on queries per line; allowing more attempts would likely raise the repair success rate, so the number is a free experimental choice.
assumptions (4)
  • domain assumption Formal specifications are correct and complete oracles
    Stated in Section 4 and in Limitations; the approach only repairs code, never specifications, and assumes the specification captures the intended behavior.
  • ad hoc to paper Each program contains exactly one bug
    Stated in Section 4; real programs can have multiple interacting faults, so this assumption limits the generality of the tool.
  • domain assumption Partial correctness reasoning suffices for loop-based programs
    Section 6.2 reports termination reasoning gaps; while loops with decreases clauses are not fully modeled, causing missed bugs in the fault localization phase.
  • standard math Dafny verifier (Boogie/Z3) is sound
    Used for lemma checks and patch validation; the paper relies on Dafny's verification results as ground truth for success and failure.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs." pith.science (2026). https://pith.science/paper/EFCA7MWC

@misc{pith2026250703659,
  author       = {Pith},
  title        = {Pith review of: Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EFCA7MWC}},
  note         = {Machine review of arXiv:2507.03659}
}
read the original abstract

Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications - including pre-conditions, post-conditions, and invariants - as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs. Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%. These results highlight the potential of combining formal reasoning with LLM-based program synthesis for automated program repair.

Figures

Figures reproduced from arXiv: 2507.03659 by the authors.

Figure 1
Figure 1. Overview of the Solution Pipeline The tool receives a buggy Dafny program and its corresponding specification. It first identifies a ranked list of suspicious lines using static analysis. For each [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 33 canonical work pages

  1. [1]

    In: 2023 38th IEEE/ACM Int

    Abreu, A., Macedo, N., Mendes, A.: Exploring Automatic Specification Repair in Dafny Programs. In: 2023 38th IEEE/ACM Int. Conference on Automated Soft- ware Engineering Workshops, ASEW. pp. 105–112. IEEE ACM International Con- ference on Automated Software Engineering, IEEE COMPUTER SOC (2023)

    work page 2023

  2. [2]

    In: Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION

    Abreu, R., Zoeteweij, P., van Gemund, A.J.: On the Accuracy of Spectrum-based Fault Localization. In: Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION. pp. 89–98 (Sep 2007)

    work page 2007

  3. [3]

    In: 23rd Int

    Carreira, C., Silva, Á., Abreu, A., Mendes, A.: Can large language models help students prove software correctness? An experimental study with Dafny. In: 23rd Int. Conf. on Software Engineering and Formal Methods (SEFM) (2025)

    work page 2025

  4. [4]

    Feng, Z., Guo, D., Tang, D., Duan, N., Feng, X., Gong, M., Shou, L., Qin, B., Liu, T., Jiang, D., Zhou, M.: CodeBERT: A Pre-Trained Model for Programming and Natural Languages (Sep 2020)

    work page 2020

  5. [5]

    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (Oct 1969)

    work page 1969

  6. [6]

    In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design

    Könighofer, R., Bloem, R.: Automated error localization and correction for impera- tive programs. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. pp. 91–100. FMCAD Inc, Austin, Texas (Oct 2011)

    work page 2011

  7. [7]

    IEEE Transactions on Software Engineering38(1), 54–72 (Jan 2012)

    Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: GenProg: A Generic Method for Automatic Software Repair. IEEE Transactions on Software Engineering38(1), 54–72 (Jan 2012)

    work page 2012

  8. [8]

    ACM62(12), 56–65 (Nov 2019)

    LeGoues,C.,Pradel,M.,Roychoudhury,A.:Automatedprogramrepair.Commun. ACM62(12), 56–65 (Nov 2019)

    work page 2019

Show all 34 references
  1. [9]

    IEEE Software38(4), 22–27 (Jul 2021)

    Le Goues, C., Pradel, M., Roychoudhury, A., Chandra, S.: Automatic Program Repair. IEEE Software38(4), 22–27 (Jul 2021)

    2021

  2. [10]

    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning. pp. 348–370. Springer (2010)

    2010

  3. [11]

    Electron

    Leino, K.R.M., Wüstholz, V.: The Dafny Integrated Development Environment. Electron. Proc. Theor. Comput. Sci.149, 3–15 (Apr 2014)

    2014

  4. [12]

    arXiv preprint arXiv:2406.08467 (2024)

    Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M.R.H., Amin, N., Tegmark, M.: Dafnybench: A benchmark for formal software verification. arXiv preprint arXiv:2406.08467 (2024)

    2024 arXiv

  5. [13]

    Prentice Hall Upper Saddle River (2002)

    Meyer, B.: Design by contract. Prentice Hall Upper Saddle River (2002)

    2002

  6. [14]

    Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng.1(FSE), 812–835 (Jul 2024)

    2024

  7. [15]

    Technical Report hal-01956501, HAL Archives Ouvertes (2018)

    Monperrus, M.: The living review on automated program repair. Technical Report hal-01956501, HAL Archives Ouvertes (2018)

    2018

  8. [16]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Sys- tems. pp. 337–340. Springer, Berlin, Heidelberg (2008)

    2008

  9. [17]

    IEEE Software30(3), 50–57 (May 2013)

    Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B.: Testing or Formal Ver- ification: DO-178C Alternatives and Industrial Experience. IEEE Software30(3), 50–57 (May 2013)

    2013

  10. [18]

    Mugnier, E., Gonzalez, E.A., Polikarpova, N., Jhala, R., Yuanyuan, Z.: Laurel: Un- blocking automated verification with large language models. Proc. ACM Program. Lang.9(OOPSLA1) (Apr 2025) 18 V. Wu et al

    2025

  11. [19]

    ACM Trans

    Naveed, H., Khan, A.U., Qiu, S., Saqib, M., Anwar, S., Usman, M., Akhtar, N., Barnes, N., Mian, A.: A comprehensive overview of Large Language Models. ACM Trans. Intell. Syst. Technol. (Jun 2025)

    2025

  12. [20]

    In: 2013 35th International Conference on Software Engi- neering (ICSE)

    Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: SemFix: Program repair via semantic analysis. In: 2013 35th International Conference on Software Engi- neering (ICSE). pp. 772–781 (May 2013)

    2013

  13. [21]

    In: Enea, C., Piskac, R

    Nguyen, T.T., Ta, Q.T., Chin, W.N.: Automatic Program Repair Using Formal Verification and Expression Templates. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 70–91. Springer International Publishing, Cham (2019)

    2019

  14. [22]

    In: Gnesi, S., Rensink, A

    Pei, Y., Furia, C.A., Nordio, M., Meyer, B.: Automatic Program Repair by Fixing Contracts. In: Gnesi, S., Rensink, A. (eds.) Fundamental Approaches to Software Engineering. pp. 246–260. Springer, Berlin, Heidelberg (2014)

    2014

  15. [23]

    In: 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)

    Pei, Y., Wei, Y., Furia, C.A., Nordio, M., Meyer, B.: Code-based automated pro- gram fixing. In: 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011). pp. 392–395 (Nov 2011)

    2011

  16. [24]

    Poesia, G., Loughridge, C., Amin, N.: dafny-annotator: AI-Assisted Verification of Dafny Programs (Nov 2024)

    2024

  17. [25]

    In: Proc

    Prenner, J.A., Babii, H., Robbes, R.: Can OpenAI’s codex fix bugs? an evalua- tion on QuixBugs. In: Proc. of the Third International Workshop on Automated Program Repair. pp. 69–75. APR ’22, ACM, New York, NY, USA (Oct 2022)

    2022

  18. [26]

    In: Proceedings of the 2024 IEEE/ACM 12th Int

    Silva, A.F., Mendes, A., Ferreira, J.F.: Leveraging Large Language Models to Boost Dafny’s Developers Productivity. In: Proceedings of the 2024 IEEE/ACM 12th Int. Conference on Formal Methods in Software Engineering. pp. 138–142. FormaliSE ’24, Association for Computing Machin...

    2024

  19. [27]

    In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering

    Smith, E.K., Barr, E.T., Le Goues, C., Brun, Y.: Is the cure worse than the disease? overfitting in automated program repair. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering. pp. 532–543. ESEC/FSE 2015, Association for Computing Machinery,...

    2015

  20. [28]

    In: Avni, G., Giacobbe, M., Johnson, T.T., Katz, G., Lukina, A., Narodytska, N., Schilling, C

    Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Closed-Loop Verifiable Code Generation. In: Avni, G., Giacobbe, M., Johnson, T.T., Katz, G., Lukina, A., Narodytska, N., Schilling, C. (eds.) AI Verification. pp. 134–155. Springer Nature Switzerland, Cham (2024)

    2024

  21. [29]

    In: Proceedings of the 19th international symposium on Software testing and analysis

    Wei, Y., Pei, Y., Furia, C.A., Silva, L.S., Buchholz, S., Meyer, B., Zeller, A.: Auto- mated fixing of programs with contracts. In: Proceedings of the 19th international symposium on Software testing and analysis. pp. 61–72. ISSTA ’10, Association for Computing Machinery, New ...

    2010

  22. [30]

    IEEE Transactions on Reliability63(1), 290–308 (Mar 2014)

    Wong, W.E., Debroy, V., Gao, R., Li, Y.: The DStar Method for Effective Software Fault Localization. IEEE Transactions on Reliability63(1), 290–308 (Mar 2014)

    2014

  23. [31]

    IEEE Trans

    Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A Survey on Software Fault Localization. IEEE Trans. on Software Engineering42(8), 707–740 (Aug 2016)

    2016

  24. [32]

    In: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)

    Xia, C.S., Wei, Y., Zhang, L.: Automated Program Repair in the Era of Large Pre-trained Language Models. In: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). pp. 1482–1494 (May 2023)

    2023

  25. [33]

    In: Proc

    Xia, C.S., Zhang, L.: Less training, more repairing please: revisiting automated program repair via zero-shot learning. In: Proc. of the 30th ACM Joint European Software Engineering Conf. and Symposium on the Foundations of Software Engi- neering. pp. 959–971. ESEC/FSE 2022, A...

    2022

  26. [34]

    ACM Trans

    Zhao, H., Chen, H., Yang, F., Liu, N., Deng, H., Cai, H., Wang, S., Yin, D., Du, M.: Explainability for Large Language Models: A Survey. ACM Trans. Intell. Syst. Technol.15(2), 20:1–20:38 (Feb 2024)

    2024

Pith tools

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