该研究介绍了一种交互式学习方法，能够从自然语言描述中学习正确、简洁的统一信号时序逻辑公式，并使用深度 Q 学习算法确定机器人的最优控制策略。

Jul, 2022

提出了一种新颖的模仿学习方法，结合了信号时态逻辑（STL）推理和控制综合，能够明确地表示任务作为一个 STL 公式，在理解学习代理的具体任务方面提供了清晰的理解，并通过手动调整 STL 公式将人类知识纳入，以便适应新的场景。此外，我们采用了生成对抗网络（GAN）受启发的训练方法，既能进行推理，又能进行控制策略，有效地缩小了专家策略和学习策略之间的差距。通过两个案例研究，证明了我们算法的有效性，展示了其实际应用性和适应性。

Feb, 2024

该研究在交互式定理证明器 Isabelle/HOL 中，提出了一种简单而简洁的时间规划语义，并基于该语义推导了验证算法。通过正式证明，该验证算法实现了时间规划语义，并进行了实验评估，证明其实用性。

Mar, 2022

通过可交互的证明助手，开发者能够证明机器学习系统的正确性，这种方法暴露了所有的实现错误，并通过 Certigrad 实现了优化的随机计算图，并生成了一个机器可验证的证明，证明了系统采样的梯度是数学梯度的无偏估计方法。

Jun, 2017

给出关于应用形式方法于自治系统领域的当前最新研究状态的概述，包括系统的合成、不确定性的概念、采用形式方法的学习系统的行为界限、系统的监测以及形式方法在强化学习、不确定性、隐私、可解释性、规制和认证方面的未来发展方向。

Nov, 2023

从观察行为中学习 Signal Temporal Logic (STL) 的要求，通过结合贝叶斯优化和信息检索技术，同时学习 STL 公式的结构和参数，提高了对于需求挖掘的有效性，进一步推动了在计算机物理系统中的研究。

May, 2024

本文介绍一种基于 funnel functions 的可行强化学习算法，用于实现连续状态空间中 STL 规范的鲁棒满足，并在摆和移动机器人示例上演示了该方法的实用性。

Nov, 2022

通过直接学习神经网络控制器以满足信号时间逻辑 (STL) 的要求，以确保长期机器人任务的安全性和满足时间规范的挑战。同时，采用备用策略以保证控制器故障时的安全性。该方法可以适应不同的初始条件和环境参数，并在复杂的 STL 规范任务中以 10 倍至 100 倍速度快于传统方法。

Sep, 2023

本文主要介绍了一种用于从有限集的正面和负面例子中学习复杂系统可解释性描述的算法，通过在 IEEE 标准时间逻辑 PSL (Property Specification Language) 中学习公式来解决此问题，并比较了与现有 LTL 学习算法的效果。

Feb, 2020

该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

Oct, 2023