CoChat
Sign Up
PreprintCited by 4Software Testing and Debugging TechniquesTeaching and Learning ProgrammingSoftware Engineering Research

Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization

Open access
Orvalho, Pedro, Janota, Mikoláš, Manquinho, Vasco·2025·arXiv
DOI 10.48550/arxiv.2502.07786arXiv 2502.07786
Open this paper in CoChat — free accountOpen PDF

Abstract

Automated Program Repair (APR) for introductory programming assignments (IPAs) is motivated by the large number of student enrollments in programming courses each year. Since providing feedback on IPAs requires substantial time and effort from faculty, personalized feedback often involves suggesting fixes to students' programs. Formal Methods (FM)-based semantic repair approaches, check a program's execution against a test suite or reference solution, are effective but limited. These tools excel at identifying buggy parts but can only fix programs if the correct implementation and the faulty one share the same control flow graph. Conversely, Large Language Models (LLMs) are used for APR but often make extensive instead of minimal rewrites. This leads to more invasive fixes, making it harder for students to learn from their mistakes. In summary, LLMs excel at completing strings, while FM-based fault localization excel at identifying buggy parts of a program. In this paper, we propose a novel approach that combines the strengths of both FM-based fault localization and LLMs, via zero-shot learning, to enhance APR for IPAs. Our method uses MaxSAT-based fault localization to identify buggy parts of a program, then presents the LLM with a program sketch devoid of these buggy statements. This hybrid approach follows a CEGIS loop to iteratively refine the program. We ask the LLM to synthesize the missing parts, which are then checked against a test suite. If the suggested program is incorrect, a counterexample from the test suite is fed back to the LLM. Our experiments show that our counterexample guided approach, using MaxSAT-based bug-free program sketches, significantly improves the repair capabilities of all six evaluated LLMs. This method allows LLMs to repair more programs with smaller fixes, outperforming other configurations and state-of-the-art symbolic program repair tools.

AI snapshot

Written from the paper’s full text.

TL;DR

The paper combines MaxSAT-based fault localization with zero-shot LLM program repair in a CEGIS loop: localize faulty statements, replace them with holes, ask an LLM to synthesize the missing parts, and feed counterexamples from a test suite. On 1,431 incorrect student C programs, this approach lets six open-access LLMs repair more programs and produce smaller fixes than other configurations and symbolic repair baselines.

Key findings

  • On C-PACK-IPAS (1,431 semantically incorrect C programs), all six evaluated LLMs repaired more programs than CLARA (495, 34.6%) and Verifix (91, 6.3%); without reference implementation, the portfolio across all LLMs/configurations fixed 1,013 programs (70.8%), and with reference implementation it fixed 1,190 (83.2%).
  • FL-based sketches and FIXME annotations improved success: Granite fixed 691 programs (48.3%) with Sk_De-TS and 876 (61.2%) with Sk_De-TS-CE-RI; CodeGemma fixed 688 (48.1%) with Sk_De-TS-CE and 739 (51.6%) with Sk_De-TS-CE-RI.
  • Counterexample feedback improved accuracy across configurations, especially for CodeGemma and Llama3; reference implementation increased repair counts but often caused copying—442 of Granite’s 876 Sk_De-TS-CE-RI repairs had TED zero between the reference implementation and the fixed program.
  • For programs CLARA fails due to control-flow issues, Granite with Sk_De-TS fixed 37.0% of cases, while CodeGemma with Sk_De-TS-CE fixed 34.5%.

Methods

  • CEGIS loop: MaxSAT-based fault localization (CFaults) identifies minimal faulty statements; a prompt generator builds a bug-free program sketch replacing faulty statements with `@HOLE@`; the LLM synthesizes missing parts; a Decider checks the program against a test suite; if incorrect, a counterexample is fed back for revised synthesis.
  • Benchmark: C-PACK-IPAS, 1,431 semantically incorrect student C programs that compile but fail at least one test. Six open-access ~7B LLMs were evaluated: Granite, CodeGemma, CodeLlama, Gemma, Llama3, and Phi3, using 4-bit quantization, a 90-second timeout, and 10GB memory.
  • Metrics: number of programs successfully repaired and Tree Edit Distance/distance score for patch quality; baselines were CLARA and Verifix.

