Generative transformations and patterns in LLM-native approaches for software verification and falsification
Department of Computer Science, The University of Manchester（曼彻斯特大学计算机科学系）；Instituto de Computação (ICOMP-UFAM), Universidade Federal do Amazonas（亚马逊联邦大学计算学院（ICOMP-UFAM））
Víctor A. Braberman, Flavia Bonomo-Braberman, Yiannis Charalambous, Juan G. Colonna, Lucas C. Cordeiro, Rosiane de Freitas
提示（prompting）作为利用大型语言模型（LLM）的主导范式而出现，导致了LLM原生软件的激增，其中应用程序行为源于复杂的、随机的数据变换。然而，此类系统的工程实践在很大程度上仍处于探索性和临时性阶段，受到缺乏概念框架、事前方法论、设计指南和专门基准的阻碍。我们认为，迈向更规范工程实践的基础性步骤，是系统性地理解核心功能单元——生成式变换（generative transformations）——及其在LLM原生应用中的组合模式。聚焦于软件验证与反证（software verification and falsification）这一丰富领域，我们开展了一项涵盖100多篇研究提案的二次研究以填补这一空白。我们首先提出一个细粒度的生成式变换分类法，将基于提示的交互抽象为概念性签名。该分类法作为脚手架，用于识别反复出现的变换关系模式——类似于软件设计模式——这些模式表征了文献中的解决方案方法。我们的分析不仅验证了分类法的实用性，还揭示了战略空白和跨维度关系，为未来在模块化和组合式LLM应用设计、基准测试以及开发可靠LLM原生系统方面的研究提供了结构化基础。
英文摘要：
The emergence of prompting as the dominant paradigm for leveraging Large Language Models (LLMs) has led to a proliferation of LLM-native software, where application behavior arises from complex, stochastic data transformations. However, the engineering of such systems remains largely exploratory and ad-hoc, hampered by the absence of conceptual frameworks, ex-ante methodologies, design guidelines, and specialized benchmarks. We argue that a foundational step towards a more disciplined engineering practice is a systematic understanding of the core functional units--generative transformations--and their compositional patterns within LLM-native applications.
Focusing on the rich domain of software verification and falsification, we conduct a secondary study of over 100 research proposals to address this gap. We first present a fine-grained taxonomy of generative transformations, abstracting prompt-based interactions into conceptual signatures. This taxonomy serves as a scaffolding to identify recurrent transformation relationship patterns--analogous to software design patterns--that characterize solution approaches in the literature. Our analysis not only validates the utility of the taxonomy but also surfaces strategic gaps and cross-dimensional relationships, offering a structured foundation for future research in modular and compositional LLM application design, benchmarking, and the development of reliable LLM-native systems.
AIGS: Generating Science from AI-Powered Automated Falsification
Department of Computer Science & Technology, Tsinghua University（清华大学计算机科学与技术系）；Institute for AI Industry Research (AIR), Tsinghua University（清华大学人工智能产业研究院）
A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation
University of Liverpool（利物浦大学）；Purple Mountain Laboratories（紫金山实验室）；Université Grenoble Alpes（格勒诺布尔阿尔卑斯大学）；The University of Manchester（曼彻斯特大学）；KU Leuven（鲁汶大学）
Symbolic Analysis of Grover Search Algorithm via Chain-of-Thought Reasoning and Quantum-Native Tokenization
Department of Computer Science, The University of Pittsburgh（匹兹堡大学计算机科学系）；Department of Computer Science, The University of North Carolina at Chapel Hill（北卡罗来纳大学教堂山分校计算机科学系）
Accurate, Interdisciplinary and Transparent Structure-property Understanding with Deep Native Structural Reasoning
Shanghai Artificial Intelligence Laboratory（上海人工智能实验室）；The Chinese University of Hong Kong（香港中文大学）；Shanghai Jiao Tong University（上海交通大学）；Fudan University（复旦大学）；University of Sydney（悉尼大学）；Nanjing University（南京大学）；University of Oxford（牛津大学）；The University of Science and Technology of China（中国科学技术大学）；Drug Discovery and Design Center, State Key Laboratory of Drug Research, Shanghai Institute of Materia Medica, Chinese Academy of Sciences（药物发现与设计中心、国家药物研究重点实验室、上海中医药材料医学研究所、中国科学院）；University of Chinese Academy of Sciences（中国科学院大学）；Stanford University（斯坦福大学）
DScale: Scaling Block-Diffusion Speculative Decoding with Adaptive Verification
Shenzhen Institutes of Advanced Technology, Chinese Academy of Sciences（中国科学院深圳先进技术研究院）；University of Chinese Academy of Sciences（中国科学院大学）；Victoria University of Wellington（惠灵顿维多利亚大学）；University of Macau（澳门大学）
LaTER: Efficient Test-Time Reasoning via Latent Exploration and Explicit Verification
University of Science and Technology of China（科学技术大学）；Unisound AI Technology Co., Ltd（Unisound AI技术有限公司）；MAIS, Institute of Automation, Chinese Academy of Sciences（自动化研究所，中国科学院）
