ai-research-survey

scan.json (22632B)

---

 {
   "paper": {
     "title": "LLM-based framework to support the construction of valid formal models",
     "authors": [
       "Gábor Guta",
       "Gábor Kusper"
     ],
     "year": 2025,
     "venue": "FMF-AI 2025 (International Conference on Formal Methods and Foundations of Artificial Intelligence)",
     "doi": "10.17048/fmfai.2025.78"
   },
   "scan_version": 2,
   "active_modules": [],
   "methodology_tags": [
     "case-study",
     "qualitative"
   ],
   "key_findings": "The paper proposes a human-in-the-loop tool for validating LLM-generated UML models by deterministically back-translating them to natural language for comparison with original requirements. Testing on a single web-shop specification (32 functional, 15 nonfunctional requirements) reveals that mechanical back-translation operates at a different abstraction level than the original requirements, making direct comparison confusing. The authors acknowledge the tool currently lacks practical capability, identifying model-to-NL translation quality and bidirectional model management as key unsolved challenges.",
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": false,
         "justification": "No code repository, archive, or download link is provided anywhere in the paper. The tool is described as a prototype implemented in Python with LangChain and Streamlit, but no source code is released."
       },
       "data_released": {
         "applies": true,
         "answer": false,
         "justification": "The web-shop specification (32 functional, 15 nonfunctional requirements following IEEE 830) used as the test input is not released. Only fragments are shown in the paper (Listings 1-3)."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper mentions Python, LangChain, Streamlit, and PlantUML as technologies used (Section 4.1) but provides no version numbers, requirements file, or environment specification sufficient to recreate the setup."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "No reproduction instructions are provided. There are no README files, setup guides, or step-by-step instructions for replicating the experiments."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "The paper reports no quantitative results whatsoever. The three experiments (Section 5) are entirely qualitative with no measurements, so no confidence intervals or error bars are provided."
       },
       "significance_tests": {
         "applies": false,
         "answer": false,
         "justification": "The paper makes no comparative quantitative claims. All comparisons between approaches are qualitative observations."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": false,
         "justification": "No effect sizes or quantitative measurements of any kind are reported. The paper claims 'our approach works' (Section 6) without quantifying the effect."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "The entire evaluation uses a single web-shop example specification. No justification is given for why this single example is sufficient to support the paper's claims."
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "No repeated runs, no variance, no quantitative results of any kind are reported across the three experiments."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": false,
         "justification": "Section 5.1 qualitatively describes testing 'available LLM tools' for generating specifications but provides no quantitative comparison against their approach. No structured baseline comparison exists."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": false,
         "justification": "No baselines are quantitatively compared. Section 5.1 references existing LLM tools generically without naming specific tools or providing comparative results."
       },
       "ablation_study": {
         "applies": true,
         "answer": false,
         "justification": "The system has multiple components (LLM generation, rule-based back-translation, human validation UI) but no ablation study isolates their individual contributions."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": false,
         "justification": "No evaluation metrics are defined or reported. The evaluation is entirely qualitative with no measurements."
       },
       "human_evaluation": {
         "applies": true,
         "answer": false,
         "justification": "Despite the entire approach centering on human-in-the-loop validation, no user study or formal human evaluation is conducted. The authors appear to have tested the tool themselves without involving independent evaluators."
       },
       "held_out_test_set": {
         "applies": false,
         "answer": false,
         "justification": "No ML training or test sets are involved. This is a tool prototype tested on a single manually-created specification."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": false,
         "justification": "No breakdowns by requirement type, diagram type, or any other category are provided. Results are discussed only in general qualitative terms."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section 5.2 reports that 'just mechanistically translating back the models to natural language is not sufficient.' Section 5.3 identifies that back-translated descriptions operate at a different abstraction level than original specifications, causing confusion from 'mechanical enumerations' vs 'compact concepts.'"
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "The paper honestly reports several negative findings: back-translation quality is insufficient (Section 5.2), abstraction level mismatches are problematic (Section 5.3), and the tool 'currently lacks the capability to be used in practice' (Section 6)."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract modestly claims to 'propose a tool which facilitates the validation' and describes its two-step process. The paper does present this tool and demonstrate its workflow. The abstract does not overclaim quantitative results."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": false,
         "justification": "The paper claims the approach 'mitigates the risks associated with LLM black-box generation' (Abstract) and that 'it is evident that our approach works' (Section 6). These are causal claims about the effectiveness of the intervention, but the single-example qualitative evaluation with no control condition does not support causal inference."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": false,
         "justification": "The title claims support for 'construction of valid formal models' generally, but the evaluation uses only UML diagrams (class, sequence, use case) on a single web-shop example. No explicit statement bounds the generalization to this specific domain, diagram type, or application class."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": false,
         "justification": "No alternative explanations for the observed challenges are discussed. For example, the paper does not consider whether the abstraction level mismatch could be due to prompt quality, LLM choice, or specification complexity rather than inherent limitations of the approach."
       },
       "proxy_outcome_distinction": {
         "applies": true,
         "answer": false,
         "justification": "The paper claims its approach enables 'validation' and 'mitigates risks,' but what it actually demonstrates is that back-translation produces natural language text. Whether this output actually helps users validate models or reduces errors is not measured. The gap between producing back-translations and achieving validation is not discussed."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper refers only to 'a generic LLM with prompt-based configuration' (Section 4) and 'LLM tools' (Section 5.1). No specific model name, version, or provider is ever identified anywhere in the paper."
       },
       "prompts_provided": {
         "applies": true,
         "answer": false,
         "justification": "The paper mentions 'prompt-based configuration' and 'extensive prompting' (Section 5.1) but provides no actual prompt text. Only the output (PlantUML listings) is shown."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": false,
         "justification": "No hyperparameters (temperature, top-p, max tokens, etc.) are reported for any LLM interaction."
       },
       "scaffolding_described": {
         "applies": false,
         "answer": false,
         "justification": "The system uses LangChain as an LLM integration framework in a pipeline architecture (NL → LLM → UML → rule-based back-translation), not agentic scaffolding with tools, retry logic, or autonomous decision-making."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": false,
         "justification": "The paper mentions the specification follows IEEE 830 format (Section 1.1) and shows fragments, but does not document how the specification was preprocessed or formatted for LLM consumption, or how the LLM output was parsed into PlantUML."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": true,
         "justification": "Section 5 (Discussion) provides substantive discussion of challenges and limitations across three experiments (5.1-5.3). Section 6 (Conclusion) explicitly states the tool 'currently lacks the capability to be used in practice' and identifies two specific areas requiring further research."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": false,
         "justification": "The discussion in Section 5 covers implementation challenges (abstraction level mismatch, mechanical enumerations) but does not discuss threats to the validity of the study's conclusions, such as whether the web-shop example is representative, whether the qualitative findings generalize, or whether author-only evaluation introduces bias."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": false,
         "justification": "While Section 5.3 notes 'we support only the validation of the forward-engineering approach' and Section 6 acknowledges practical limitations, the paper does not explicitly state what its results do NOT show or which settings/domains are excluded from its claims."
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": false,
         "justification": "The full web-shop specification (32 functional + 15 nonfunctional requirements) is not available. Only fragments are shown in the paper (Listings 1-3). Generated UML models and back-translations are partially shown but not fully available."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "Section 1.1 describes the motivational example: a web-shop application specification formulated according to IEEE 830 standard with 32 functional and 15 nonfunctional requirements, chosen because it 'adequately represents the typical real-world challenges.'"
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants were involved. The test data is a self-created specification, not a standard benchmark."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": false,
         "justification": "The high-level workflow is shown in Figures 1 and 2, but the detailed pipeline from specification input through LLM processing to UML generation and back-translation is not documented with sufficient detail to understand each transformation step."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": false,
         "justification": "No funding source, grants, or sponsorship are mentioned anywhere in the paper. There is no acknowledgments section discussing funding."
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Author affiliations are clearly stated: Gábor Guta is from Axonmatics Kft. (a company), and Gábor Kusper is from the Mathematics and Informatics Institute at Eszterházy Károly University."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": false,
         "justification": "No funding disclosure is present, so independence cannot be assessed. The first author's affiliation with Axonmatics Kft. suggests potential commercial interest in the tool, but this conflict is not discussed."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests or financial interests statement is present. The first author is from Axonmatics Kft. which could potentially commercialize the tool, but no declaration is made."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": false,
         "answer": false,
         "justification": "The paper does not evaluate a pre-trained model's capability on any benchmark. It uses an LLM as a tool for specification translation, not to measure model knowledge or capability."
       },
       "train_test_overlap_discussed": {
         "applies": false,
         "answer": false,
         "justification": "No benchmark evaluation is performed. The paper tests a tool pipeline, not model capabilities on a test set."
       },
       "benchmark_contamination_addressed": {
         "applies": false,
         "answer": false,
         "justification": "No benchmark evaluation is performed. The web-shop specification is a custom-created input, not a benchmark for measuring model performance."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study. The tool is tested by the authors themselves."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved in the study."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": false,
         "justification": "The tool uses LLM API calls for generating UML from natural language but no inference costs, API costs, or latency figures are reported."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "No computational budget, hardware requirements, or resource consumption is stated for the tool or experiments."
       }
     }
   },
   "claims": [
     {
       "claim": "The two-step approach (LLM generation + deterministic back-translation + human validation) enables semantic verification of formal models",
       "evidence": "Section 4 describes the workflow and Section 4.1 shows implementation with PlantUML examples (Listings 2-3) and requirement-to-model mappings. However, no empirical measurement of verification effectiveness is provided.",
       "supported": "weak"
     },
     {
       "claim": "Mechanistic back-translation of formal models to natural language is insufficient for validation",
       "evidence": "Section 5.2: 'just mechanistically translating back the models to natural language is not sufficient even if the textual representation is nicely formulated.' The key finding is that template-based descriptions don't operate at the same abstraction level as original specifications.",
       "supported": "moderate"
     },
     {
       "claim": "The approach works but currently lacks practical capability",
       "evidence": "Section 6: 'Based on our initial experiments described in the previous section, it is evident that our approach works, but we have identified two main areas of functionality that require further research.' And: 'it currently lacks the capability to be used in practice.'",
       "supported": "weak"
     },
     {
       "claim": "Back-translated descriptions confuse users because compact concepts become mechanical enumerations at a different abstraction level",
       "evidence": "Section 5.3 identifies two specific confusion sources: 'compact concepts are described as mechanical enumerations' and 'only a single model-specific aspect is presented.' Illustrated by Listing 3 where 'Add item to cart with quantity' becomes a multi-sentence field enumeration.",
       "supported": "moderate"
     }
   ],
   "red_flags": [
     {
       "flag": "No quantitative evaluation",
       "detail": "Despite claiming 'our approach works,' the paper reports zero quantitative metrics. No accuracy measurements, no user task performance, no error rates — only qualitative observations from the authors themselves."
     },
     {
       "flag": "Single example evaluation",
       "detail": "The entire evaluation rests on one web-shop specification. No variation in domain, complexity, or specification style is tested. Claims about 'formal models' generally are unsupported by this single case."
     },
     {
       "flag": "Unspecified LLM",
       "detail": "The paper never identifies which LLM was used, referring only to 'a generic LLM with prompt-based configuration.' This makes the work completely unreproducible — different models would likely produce very different results."
     },
     {
       "flag": "No user study for a human-in-the-loop tool",
       "detail": "The core value proposition is that humans can validate back-translated models, yet no independent users were tested. The authors evaluated their own tool, introducing obvious bias. Whether the approach actually helps users catch errors is unknown."
     },
     {
       "flag": "Undisclosed potential conflict of interest",
       "detail": "First author is from Axonmatics Kft. (a company) which could have commercial interest in the tool. No competing interests statement or funding disclosure is provided."
     }
   ],
   "cited_papers": [
     {
       "title": "Formalising Software Requirements using Large Language Models",
       "authors": ["A. Beg", "D. O'Donoghue", "R. Monahan"],
       "year": 2025,
       "arxiv_id": "2506.10704",
       "doi": "10.48550/arxiv.2506.10704",
       "relevance": "Directly addresses LLM use for generating formal specifications from natural language, a core application area for AI-assisted software engineering."
     },
     {
       "title": "nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models",
       "authors": ["M. Cosler", "C. Hahn", "D. Mendoza", "F. Schmitt", "C. Trippel"],
       "year": 2023,
       "arxiv_id": "2303.04864",
       "doi": "10.48550/arXiv.2303.04864",
       "relevance": "Introduces prompt engineering and structured intermediate formats for LLM-based formal specification translation, addressing reliability of LLM outputs."
     },
     {
       "title": "A Survey on Code Generation with LLM-based Agents",
       "authors": ["Y. Dong", "X. Jiang", "J. Qian", "T. Wang", "K. Zhang", "Z. Jin", "G. Li"],
       "year": 2025,
       "relevance": "Comprehensive survey on LLM-based code generation agents, directly relevant to understanding the broader LLM programming landscape."
     },
     {
       "title": "Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving",
       "authors": ["S. K. Jha", "S. Jha", "P. Lincoln", "N. D. Bastian", "A. Velasquez", "R. Ewetz", "S. Neema"],
       "year": 2023,
       "arxiv_id": "2309.16436",
       "doi": "10.48550/arxiv.2309.16436",
       "relevance": "Combines LLMs with formal verification (SAT solving) for synthesis, exploring the intersection of LLM capabilities with formal methods."
     },
     {
       "title": "Safety analysis in the era of large language models: A case study of STPA using ChatGPT",
       "authors": ["Y. Qi", "X. Zhao", "S. Khastgir", "X. Huang"],
       "year": 2025,
       "doi": "10.1016/j.mlwa.2025.100622",
       "relevance": "Evaluates ChatGPT for safety-critical analysis with human validation, directly addressing reliability and human-in-the-loop needs for LLM-based tools."
     },
     {
       "title": "From Image to UML: First Results of Image Based UML Diagram Generation Using LLMs",
       "authors": ["A. Conrardy", "J. Cabot"],
       "year": 2024,
       "arxiv_id": "2404.11376",
       "doi": "10.48550/arXiv.2404.11376",
       "relevance": "Explores LLM capabilities for generating UML models from images, relevant to understanding LLM limitations in model-driven engineering."
     }
   ]
 }