复杂智能系统仿真测试

题目：Trustworthiness Assurance of Intelligent Systems in the Age of AI Agents

摘要：Recent advances in AI-enabled systems have driven a surge in intelligent applications across diverse domains. This rapid growth has been further accelerated by the emergence of large foundation models, which now form the backbone of many modern AI agentic systems. However, the evolving complexity and centralization of these models introduce new challenges for ensuring their trustworthiness. In this talk, I will provide a high-level overview of our ongoing research on the trustworthiness assurance and systematic engineering of AI-enabled systems in the era of AI agents.

简介：Lei Ma is currently an Associate Professor with the University of Tokyo and an associate professor with University of Alberta. He is a Canada CIFAR AI Chair and Fellow of Amii - Alberta Machine Intelligence Institute. His research centers around the interdisciplinary fields of human-centered trustworthy artificial intelligence (AI), software engineering (SE), and cyber-physical system (CPS) with a special focus on quality, reliability, safety, and security assurance, as well as the interpretation and human interactivity of and AI Systems. Many of his works were published in top-tier AI, software engineering, and security venues (e.g., TSE, TOSEM, ICSE, FSE, ASE, CAV, ICML, NeurIPS, AAAI, IJCAI, TDSC), among which four papers received the ACM SIGSOFT Distinguished Paper Awards (ASE 16, ASE 18, ASE 18, FSE 23), an annual best paper award of the 2022 IEEE Transactions on Software Engineering (TSE 2022), and IEEE TCSE New Directions Awards (2025). More information about his research activities can be found at https://www.malei.org.

题目：从需求到规约：大模型赋能复杂系统形式化验证

摘要：复杂软件系统的开发对软件可信性提出了更高要求，而形式化验证作为保障正确性的有效手段，其瓶颈往往在于形式化规约的构建。近年来，大语言模型为自动化规约生成与验证带来了新的可能。本报告将介绍我们在该方向的系列工作：从自然语言需求到形式化规约的转化框架 REQ2LTL，在航天领域实现高精度需求形式化；基于静态分析与大模型结合的 AutoSpec，用于复杂程序的自动规约综合；以及面向航天嵌入式软件IP组件的智能验证框架，在工业嵌入式系统中显著提升验证效率。这些探索展示了大模型如何助力从需求理解到系统验证的完整链路，为复杂智能系统的可靠性保障开辟新路径。

简介：文成，西安电子科技大学广州研究院华山准聘副教授，CCF形式化方法专委会通讯委员。主要从事高可信软件工程技术、人工智能使能软件开发与验证、可信软件的基础理论与方法等方面的研究，目前已经在包括ACL，ASE，ICSE，CAV，TKDD，TPDS，Information Fusion，IEEE Transactions on Reliability等顶级国际会议和期刊上发表十余篇论文；在Linux内核等开源软件中发现数百个安全漏洞（80+CVEs），多项研究成果已在产业实际场景中（华为、航天）应用。

题目：基于形式化规约与模型检查的需求驱动MIL自动测试

摘要：在汽车工业中，MIL（Model-in-the-Loop）测试是验证软件设计正确性的关键环节。然而，自然语言需求的歧义性与手动建模的高成本，使测试效率与可靠性难以保障。现有基于大语言模型的形式化尝试虽然具备自动化潜力，但因缺乏可控性与领域语义认知，难以生成可信规约，同时面临状态空间爆炸带来的测试生成瓶颈。为此，我们提出 AutoFT，一个从需求到形式化规约再到可执行 MIL 测试的自动化框架。 AutoFT 采用“LLM 信息抽取 + 语义感知的编译”双阶段机制生成TLA+规约，在保持结构化可控性的同时实现领域精确建模；并通过覆盖率引导剪枝，有效降低模型检查生成状态空间的复杂度，从而生成最小且完备的MIL测试用例。

简介：陈金宝，中国科学技术大学2024级博士生，研究方向为现代语言编译和运行时系统、软件安全。相关工作及合作工作在软件学报、JSS、CGO、OOPSLA等国内外知名软件工程期刊和会议中发表。研究成果曾获华为年度优秀合作项目，并已应用于工业实践。

题目：自动驾驶系统仿真测试——何者为要，何者非然

摘要：在自动驾驶系统仿真测试领域，虽已有大量研究，但目前仍缺乏对现有技术价值与贡献的客观评估标准。本文尝试从两个维度回应这一问题：首先，提出一种评估框架，从内在效率与测试有效性两个层面系统比较现有测试方法。研究发现，多数方法难以同时满足这两项要求。其次，指出测试的效率与有效性高度依赖于自动驾驶系统的设计机理，具体体现在不同控制策略间的决策逻辑以及测试结果的可复现性。事实上，自动驾驶系统在决策合理性与环境交互确定性方面的缺失，会显著削弱测试方法的有效性。我们基于八个开源自动驾驶系统的仿真测试结果验证了上述观点。