Limitations

  • The paper has no dedicated limitations section. It states that LLMs often copy the provided reference implementation rather than minimally repairing, that reference implementation yields more repairs but potentially less efficient fixes, and that counterexamples help some LLMs only in specific configurations.
  • Evident from the text: evaluation is limited to open-access ~7B models with 4-bit quantization, C introductory programs, a 90-second timeout, and no fine-tuning; no human or pedagogical evaluation of the feedback is reported.
  • Evident: the distance score is used to penalize copying or unnecessarily large fixes, but the reported distance-score sums are not monotonic with repair counts, so patch-quality interpretation depends on the metric.

Model-written summary. Check it against the paper before relying on it.

Integrity signals

Registry

DataCite · 10.48550/arxiv.2502.07786

Cites

0 citation errors · 0 not checkable

Statistics

Nothing to recompute.

Claims the paper makes

5 of 32 cited sources checked · 2 supported · 1 flagged · accuracy not yet measured

  • Findingown data
    § Abstract · p. 1

    Our experiments on 1,431 incorrect student programs show that our counterexample guided approach, using MaxSAT-based bug-free program sketches, significantly improves the repair capabilities of all six evaluated LLMs.

    “Our experiments on 1,431 incorrect student programs show that our counterexample guided approach, using MaxSAT-based bug-free program sketches, significantly improves the repair capabilities of all six evaluated LLMS.”
    • Also stated in: § Introduction · p. 2 · boosted
      “Our experiments with 1431 incorrect student programs reveal that our counterexample guided approach, utilizing MaxSAT-based bug-free program sketches, significantly boosts the repair capabilities of all six evaluated LLMS.”
    Quote in the paperSubstantial claim
  • Findingown data
    § Evaluation · p. 5

    VERIFIX repairs 91 programs (6.3%).

    “In comparison, VERIFIX repairs 91 programs (6.3%), reaches the time limit on 0.6%, and fails to repair 1338 programs (93.5%).”
    Quote in the paperSubstantial claim
  • Findingown data
    § Evaluation · p. 5

    CLARA fails to repair 738 programs (54.7%).

    “Within a 90-second time limit, CLARA repairs 495 programs (34.6%), times out without producing a repair on 154 programs (10.8%), and fails to repair 738 programs (54.7%).”
    Quote in the paperSubstantial claim
  • Findingown data
    § Evaluation · p. 5

    CLARA times out without producing a repair on 154 programs (10.8%).

    “Within a 90-second time limit, CLARA repairs 495 programs (34.6%), times out without producing a repair on 154 programs (10.8%), and fails to repair 738 programs (54.7%).”
    Quote in the paperNot a substantial claim
  • Findingown data
    § Evaluation · p. 5

    VERIFIX fails to repair 1338 programs (93.5%).

    “In comparison, VERIFIX repairs 91 programs (6.3%), reaches the time limit on 0.6%, and fails to repair 1338 programs (93.5%).”
    Quote in the paperSubstantial claim
  • May combine two claims. 12
  • Classified as probably not a substantial claim. 14
  • The quote only partly states this claim. 1

  • May combine two claims.

    Premisecitation
    § Evaluation · p. 5

    Both VERIFIX and CLARA require an exact match between control flow graphs and a bijective relationship between variables; otherwise they return a structural mismatch error.

    “Both tools require an exact match between the control flow graphs (e.g., branches, loops) and a bijective relationship between the variables; otherwise, they return a structural mismatch error.”
    Quote in the paperSubstantial claim2 of 2 sources checked
    • cites Ahmed et al. 2022 source

      Section 7 (Evaluation; page unavailable) explicitly distinguishes the tools: Clara requires matching control-flow edges, while Verifix requires matching CFA nodes and can repair some programs whose CFGs differ. Section 4.2 describes a bijective variable alignment for Verifix, but does not establish that Clara requires one. The paper reports structural-match failures, yet contradicts the claim that both tools require exact CFG matches. (LLM, conf=0.88)

      Checked by a reasoning model — may be wrong.

      Experimental — accuracy not yet measured
    • cites Gulwani, Radicek, and Zuleger 2018 source

      The Matching and §4 Matching and Clustering passages say CLARA requires matching control flow and defines program matching using a bijective variable relation. But Matching explicitly allows different branching structures when the looping structure matches, so an exact match of branches is not required. The paper does not establish VERIFIX’s requirements or say either tool returns a ‘structural mismatch error.’ (LLM, conf=0.89)

      Experimental — accuracy not yet measured

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Premisecitation
    § Evaluation · p. 5

    CLARA clusters multiple correct implementations and selects the one that produces the smallest fix when aligned with the buggy program.

    “CLARA clusters multiple correct implementations and selects the one that produces the smallest fix when aligned with the buggy program.”
    Quote in the paperNot a substantial claim1 of 1 sources checked
    • cites Gulwani, Radicek, and Zuleger 2018 source

      In “Constraint-Optimization Local Repairs” (page not specified), the paper says CLARA runs the repair algorithm on each cluster of correct programs and chooses the repair with the lowest syntactic-distance cost. But the claim says it selects one correct implementation; the “Summary” says a repair can combine expressions from multiple correct solutions within a cluster. (LLM, conf=0.87)

      Experimental — accuracy not yet measured

  • Classified as probably not a substantial claim.

    Premisecitation
    § Related Work · p. 7

    Large Language Models trained on code have demonstrated significant effectiveness in generating program fixes.

    “Large Language Models (LLMS) trained on code (LLMCS) have demonstrated significant effectiveness in generating program fixes (Joshi et al. 2023; Xia, Ding, and Zhang 2023; Wei, Xia, and Zhang 2023; Fan et al. 2023; Xia, Wei, and Zhang 2023; Brancas, Manquinho, and Martins 2024).”
    Quote in the paperSubstantial claim2 of 3 sources checked
    • cites Joshi et al. 2023 source
    • cites Xia, Ding, and Zhang 2023 source

      Checked before — its earlier verdict is held back until a new check runs.

    • cites Wei, Xia, and Zhang 2023 source

  • Probably not a substantial claim: may not pass S3 (load-bearing). The quote only partly states this claim.

    Findingnone given
    § Motivation · p. 2

    In the motivation example, VERIFIX returns a compilation error for the program in Listing 1.

    “VERIFIX returns a compilation error.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § Introduction · p. 2

    Our method allows LLMs to repair more programs than other configurations and state-of-the-art symbolic program repair tools.

    “This method enables LLMS to repair more programs and produce superior fixes with smaller patches, outperforming both other configurations and state-of-the-art symbolic program repair tools (Gulwani, Radicek, and Zuleger 2018; Ahmed et al. 2022).”
    • Also stated in: § Introduction · p. 2 · boosted
      “Experiments show that our approach enables all six evaluated LLMS to fix more programs and produce smaller patches than other configurations and symbolic tools.”
    Quote in the paperSubstantial claim0 of 2 sources checked
    • cites Gulwani, Radicek, and Zuleger 2018 source

      Checked before — its earlier verdict is held back until a new check runs.

    • cites Ahmed et al. 2022 source

      Checked before — its earlier verdict is held back until a new check runs.

  • May combine two claims.

    Findingreasoning
    § Evaluation · p. 7

    For other LLMS, counterexamples are beneficial but only in specific configurations.

    “For other LLMS, counterexamples are beneficial but only in specific configurations.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § Evaluation · p. 5

    The portfolio approach, which combines the strengths of all LLMs and configurations without using reference implementation, achieves the highest overall success rate, fixing 70.8% of the programs.

    “The portfolio approach, which combines the strengths of all LLMS and configurations without using reference implementation, achieves the highest overall success rate, fixing 70.8% of the programs.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingreasoning
    § Evaluation · p. 7

    Including a reference implementation allows for more repaired programs but with potentially less efficient fixes.

    “For RQ4, including a reference implementation allows for more repaired programs but with potentially less efficient fixes.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data
    § Conclusion · p. 7

    Our bug-free program sketches significantly improve the repair capabilities of all six evaluated LLMS, enabling them to repair more programs and produce smaller patches compared to other configurations and state-of-the-art symbolic program repair tools.

    “Experiments show that our bug-free program sketches, significantly improves the repair capabilities of all six evaluated LLMS, enabling them to repair more programs and produce smaller patches compared to other configurations and state-of-the-art symbolic program repair tools.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Premisereasoning
    § Introduction · p. 1

    Few-shot learning can lead to larger fixes than necessary, as it is based on a limited number of examples.

    “Nonetheless, few-shot learning can lead to larger fixes than necessary, as it is based on a limited number of examples.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Premisecitation
    § Evaluation · p. 5

    TED computes structural differences between two ASTs by calculating the minimum number of edit operations needed to transform one AST into another.

    “TED computes the structural differences between two Abstract Syntax Trees (ASTS) by calculating the minimum number of edit operations (i.e., insertions, deletions, and substitutions) needed to transform one AST into another.”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites Tai 1979; Zhang and Shasha 1989

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § Counterexample Guided Automated Repair · p. 4

    The syntax used in our prompts is similar to that in other works on LLM-driven program repair.

    “The syntax used in our prompts is similar to that in other works on LLM-driven program repair (Joshi et al. 2023).”
    Quote in the paperNot a substantial claim0 of 1 sources checked
    • cites Joshi et al. 2023 source

      Not checked in the free run.

  • Classified as probably not a substantial claim.

    Premisecitation
    § Experimental Results · p. 5

    CFAULTS is a formula-based fault localization tool that pinpoints bug locations within programs.

    “We used CFAULTS (Orvalho, Janota, and Manquinho 2024b) which is a formula-based FL tool, that pinpoints bug locations within the programs.”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites Orvalho, Janota, and Manquinho 2024b

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § Evaluation · p. 5

    VERIFIX employs MaxSMT to align a buggy program with a reference implementation provided by the lecturer.

    “VERIFIX employs MaxSMT to align a buggy program with a reference implementation provided by the lecturer”
    Quote in the paperNot a substantial claim0 of 1 sources checked
    • cites Ahmed et al. 2022 source

      Checked before — its earlier verdict is held back until a new check runs.

  • Probably not a substantial claim: may not pass S4 (based). May combine two claims.

    Premisereasoning
    § Abstract · p. 1

    LLMs excel at completing strings, while FM-based fault localization excels at identifying buggy parts of a program.

    “In summary, LLMS excel at completing strings, while FM-based fault localization excel at identifying buggy parts of a program.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § Listing 3 Program sketch with holes. · p. 3

    FBFL tools leverage MaxSAT and the theory of Model-Based Diagnosis (MBD).

    “FBFL tools leverage MaxSAT and the theory of Model-Based Diagnosis (MBD) (Reiter 1987; Jose and Majumdar 2011b; Marques-Silva et al. 2015; Ignatiev et al. 2019; Orvalho, Janota, and Manquinho 2024b).”
    Quote in the paperNot a substantial claim0 of 3 sources checked
    • cites Reiter 1987 source
    • cites Jose and Majumdar 2011b

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites Marques-Silva et al. 2015

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • May combine two claims.

    Premisecitation
    § Introduction · p. 1

    Traditional semantic APR techniques based on Formal Methods are often slow and may struggle when the correct implementation diverges significantly from the erroneous one.

    “Traditional semantic APR techniques based on Formal Methods (FM), while providing high-quality fixes, are often slow and may struggle when the correct implementation diverges significantly from the erroneous one (Contractor and Rivero 2022).”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites Contractor and Rivero 2022 source

  • May combine two claims.

    Interpretationown data
    § Introduction · p. 1

    LLMs do not guarantee minimal repairs and typically rewrite most of the student's implementation rather than making minimal adjustments, making their fixes less efficient and harder for students to learn from.

    “LLMS do not guarantee minimal repairs and typically rewrite most of the student's implementation to fix it, rather than making minimal adjustments, making their fixes less efficient and harder for students to learn from.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § Preliminaries · p. 2

    CEGIS is an iterative algorithm commonly used in Program Synthesis and Formal Methods to construct programs or solutions that satisfy a given specification.

    “CEGIS is an iterative algorithm commonly used in Program Synthesis and Formal Methods to construct programs or solutions that satisfy a given specification (Abate et al. 2018; Jha et al. 2010; Solar-Lezama et al. 2005).”
    Quote in the paperNot a substantial claim0 of 3 sources checked
    • cites Abate et al. 2018 source

      Checked before — its earlier verdict is held back until a new check runs.

    • cites Jha et al. 2010 source
    • cites Solar-Lezama et al. 2005 source

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § Listing 4 GRANITE's fix using the program sketch. · p. 3

    FBFL tools enumerate all diagnoses of a MaxSAT formula corresponding to bug locations.

    “Moreover, these FBFL tools enumerate all diagnoses of a MaxSAT formula corresponding to bug locations.”
    Quote in the paperNot a substantial claim0 of 3 sources checked
    • cites Reiter 1987 source
    • cites Jose and Majumdar 2011b

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites Marques-Silva et al. 2015

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § Experimental Results · p. 5

    CFAULTS aggregates all failing test cases into a unified MaxSAT formula.

    “It aggregates all failing test cases into a unified MaxSAT formula.”
    Quote in the paperNot a substantial claim0 of 1 sources checked
    • cites Orvalho, Janota, and Manquinho 2024b

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • May combine two claims.

    Interpretationown data
    § Evaluation · p. 7

    While access to a reference implementation enables GRANITE and other LLMS to repair more programs, it often results in larger changes to the student's program than when no correct implementation is given.

    “This suggests that while access to a reference implementation enables GRANITE and other LLMS to repair more programs, it often results in larger changes to the student's program than when no correct implementation is given.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Premisenone given
    § Related Work · p. 7

    No existing work has explored the use of LLMS guided by formula-based FL.

    “However, to the best of our knowledge, no existing work has explored the use of LLMS guided by formula-based FL.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationown data
    § Conclusion · p. 7

    The interaction between Formal Methods and LLMS yields more accurate and efficient program fixes, enhancing feedback mechanisms in programming education.

    “Therefore, this interaction between Formal Methods and LLMS yields more accurate and efficient program fixes, enhancing feedback mechanisms in programming education.”
    Quote in the paperSubstantial claim
