ai-research-survey

scan.json (25634B)

---

 {
   "paper": {
     "title": "Automated Repair of AI Code with Large Language Models and Formal Verification",
     "authors": [
       "Yiannis Charalambous",
       "Edoardo Manino",
       "Lucas C. Cordeiro"
     ],
     "year": 2024,
     "venue": "arXiv preprint",
     "arxiv_id": "2405.08848"
   },
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": true,
         "justification": "The paper explicitly states 'This report is to be considered as the official documentation of the public software repository at https://github.com/emanino/plain_c_nn_benchmark' and also references a staging repository at https://github.com/Yiannis128/plain_c_nn_benchmark."
       },
       "data_released": {
         "applies": true,
         "answer": true,
         "justification": "The NeuroCodeBench dataset is publicly available (part of SV-COMP since November 2023), and the expanded dataset is generated via the released code pipeline. The GitHub repositories contain the benchmark and mutation pipeline."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper mentions hardware specs (Intel Xeon E5-2620 v4, 198 GB RAM) and ESBMC version (v7.4.0), ESBMC-AI version (0.5.0rc4), but does not provide a requirements.txt, Dockerfile, or detailed environment specification with library versions sufficient to recreate the full environment."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "The paper describes its methodology but does not provide step-by-step reproduction instructions. There is no README with commands to run, no 'Reproducing Results' section, and no explicit scripts to replicate the main experiments."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "Results are reported as point estimates (percentages in tables and figures) without confidence intervals or error bars. Box plots show distributions but no formal confidence intervals are given for the main repair rate claims."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "The paper makes comparative claims (e.g., 'persona prompts yield a higher percentage', 'Forward History performed best') based solely on comparing raw percentages without any statistical significance tests."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": false,
         "justification": "No formal effect sizes (Cohen's d, odds ratios, etc.) are reported. The paper reports raw percentages (e.g., 18% for single-iteration, ~25% for iterative) but without baseline context or standardized effect size measures."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "Each experiment uses 100 random samples from the dataset but there is no justification for why 100 was chosen and no power analysis. Given that repair rates are often below 10%, 100 samples may be insufficient for reliable comparisons."
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "Results appear to be from single runs per configuration. There is no mention of multiple experimental runs, standard deviations, or variance across repeated experiments. The box plots show distributions of scores within a single run, not across multiple runs."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": true,
         "justification": "The paper includes the 'old ESBMC-AI prompt' from prior work (Charalambous et al. 2023) as a baseline, and compares simple prompts, persona prompts, and various configurations against each other."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": false,
         "justification": "The only baseline is the authors' own prior prompt (ESBMC-AI from 2023). No comparison is made against other contemporary automated program repair tools or approaches from the literature (e.g., other LLM-based APR systems)."
       },
       "ablation_study": {
         "applies": true,
         "answer": true,
         "justification": "The paper systematically varies prompt components: source code format (contextual vs. one-line), verifier feedback (none, before, after), prompt style (simple, persona, old), roles (6 different roles), backtick presence, and history format (LSO, Forward, Reverse). These function as ablations showing which components matter."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": true,
         "justification": "Four metrics of increasing difficulty are used: syntax (C/C++ detection score), relevance (string match), compilation rate, and verification rate (Section 4.2)."
       },
       "human_evaluation": {
         "applies": true,
         "answer": false,
         "justification": "The paper evaluates repair quality entirely through automated metrics (C/C++ detection, string matching, compilation, ESBMC verification). No human evaluation of patch quality, correctness beyond verification, or semantic appropriateness is included."
       },
       "held_out_test_set": {
         "applies": true,
         "answer": false,
         "justification": "The paper samples 100 random examples from the dataset for experiments but does not describe a formal train/test split or held-out test set. The same 100 samples appear to be used across experiments."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Results are broken down by prompt template, source code strategy (contextual vs. one-line), verifier feedback type, persona role, temperature, and message history format. Figure 4 breaks down ESBMC results by neural network category."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "The paper discusses why contextual patches fail (LLM skips code portions), why compilation rates are low, why verifier feedback hurts performance, and identifies the 'Reverse History' approach as performing poorly. The 'Lessons Learned' sections discuss failure modes."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "Several negative results are reported: verifier feedback makes performance worse (Section 4.2), contextual strategy yields very low compilation rates (~1%), Reverse History performs worst, the 'Dog' persona performs comparably to expert roles, and the overall best repair rate is still only ~25%."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract claims are relatively modest: expanding NeuroCodeBench to 81k programs (supported in Section 3), verifying memory safety with ESBMC (supported in Section 3.3), and comparing prompt engineering techniques (supported in Sections 4 and 5). No unsupported claims in the abstract."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": false,
         "justification": "The paper makes causal claims like 'persona prompts yield a higher percentage of C-like LLM outputs' and 'providing feedback from a verifier about the nature of the vulnerability makes the performance worse' without controlling for confounds or running significance tests. With only 100 samples and no repeated runs, observed differences could be noise."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": false,
         "justification": "The paper tests only GPT-3.5-Turbo on AI C code (neural network implementations) but makes broad claims about 'large language models' and 'prompt engineering techniques' in general. The title says 'Large Language Models' (plural) though only one is tested. The conclusion acknowledges the need to test other LLMs, but the body text often generalizes beyond what the single-model evidence supports."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not systematically discuss alternative explanations. For example, the finding that verifier feedback hurts performance could have multiple explanations (prompt length, confusion from technical output, etc.) but only speculation is offered. The anomalous 'Dog' persona result is not explored."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": true,
         "justification": "Section 4.2 specifies 'GPT-3.5-Turbo was used as the LLM of choice, specifically gpt-3.5-turbo-0125' — this is a specific model version with a snapshot identifier."
       },
       "prompts_provided": {
         "applies": true,
         "answer": true,
         "justification": "Full prompt templates are provided in Listings 1-7 and the modified templates 9-2 and 11-2. While they use placeholders ({source}, {esbmc}, {role}), the fill values are described: specific roles are listed, and source/ESBMC formats are defined. The actual prompt text structure is fully provided."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": true,
         "justification": "Temperature is stated as 1.0 (default) for Section 4 experiments, and temperatures 0.0, 0.4, 0.7, 1.0, 1.3 are explored in Section 5. The paper states 'no defaults were changed' for the initial experiments."
       },
       "scaffolding_described": {
         "applies": true,
         "answer": true,
         "justification": "The iterative repair scaffold is described in detail in Section 5.1 with Algorithm 1, including the loop structure, message history formats (LSO, Forward, Reverse), the verification feedback loop, and the maximum attempts (5). Figures 5, 9, and 10 provide visual diagrams."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "Section 3 describes the full pipeline: building base samples from NeuroCodeBench (505 samples), generating mutation patches with Mull, expanding to 81,129 samples, and classifying with ESBMC. The data augmentation process is documented with numbers at each stage."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": false,
         "justification": "There is no dedicated 'Limitations' or 'Threats to Validity' section. The 'Lessons Learned' subsections (3.4, 4.5, 5.4) discuss some findings but are not structured as limitations discussions. Section 6 (Conclusions and Future Work) briefly mentions testing other LLMs but does not substantively discuss limitations."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": false,
         "justification": "No specific threats to validity are discussed. The paper does not address internal validity (e.g., random sampling of 100 examples, single LLM), construct validity (e.g., whether ESBMC verification truly captures repair quality), or external validity (e.g., generalizability beyond AI C code)."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not explicitly state what the results do NOT show. While it mentions plans to test other LLMs in the future, it does not provide explicit scope boundaries like 'these results apply only to GPT-3.5-Turbo on memory safety bugs in neural network C code.'"
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": false,
         "justification": "While the code repositories are linked, the actual experimental results (the 14,400 LLM outputs, ESBMC verification results, etc.) are not made available as raw data files for independent verification."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "Section 3 thoroughly describes how the dataset was created: starting from NeuroCodeBench, using Mull for mutation, expanding from 505 to 81,129 samples, and classifying with ESBMC. The 100 random sample selection for experiments is mentioned."
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved. The study uses automated benchmarks and LLM APIs."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "The full pipeline from NeuroCodeBench through mutation with Mull to ESBMC classification is documented in Section 3 with Figure 3 providing a visual overview. Numbers at each stage are provided (505 base samples, 81,129 after mutation, breakdown by category in Figure 4a)."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": false,
         "justification": "No funding information or acknowledgments section is present in the paper. There is no mention of grants, sponsors, or funding agencies."
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Author affiliations are clearly listed: University of Manchester and Federal University of Amazonas. The paper evaluates GPT-3.5-Turbo and ESBMC; the authors are ESBMC developers (Cordeiro is a known ESBMC author), which is relevant but affiliations are disclosed."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": false,
         "justification": "No funding is disclosed, so independence cannot be assessed. Additionally, the authors are the developers of ESBMC and ESBMC-AI, the tools being evaluated, which represents a potential conflict of interest that is not acknowledged."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests statement is present. The authors evaluate their own tool (ESBMC-AI) without disclosing whether they have financial interests related to it."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not state the training data cutoff for GPT-3.5-Turbo. It argues that the mutated code is 'out-of-distribution' because NeuroCodeBench was released in late 2023, but does not state the actual training cutoff date."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section 4 explicitly discusses this: 'the original NeuroCodeBench is in the public domain, it was released in late 2023, and it is thus unlikely to have been included in the training set of most state-of-the-art large language models. In addition, our automated mutation technique further ensures that our AI code dataset looks very different from any piece of software the current large language models have been trained on.'"
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": true,
         "justification": "The paper argues that contamination risk is low because (1) NeuroCodeBench was released in late 2023 and (2) the mutation process creates code that is different from anything in training sets. This is a reasonable argument even if not formally verified."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved in this study."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": false,
         "justification": "The paper runs 14,400 GPT-3.5-Turbo API calls for Section 4 and additional calls for the iterative experiments in Section 5, but never reports the API cost, tokens consumed, or wall-clock time for the LLM inference."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "Hardware specifications are given (Intel Xeon CPUs, 32 GB / 198 GB RAM) but no total compute budget is stated: no GPU hours, no total API spend, no total experiment runtime."
       }
     }
   },
   "claims": [
     {
       "claim": "ESBMC can efficiently verify memory safety properties in neural network C code, contrasting with prior claims that software verifiers struggle with such code.",
       "evidence": "Section 3.3 and Figure 4 show ESBMC classified a sizable portion of the 81,129 mutated programs as safe or unsafe within a 300-second timeout, with verification times often in the range of seconds to minutes.",
       "supported": "moderate"
     },
     {
       "claim": "The best single-iteration prompt engineering approach achieves approximately 18% successful repair rate using the one-line source code strategy with persona prompts.",
       "evidence": "Section 4.3 and Figure 8b report the best single-line prompt (template 11, role 'Automated Code Repair Tool', counterexample feedback) achieved ~18% verified repairs. Tables 2-3 provide compilation and verification rates across all configurations.",
       "supported": "moderate"
     },
     {
       "claim": "Iterative automated program repair increases the successful repair rate from ~18% to ~25% compared to single-iteration approaches.",
       "evidence": "Section 5.4 states 'the best results of non-iterative APR were ~18%, while the iterative approach explored in Section 5 increased the successful repairs to ~25%.' Figure 11 shows per-attempt success rates.",
       "supported": "moderate"
     },
     {
       "claim": "Providing verifier feedback in the prompt worsens LLM repair performance.",
       "evidence": "Figures 6b, 7b show that adding ESBMC output lowers C/C++ detection scores and source code match for the contextual strategy. Section 4.5 states 'providing feedback from a verifier about the nature of the vulnerability makes the performance worse.'",
       "supported": "weak"
     },
     {
       "claim": "Forward History message format is the best approach for iterative APR, and lower temperature yields higher repair accuracy.",
       "evidence": "Figures 11 and 12 show Forward History outperforming LSO and Reverse History, with temperature 0.0 yielding the best results for Forward History. Section 5.4 summarizes these findings.",
       "supported": "moderate"
     },
     {
       "claim": "Persona prompts produce C-like code more consistently than simple prompts.",
       "evidence": "Figure 6a shows persona prompts yield higher C/C++ detector scores than simple prompts for the contextual strategy.",
       "supported": "weak"
     }
   ],
   "methodology_tags": [
     "benchmark-eval"
   ],
   "key_findings": "The paper expands NeuroCodeBench from 505 to 81,129 neural network C programs via mutation and uses ESBMC to identify memory safety vulnerabilities. Using GPT-3.5-Turbo with 144 prompt engineering configurations, the best single-iteration repair rate is approximately 18% (one-line source code with persona prompt), while iterative repair with forward history reaches approximately 25%. The study reveals that providing verifier feedback paradoxically worsens repair performance, and that the specific persona role assigned to the LLM has minimal effect on outcomes.",
   "red_flags": [
     {
       "flag": "Authors evaluate their own tool",
       "detail": "The authors are developers of ESBMC and ESBMC-AI, the core tools being evaluated. This conflict of interest is not acknowledged anywhere in the paper."
     },
     {
       "flag": "Single LLM tested with broad claims",
       "detail": "Only GPT-3.5-Turbo is tested, but the title and text frequently reference 'Large Language Models' in the plural, suggesting broader generalizability than the evidence supports."
     },
     {
       "flag": "No statistical significance testing",
       "detail": "Comparisons between prompt configurations are made by comparing raw percentages from 100 samples without any significance tests. With small sample sizes and low repair rates (<18%), many observed differences could be due to random variation."
     },
     {
       "flag": "No repeated experimental runs",
       "detail": "Experiments appear to be single runs with temperature=1.0 (stochastic), meaning results could vary significantly across repetitions. The paper acknowledges that 'temporary changes in the ChatGPT backend' could affect results but does not address this with repeated runs."
     },
     {
       "flag": "No cost reporting despite large API usage",
       "detail": "14,400+ API calls to GPT-3.5-Turbo in Section 4 alone, plus extensive iterative experiments in Section 5, with no cost or token consumption reported."
     },
     {
       "flag": "Missing limitations section",
       "detail": "The paper has no dedicated limitations or threats-to-validity section, which is a significant omission for empirical work."
     }
   ],
   "cited_papers": [
     {
       "title": "A new era in software security: Towards self-healing software via large language models and formal verification",
       "authors": ["Y. Charalambous", "N. Tihanyi", "R. Jain", "Y. Sun", "M. A. Ferrag", "L. C. Cordeiro"],
       "year": 2023,
       "arxiv_id": "2305.14752",
       "relevance": "Precursor work on using LLMs with formal verification for automated code repair, providing the baseline prompt template evaluated in this paper."
     },
     {
       "title": "Automated repair of programs from large language models",
       "authors": ["Z. Fan", "X. Gao", "M. Mirchev", "A. Roychoudhury", "S. H. Tan"],
       "year": 2023,
       "relevance": "Contemporary work on LLM-based automated program repair, directly relevant to the survey scope of AI-assisted code generation and repair."
     },
     {
       "title": "A prompt pattern catalog to enhance prompt engineering with ChatGPT",
       "authors": ["J. White", "Q. Fu", "S. Hays", "M. Sandborn", "C. Olea", "H. Gilbert", "A. Elnashar", "J. Spencer-Smith", "D. C. Schmidt"],
       "year": 2023,
       "arxiv_id": "2302.11382",
       "relevance": "Foundational work on prompt engineering patterns used as theoretical basis for the prompting strategies compared in this paper."
     },
     {
       "title": "Language models are few-shot learners",
       "authors": ["T. Brown", "B. Mann", "N. Ryder"],
       "year": 2020,
       "relevance": "GPT-3 paper providing the foundation for the GPT-3.5-Turbo model used in the experiments."
     },
     {
       "title": "How is ChatGPT's behavior changing over time?",
       "authors": ["L. Chen", "M. Zaharia", "J. Zou"],
       "year": 2023,
       "arxiv_id": "2307.09009",
       "relevance": "Addresses temporal instability in LLM behavior, cited to explain anomalous experimental results — relevant to evaluation methodology for LLM studies."
     },
     {
       "title": "Pitfalls in machine learning research: Reexamining the development cycle",
       "authors": ["S. Biderman", "W. J. Scheirer"],
       "year": 2020,
       "relevance": "Discusses methodological pitfalls in ML research, relevant to the survey's focus on research quality assessment."
     },
     {
       "title": "NeuroCodeBench: a Plain C Neural Network Benchmark for Software Verification",
       "authors": ["E. Manino", "R. S. Menezes", "F. Shmarov", "L. C. Cordeiro"],
       "year": 2023,
       "relevance": "The foundational benchmark expanded in this paper, central to the evaluation of AI code verification and repair."
     },
     {
       "title": "Taxonomy of real faults in deep learning systems",
       "authors": ["N. Humbatova", "G. Jahangirova", "G. Bavota", "V. Riccio", "A. Stocco", "P. Tonella"],
       "year": 2020,
       "relevance": "Provides taxonomy of bugs in deep learning systems, motivating the focus on memory safety vulnerabilities in neural network code."
     },
     {
       "title": "Language models are unsupervised multitask learners",
       "authors": ["A. Radford", "J. Wu", "R. Child", "D. Luan", "D. Amodei", "I. Sutskever"],
       "year": 2019,
       "relevance": "GPT-2 paper referenced for the GPT family architecture underlying the LLM used in experiments."
     }
   ]
 }