简介：晏荣杰，中国科学院软件研究所副研究员。CCF高级会员、系统软件专委、嵌入式系统专委和智慧交通分会执行委员。研究方向包括系统形式化建模与分析、智能软件的验证与测试、自主无人系统的仿真测试。在相关领域重要国际期刊SoSYM、JSS、SCP和国际会议ISSTA、FM、FSE、ICRA、DATE、IROS等发表了多篇学术论文。担任中国科学院大学《理论计算机科学基础》课程的主讲教师。

题目：具身智能安全性等效加速测试

摘要：具身智能在安全攸关领域的落地应用，正面临稀疏度灾难（Curse of Rarity）这一关键科学难题，即在复杂的超高维运行环境中安全攸关事件极为罕见，导致传统的测试方法无法对其进行有效统计评估，使得系统的安全水平难以被精确量化与验证。为破解此难题，等效加速测试成为一种重要的解决思路，其目标是在不引入评估偏差的前提下，大幅提升测试效率。这不仅为系统性的安全验证奠定了坚实基础，也构成了智能体实现安全自我迭代闭环的关键一环，最终推动可信赖的具身智能系统走向现实应用。

简介：封硕，清华大学自动化系副教授、特别研究员、博士生导师，目前担任系统工程研究所副所长，入选国家海外高层次青年人才计划。从事智能安全攸关系统测试验证研究，研究成果在自动驾驶汽车领域得到广泛应用，以通讯作者或第一作者在《自然》（2023，封面论文）、《自然·通讯》（2021，2024，featured articles）等高水平期刊发表论文。曾获IEEE智能交通系统学会最佳博士学位论文奖、美国运筹与管理协会智能交通系统年度最佳论文奖、MIT TR35、达摩院青橙奖、AI100青年先锋等荣誉。

题目：机器人具身导航的仿真测试与实机部署

摘要：人形机器人的具身智能导航，要求机器人能与环境进行语义交互，并自主做出导航推理和行动。为攻克这一难题，需要确立了一条以高保真仿真为核心的高效路径：通过在物理逼真、内容多样的虚拟环境中，利用强化学习等算法大规模训练机器人的导航与运动控制策略；进而，采用域随机化等关键技术，主动弥合仿真与现实的鸿沟，将鲁棒的策略安全、平滑地迁移至实机。最终，通过构建“仿真-测试-部署”的闭环迭代系统，持续优化机器人性能，推动人形机器人从走出实验室，最终迈向在复杂真实世界中自主、可靠地执行任务。

简介：郭迟，武汉大学机器人学院副院长，教授，博士生导师，湖北省时空信息与定位导航技术创新中心副主任。主要从事无人系统智能导航、机器人具身智能理论方法及应用方面的研究。主持国家重点研发计划课题、湖北重大科技专项、国家自然科学基金多项。获得自然资源部科学技术一等奖，上海市科技进步一等奖，教育部科技进步二等奖。任武汉大学数智教育核心课《人工智能与机器学习》课程组长，获高等教育（本科）国家级教学成果二等奖、宝钢优秀教师奖。入选湖北首批青年人才计划，任中国卫星导航定位协会无人机专业委员会副主任委员，湖北省测绘地理信息学会理事。

题目：矿山自动驾驶面临的安全挑战

摘要：矿山自动驾驶作为“智慧矿山”的核心，依托矿区封闭、路线固定等优势，已成为自动驾驶技术商业化落地的先行领域。截至2024年，中国露天煤矿已部署约2500辆无人驾驶矿卡，预计到2025年将跃升至5750辆，年增长率高达130%。然而，在规模化部署与追求7×24小时高效运营（单车日均运输量提升15%–20%）的同时，其安全挑战也日益凸显。本文从两个维度探讨这一问题：首先，提出一种适用于矿山场景的评估框架，从内在测试效率与安全有效性两个层面系统比较现有仿真测试方法。研究发现，多数方法难以兼顾矿区对高效率闭环测试和复杂安全场景（如多机协同、极端工况）覆盖的双重要求。其次，指出测试的有效性高度依赖于矿山自动驾驶系统自身的控制机理，具体体现在不同决策策略对矿卡编队、协同装卸等典型作业场景的适应性，以及测试结果在恶劣、动态矿区环境下的可复现性。

简介：杨开睿，易控智驾数据闭环&仿真安全负责人、中国仿真学会自动驾驶汽车仿真测试专委会秘书&委员。国内最早的L4自动驾驶质量领域专家之一，主攻自动驾驶算法仿真测试、仿真对抗性测试、场景自动生成技术以及自动驾驶质量保障。在ICLR、ICCV、NeurIPS、ASE、ICSE、ICRA等国际期刊和会议发表论文多篇。曾负责百度自动驾驶系统集成测试从0到1搭建和Apollo中美测试工作、阿里达摩院自动驾驶测试等。申请发明专利数十篇、主导了自动驾驶领域首个高速枢纽仿真HDmap开源数据集Flyover的研发、主导了阿里天池杯“2022未来汽车”自动驾驶算法挑战赛的赛题设计和专家评测工作，吸引了全球超过1500支队伍参赛。参与了多项自动驾驶场景和法规相关的国家项目和标准制定工作、CCF ChinaSoft分论坛主席等。