24 of 24

  • The paper relies on this without support.

    LLMs can quickly synthesize the missing parts in a program sketch.

    “Afterwards, we leverage LLMS to quickly synthesize the missing parts in the program sketch.”

  • The paper relies on this without support.

    A counterexample from the test suite can guide LLMs in generating patches that make the synthesized program compliant with the entire test suite.

    “Finally, we use a counterexample from the test suite to guide LLMS in generating patches that make the synthesized program compliant with the entire test suite, thus completing the repair.”

  • The paper relies on this without support.

    Closed-access models like ChatGPT are cost-prohibitive and raise concerns over student data privacy.

    “Firstly, closed-access models like Chat-GPT are cost-prohibitive and raise concerns over student data privacy.”

  • The paper relies on this without support.

    Models with a very large number of parameters (e.g., 70B) need significant computational resources, such as GPUs with higher RAM capacities, and take longer to generate responses, which is unsuitable for a classroom setting.

    “Secondly, models with a very large number of parameters (e.g., 70B) need significant computational resources, such as GPUs with higher RAM capacities, and take longer to generate responses, which is unsuitable for a classroom setting.”
4 of 4

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

Each contradiction between two passages listed here was confirmed by an independent check.

  • CLARA outcome counts omit 44 programs

    Major

    The three reported CLARA outcomes total 1,387 programs, not the 1,431 programs in the evaluation benchmark. If these are the complete outcomes, 44 programs are unaccounted for.

    Reported 1431 · recomputed 1387

  • CLARA failure percentage does not match its count

    Major

    The reported 738 failures are 51.6% of the 1,431-program benchmark, not 54.7%.

    Reported 54.7 · recomputed 51.572327

  • One evaluated model is substantially below the stated parameter size

    Minor

    The model-selection description says only models with approximately 7 billion parameters were used, but it subsequently specifies a 3.8-billion-parameter PHI3 variant.

  • GRANITE is called the leader despite LLAMA3's higher portfolio result

    Minor

    In the configurations without a reference implementation, Table 1 reports 851 repairs (59.5%) for LLAMA3, exceeding GRANITE's 846 (59.1%).

