Nov, 2023

自主系统的形式方法

PDF
TL;DR给出关于应用形式方法于自治系统领域的当前最新研究状态的概述，包括系统的合成、不确定性的概念、采用形式方法的学习系统的行为界限、系统的监测以及形式方法在强化学习、不确定性、隐私、可解释性、规制和认证方面的未来发展方向。
formal methodsautonomous systemssynthesislearningmonitoring
发现论文，激发创造
  • 面向自动化系统安全评估的形式化故障注入

    通过将形式化方法和故障注入相融合，增强自主系统的可靠性，并通过这种更加紧密的联系，为安全可靠的自动化系统的开发铺平道路。

    Nov, 2023

  • 第四届自主系统形式化方法国际研讨会（FMAS）和第四届自动化可验证软件系统开发国际研讨会（ASYDE）论文集

    本文介绍了 2022 年第四届自主系统形式化方法国际研讨会（FMAS 2022）和第四届自动化和可验证软件系统开发国际研讨会（ASYDE 2022）的联合论文集。该研讨会目的在于汇聚使用形式化方法解决自主系统所带来独特挑战的研究者，探讨在形式化方法在自主和 / 或机器人系统中的应用。该主题涵盖了自主系统、软件开发、验证、协同物理以及工业应用等方向。

    Sep, 2022

  • 机器人与综合形式方法：必要性与机遇相遇

    机器人系统是多维实体，包括硬件和软件，与现实世界的相互作用密切相关，因此需要结合各种形式化方法来开发、验证和提供认证证据，而机器人学是一个理想的催化剂来推动集成形式方法研究的发展，使其朝着新的、令人兴奋的方向发展，并揭示大规模、动态、复杂系统的发展。

    May, 2018

  • 自主驾驶汽车的正式场景测试：从仿真到现实世界

    本文提出了一种基于形式化方法的智能汽车自动场景测试的新方法，结合仿真和实际测试，并通过实验验证形式化仿真可以有效识别可在跑道上运行的测试用例，仿真和真实世界之间的差距可以得到系统评估和弥合。

    Mar, 2020

  • 一种可验证强化学习的归纳综合框架

    本文研究如何使用形式化验证技术对增强学习 - enabled 机器学习系统进行验证，以保证其行为安全，并提出了一种基于黑盒方法的综合确定性程序的方法来实现系统验证。

    Jul, 2019

  • STL: 对系统验证而言意外棘手的逻辑

    人类实验发现形式化方法的规范并不是本质上能够被人类理解的，而且验收正确性受到多种因素的影响，提出了在规范展示和验收培训中应当考虑人体工程学改进的建议。

    May, 2023

  • 利用大型语言模型进行自动形式化

    本文研究了自动形式化的过程，并发现大型语言模型可用于将自然语言的数学问题翻译为 Isabelle/HOL 的形式化说明，证明了这种方法的实用性，并通过训练预先介绍的神经定理证明器使改进了 MiniF2F 定理证明基准的证明率从 29.6% 提高到 35.2%。

    May, 2022

  • 多机器人系统不确定性下的正式建模

    本文回顾了多机器人系统模型的形式化方法，并探讨了如何将它们用于计划、加强学习、模型检验和仿真。最近的研究致力于改进方法，准确捕捉多机器人之间的相互影响与不确定性，以及减少模型规模以提高求解效率。然而，现有的多机器人模型存在着在捕捉机器人依赖和不确定性精度与规模之间的平衡，未来研究应从实际多机器人行为出发，开发精度更高、同时保留多机器人之间不确定性与相互作用的小规模模型，并利用多机器人问题的结构，如因子状态空间，来开发可扩展求解方法。

    May, 2023

  • 使用大型语言模型进行测试学习能力的网络物理系统：一种形式化方法

    通过检查以测试为基础的验证和验证作为最实用的方法，并总结当前先进的方法学，在确保学习能力的 CPS 的形式安全方面，确定了当前测试方法的局限性，并提出了从基础概率测试过渡到更严格方法的路线图，以提供正式保证。

    Nov, 2023

  • 关于可信性的规定

    该文介绍了关于自主系统的可信度、规范和应用领域的高级智力挑战，强调了对功能、安全性、安全性和其他非功能属性等方面的顶层要求的关注。

    Jun, 2022