ai-research-survey

scan.json (25149B)

---

 {
   "paper": {
     "title": "Towards Formal Verification of LLM-Generated Code from Natural Language Prompts",
     "authors": ["Aaron Councilman", "David Jiahao Fu", "Aryan Gupta", "Chengxiao Wang", "David Grove", "Yu-Xiong Wang", "Vikram Adve"],
     "year": 2025,
     "venue": "arXiv",
     "arxiv_id": "2507.13290",
     "doi": "10.48550/arXiv.2507.13290"
   },
   "scan_version": 2,
   "active_modules": ["experimental_rigor", "data_leakage"],
   "methodology_tags": ["benchmark-eval"],
   "key_findings": "Astrogator, a formal verification system for LLM-generated Ansible code, correctly accepts 82.9% of correct programs and rejects 92.4% of incorrect programs on a benchmark of 21 tasks with 1260 generated programs across 6 LLMs. Only 26.5% of LLM-generated Ansible programs were correct, with GPT-4o significantly outperforming open-source models (51.4% vs 21.5%). The paper demonstrates that a formal query language combined with a State Calculus and symbolic interpreter can provide formal correctness guarantees for DSL code generation.",
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": false,
         "justification": "No repository URL, GitHub link, or code archive is mentioned anywhere in the paper. Astrogator's implementation is described but not released."
       },
       "data_released": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark suite of 21 tasks is described (NL descriptions and formal queries in Appendix A) but no downloadable dataset or archive of the 1260 generated programs is provided."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper mentions using VMs (Debian 12.11.0, Ubuntu 24.04.2, RHEL 9.6) for testing but provides no environment specification for running Astrogator itself (no requirements.txt, Dockerfile, or dependency list)."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "No reproduction instructions, README, or scripts are provided. The paper describes the methodology but does not provide step-by-step instructions for reproducing experiments."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "Results are reported as raw counts and percentages (e.g., 82.9% acceptance of correct programs, 92.4% rejection of incorrect programs) with no confidence intervals or error bars."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "The paper claims GPT-4o 'performs significantly better' (51.4% vs 21.5%) but provides no statistical test to support this comparative claim."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": true,
         "justification": "Results are reported with baseline context: 277/334 correct programs accepted (82.9%), 856/926 incorrect programs rejected (92.4%), and per-model breakdowns with absolute counts out of 210 programs each (Table 3)."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark suite has 21 tasks with 10 generations per LLM per task (1260 total). No justification is given for why 21 benchmarks or 10 samples per task is sufficient."
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "No variance or standard deviation is reported. LLMs are nondeterministic and prompted 10 times each, but no spread measures are provided across runs."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": false,
         "justification": "There is no comparison to any alternative verification method, testing approach, or prior verification tool. Astrogator is evaluated in isolation."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": false,
         "justification": "No baselines are included at all, so contemporaneity cannot be assessed."
       },
       "ablation_study": {
         "applies": true,
         "answer": false,
         "justification": "Astrogator has multiple components (formal query language, State Calculus, symbolic interpreter, unifier, knowledge base) but no ablation study is performed to measure individual contributions."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": true,
         "justification": "The paper reports both acceptance rate of correct programs (82.9%) and rejection rate of incorrect programs (92.4%), effectively measuring both precision and recall of the verifier."
       },
       "human_evaluation": {
         "applies": true,
         "answer": false,
         "justification": "No human evaluation is conducted. The formal query language is designed for user review but no user study validates that users can actually understand and verify formal queries."
       },
       "held_out_test_set": {
         "applies": false,
         "answer": false,
         "justification": "This is not a machine learning system being trained; it is a formal verification tool. There is no training/test split to discuss."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Table 4 provides per-benchmark breakdowns of correct/incorrect programs accepted/rejected, and Table 3 provides per-model breakdowns of error types."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.3 extensively discusses both false rejections (57 correct programs rejected) and false acceptances (70 incorrect programs accepted), categorizing root causes including unsupported features, knowledge base limitations, and under-specified queries."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "The paper honestly reports that only 26.5% of LLM-generated code is correct, that Astrogator rejects 57 correct programs and accepts 70 incorrect ones, and details the specific limitations causing these failures."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract claims 83% verification of correct code and 92% identification of incorrect code, matching the results in Section 6.3 (82.9% and 92.4% respectively)."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": true,
         "justification": "The paper's causal claims are primarily about the verification system's design choices. Claims about why errors occur (e.g., knowledge base returning single values, unsupported features) are justified by detailed analysis of each failure case in Section 6.3."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": true,
         "justification": "The paper is clear that Astrogator is specific to Ansible (Section 7.2: 'While Astrogator is specific to Ansible'), and future work sections (Bash, Arduino) are presented as illustrative examples with hand-translations, not claimed as fully supported."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not discuss alternative explanations for the observed verification rates. For example, it does not consider whether the 83%/92% rates are artifacts of the benchmark suite's simplicity or the particular LLMs chosen."
       },
       "proxy_outcome_distinction": {
         "applies": true,
         "answer": true,
         "justification": "The paper is careful to distinguish between its test-based ground truth (which is imperfect) and true correctness, explicitly acknowledging in Section 6.1 that tests are used because 'no other solution was feasible' and that they 'have done our best to craft strong tests.'"
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": false,
         "justification": "Models are listed by name (Deepseek Coder 6.7b, Granite 8b Code, Qwen2.5 Coder 3b, Llama 3.1 8b, Starcoder 2 15b, GPT-4o) but no specific version strings or snapshot dates are given for GPT-4o."
       },
       "prompts_provided": {
         "applies": true,
         "answer": true,
         "justification": "The full code-generation prompt is provided in Appendix B."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": false,
         "justification": "No temperature, top-p, or other generation hyperparameters are reported for any of the 6 LLMs used."
       },
       "scaffolding_described": {
         "applies": false,
         "answer": false,
         "justification": "No agentic scaffolding is used. The LLMs are prompted directly with a single prompt to generate Ansible playbooks."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.2 describes post-processing of generated code: extracting key elements and inserting into a template, with counts of failures (42 syntax errors, 5 non-terminating programs)."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": true,
         "justification": "Section 7 (Discussion) covers engineering effort limitations and generality limitations. Section 6.3 extensively discusses verification accuracy limitations."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": true,
         "justification": "The paper discusses specific threats: the benchmark suite is hand-crafted and small (21 tasks), the knowledge base returns only one correct value causing false rejections, test-based ground truth may have errors, and the formal query language coverage is limited."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": true,
         "justification": "The paper explicitly states scope boundaries: focused on Ansible DSL, does not support shell commands, knowledge base is hand-curated, Bash and Arduino examples are hand-translated only. Section 7.1 acknowledges significant engineering effort required."
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": false,
         "justification": "The 1260 generated programs, test scripts, VM configurations, and Astrogator source code are not publicly available."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.1 describes benchmark construction from StackOverflow, Ansible Forum, Ansible Galaxy, and interesting variations. Section 6.2 describes code generation: 6 LLMs, 10 programs each, 21 benchmarks."
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants. The 'data' is LLM-generated code and a hand-crafted benchmark suite."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "The full pipeline is documented: LLM generation → post-processing (42 syntax failures, 5 non-terminating) → VM testing (Debian, Ubuntu, RHEL) → correctness classification → verifier evaluation. Counts at each stage are provided in Section 6.2."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Acknowledgments section discloses funding from IBM-ILLINOIS Discovery Accelerator Institute (IIDAI) and NSF (Delta computing resource, ACCESS program)."
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Author affiliations are clearly listed: five authors from UIUC and one from IBM Research. David Grove is from IBM Research, and the work is funded by IBM-ILLINOIS partnership."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": true,
         "justification": "IBM and NSF fund the research but do not have a direct financial stake in the specific verification results. The paper does not evaluate IBM products."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests statement is provided. Given IBM Research co-authorship and IBM-ILLINOIS funding, a competing interests declaration would be expected."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": false,
         "justification": "No training data cutoff dates are stated for any of the 6 LLMs used to generate code."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark tasks are derived from StackOverflow and Ansible Forum posts, which are likely in the training data of the LLMs. This potential overlap is not discussed."
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark is custom-built from public sources (StackOverflow, Ansible Forum, Ansible Galaxy) but no contamination analysis is performed. Since these sources are likely in LLM training data, the 26.5% correctness rate may be influenced by contamination."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.3 reports: 'Astrogator took about 70 seconds to process the 1260 programs,' giving wall-clock time for the verification pipeline."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "While verification time is mentioned (70 seconds for 1260 programs), the total compute budget for LLM code generation across 6 models and 1260 programs is not stated."
       }
     },
     "experimental_rigor": {
       "seed_sensitivity_reported": {
         "applies": true,
         "answer": false,
         "justification": "LLMs are prompted 10 times per task to get diverse outputs, but no seed sensitivity analysis or variance across generations is reported."
       },
       "number_of_runs_stated": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.2: 'we prompt each for ten programs for each problem to further increase the diversity of our program set, resulting in a total of 1,260 programs.'"
       },
       "hyperparameter_search_budget": {
         "applies": false,
         "answer": false,
         "justification": "No hyperparameter tuning is performed for the verification system. The LLMs are used off-the-shelf."
       },
       "best_config_selection_justified": {
         "applies": false,
         "answer": false,
         "justification": "No configuration selection is performed; the verifier has a fixed design without tunable parameters."
       },
       "multiple_comparison_correction": {
         "applies": false,
         "answer": false,
         "justification": "No statistical tests are performed, so multiple comparison correction is not applicable."
       },
       "self_comparison_bias_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The authors built both the verifier and the benchmark suite, including the formal queries and reference solutions. This self-evaluation bias is not acknowledged or discussed."
       },
       "compute_budget_vs_performance": {
         "applies": false,
         "answer": false,
         "justification": "The verifier is deterministic and not compute-variable. LLM comparisons are across model size, not compute budget."
       },
       "benchmark_construct_validity": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.1 discusses benchmark design: tasks are 'common tasks based on top posts on StackOverflow and the Ansible Forum' with average 1.67 tasks per reference solution, comparable to prior work [37]. The limitations of test-based ground truth are explicitly discussed."
       },
       "scaffold_confound_addressed": {
         "applies": false,
         "answer": false,
         "justification": "No scaffolding is used. LLMs are prompted directly without agents or tool use."
       }
     },
     "data_leakage": {
       "temporal_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark is derived from StackOverflow and Ansible Forum posts that predate the LLMs' training. No temporal analysis is discussed."
       },
       "feature_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether the prompt format or task descriptions leak information about expected solutions."
       },
       "non_independence_addressed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether benchmark tasks are similar to training examples. StackOverflow-derived tasks are likely well-represented in training data."
       },
       "leakage_detection_method": {
         "applies": true,
         "answer": false,
         "justification": "No leakage detection or prevention method is used."
       }
     }
   },
   "claims": [
     {
       "claim": "Astrogator accepts 82.9% of correct LLM-generated Ansible programs (277/334)",
       "evidence": "Section 6.3, Table 4: per-benchmark breakdown of accepted/rejected programs across all 21 benchmarks",
       "supported": "strong"
     },
     {
       "claim": "Astrogator rejects 92.4% of incorrect LLM-generated Ansible programs (856/926)",
       "evidence": "Section 6.3, Table 4: per-benchmark breakdown showing rejection counts for incorrect programs",
       "supported": "strong"
     },
     {
       "claim": "Only 26.5% of LLM-generated Ansible programs are correct (334/1260)",
       "evidence": "Section 6.2, Table 3: breakdown by model showing syntax errors, execution errors, test failures, and correct programs",
       "supported": "moderate"
     },
     {
       "claim": "GPT-4o significantly outperforms open-source models at Ansible code generation (51.4% vs 21.5%)",
       "evidence": "Table 3: GPT-4o produces 108 correct programs (51.4%) vs open-source models averaging 21.5%",
       "supported": "moderate"
     },
     {
       "claim": "All incorrect rejections by Astrogator are due to addressable implementation limitations, not fundamental approach limitations",
       "evidence": "Section 6.3: 18 due to unsupported features (blocks, handlers, shell commands), 39 due to knowledge base returning single values",
       "supported": "moderate"
     }
   ],
   "red_flags": [
     {
       "flag": "Self-built benchmark with no external validation",
       "detail": "The authors created both the benchmark suite (21 tasks), the formal queries, and the verification system. No independent validation of benchmark quality or formal query correctness is provided. The benchmark is small (21 tasks) for the claims being made."
     },
     {
       "flag": "No comparison to alternative approaches",
       "detail": "Astrogator is evaluated in isolation with no comparison to testing, fuzzing, static analysis, or other verification approaches. The 83%/92% rates have no baseline for comparison."
     },
     {
       "flag": "Missing hyperparameters for LLM generation",
       "detail": "Temperature, top-p, and other generation parameters are not reported for any of the 6 LLMs, making the code generation portion of the experiment non-reproducible."
     },
     {
       "flag": "Contamination risk unaddressed",
       "detail": "Benchmark tasks are derived from StackOverflow and Ansible Forum, which are likely in LLM training data. The 26.5% correctness rate and model comparisons may be influenced by training data overlap."
     }
   ],
   "cited_papers": [
     {
       "title": "Evaluating Large Language Models Trained on Code",
       "authors": ["Mark Chen", "Jerry Tworek"],
       "year": 2021,
       "arxiv_id": "2107.03374",
       "relevance": "HumanEval benchmark for LLM code generation evaluation, foundational to the code generation evaluation field."
     },
     {
       "title": "DeepSeek-Coder: When the Large Language Model Meets Programming",
       "authors": ["Daya Guo", "Qihao Zhu"],
       "year": 2024,
       "arxiv_id": "2401.14196",
       "relevance": "One of the open-source code generation models evaluated in this paper's experiments."
     },
     {
       "title": "What's Wrong with Your Code Generated by Large Language Models? An Extensive Study",
       "authors": ["Shihan Dou", "Haoxiang Jia"],
       "year": 2024,
       "arxiv_id": "2407.06153",
       "relevance": "Study of bugs in LLM-generated code, relevant to understanding code quality and verification needs."
     },
     {
       "title": "Do Users Write More Insecure Code with AI Assistants?",
       "authors": ["Neil Perry", "Megha Srivastava", "Deepak Kumar", "Dan Boneh"],
       "year": 2023,
       "doi": "10.1145/3576915.3623157",
       "relevance": "Security implications of AI code assistants, motivating the need for formal verification."
     },
     {
       "title": "Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?",
       "authors": ["Madeline Endres", "Sarah Fakhoury"],
       "year": 2024,
       "doi": "10.1145/3660791",
       "relevance": "LLM formalization of natural language into formal specifications, directly related approach."
     },
     {
       "title": "SWE-bench: Can Language Models Resolve Real-world Github Issues?",
       "authors": ["Carlos E Jimenez", "John Yang"],
       "year": 2024,
       "relevance": "Major benchmark for LLM code generation in real-world settings."
     },
     {
       "title": "A Large-Scale Survey on the Usability of AI Programming Assistants: Successes and Challenges",
       "authors": ["Jenny T. Liang", "Chenyang Yang", "Brad A. Myers"],
       "year": 2024,
       "doi": "10.1145/3597503.3608128",
       "relevance": "Survey on AI code assistant usability, documenting challenges users face verifying LLM-generated code."
     },
     {
       "title": "Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation",
       "authors": ["Jiawei Liu", "Chunqiu Steven Xia"],
       "year": 2023,
       "relevance": "Rigorous evaluation finding errors in HumanEval ground truth, relevant to code generation evaluation methodology."
     },
     {
       "title": "On the Effectiveness of Large Language Models in Domain-Specific Code Generation",
       "authors": ["Xiaodong Gu", "Meng Chen"],
       "year": 2025,
       "doi": "10.1145/3697012",
       "relevance": "Study of LLM effectiveness for DSL code generation, directly relevant to this paper's Ansible focus."
     },
     {
       "title": "Grounded Copilot: How Programmers Interact with Code-Generating Models",
       "authors": ["Shraddha Barke", "Michael B. James", "Nadia Polikarpova"],
       "year": 2023,
       "doi": "10.1145/3586030",
       "relevance": "Study of programmer interaction with AI code assistants, relevant to understanding verification needs."
     },
     {
       "title": "LLM Hallucinations in Practical Code Generation: Phenomena, Mechanism, and Mitigation",
       "authors": ["Ziyao Zhang", "Chong Wang"],
       "year": 2025,
       "doi": "10.1145/3728894",
       "relevance": "Study of hallucinations in LLM code generation, a key problem this paper aims to address through formal verification."
     }
   ]
 }