4 of 4

Cites

The publisher hasn’t deposited this paper’s reference list.

Research works printed but not linked: 11

  1. Afzal, A.; Motwani, M.; Stolee, K. T.; Brun, Y.; and Goues, C. L. 2019. SOSRepair: Expressive Semantic Search for Real-World Program Repair. IEEE Trans. Software Eng. , 47(10): 2162-2181.
  2. Aho, A. V.; Sethi, R.; and Ullman, J. D. 1986. Compilers: Principles, Techniques, and Tools . Addison-Wesley series in computer science / World student series edition. AddisonWesley.
  3. Biere, A.; Heule, M.; van Maaren, H.; and Walsh, T., eds. 2009. Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications . IOS Press.
  4. Marques-Silva, J.; Janota, M.; Ignatiev, A.; and Morgado, A. 2015. Efficient Model Based Diagnosis with Maximum Satisfiability. In IJCAI 2015 , 1966-1972. AAAI Press.
  5. Orvalho, P.; Manquinho, V.; and Martins, R. 2023. UpMax: User Partitioning for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023 , volume 271 of LIPIcs , 19:1-19:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
  6. Phung, T.; Cambronero, J.; Gulwani, S.; Kohn, T.; Majumdar, R.; Singla, A.; and Soares, G. 2023. Generating HighPrecision Feedback for Programming Syntax Errors using Large Language Models. In International Conference on Educational Data Mining, EDM . International Educational Data Mining Society.
  7. Xia, C. S.; Wei, Y.; and Zhang, L. 2023. Automated Program Repair in the Era of Large Pre-trained Language Models. In ICSE , 1482-1494. IEEE.
  8. Xia, C. S.; and Zhang, L. 2022. Less training, more repairing please: revisiting automated program repair via zero-shot learning. In ESEC/FSE , 959-971. ACM.
  9. Yasunaga, M.; and Liang, P. 2020. Graph-based, SelfSupervised Program Repair from Diagnostic Feedback. In ICML 2020 , volume 119, 10799-10808. PMLR.
  10. Zhang, J.; Cambronero, J. P.; Gulwani, S.; Le, V.; Piskac, R.; Soares, G.; and Verbruggen, G. 2024. PyDex: Repairing Bugs in Introductory Python Assignments using LLMs. . , 8(OOPSLA): 1100-1124.
  11. Zhang, K.; and Shasha, D. E. 1989. Simple Fast Algorithms for the Editing Distance Between Trees and Related Problems. SIAM J. Comput. , 18(6): 1245-1262.

Cited by

Sorted by citations

Related

Authors
Orvalho, P., Janota, M., & Manquinho, V.
Affiliations
  • University of Oxford (GB)
  • Czech Technical University in Prague (CZ)
  • Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento (PT)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2025
Volume
39
Issue
1
Pages
649-657
ISSN
2159-5399 (ISSN-L)
DOI
10.48550/arxiv.2502.07786
arXiv
2502.07786
OpenAlex
W4409346645
Semantic Scholar
630c6c5fc450b9c97469e4822e0b6d4341fd6755
Cited by
4
References
0
Citations by year
2026: 3 · 2025: 1
FWCI
2.51
Type
conference paper
Language
en
Open access
Licence
Locations
  • Proceedings of the AAAI Conference on Artificial Intelligence (publishedVersion, other-oa)
  • Oxford University Research Archive (ORA) (University of Oxford) (acceptedVersion)
  • arXiv (Cornell University) (submittedVersion, cc-by-nc-sa)
  • AAAI Publications (The Association for the Advancement of Artificial Intelligence (AAAI)) (submittedVersion)
  • arXiv (Cornell University)
Funders
  • Ministerstvo Školství, Mládeže a Tělovýchovy (CZ.02.01.01/ 00/22_008/0004590)
  • Fundação para a Ciência e a Tecnologia (UIDB/50021/2020, PTDC/CCI-COM/2156/2021, 10.54499)
  • H2020 European Research Council (834115)
Topics
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
  • Physical Sciences › Computer Science › Computer Science Applications › Teaching and Learning Programming
  • Physical Sciences › Computer Science › Information Systems › Software Engineering Research
Keywords
automated program repair, counterexample-guided inductive synthesis, zero-shot learning, large language models, student programming errors

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Claims read by deepseek-v4.1-flash under definition version 3 (extract-v3) on 2026-11-05.

Classified by jev-1.13-20260917 (gold-guideline-v0.2) on 2026-11-05.

Cited sources are checked by gpt-6-sol.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review