本文探讨了学习线性时序逻辑 (LTL) 公式的计算复杂性,并构建了 LTL 的片段逼近算法,并对许多片段证明了 NP 完全性。
Feb, 2021
本文总结了两种不同的问题设置中,从正面或反面的示例中学习 LTL 公式的两种方法,第一种方法假设示例标记有噪声,第二种方法则考虑在仅给出正面示例的情况下推断有意义的 LTL 公式,所提出的方法提供了解决上述问题的不同算法,以及推断时的其他时间性质描述,如信号时间逻辑或确定性有限自动机。
Dec, 2022
该论文提出了两种学习 Linear Temporal Logic(LTL)公式的新算法,该算法通过将学习任务简化为命题布尔逻辑中的一系列可满足问题来实现,并且验证了这两种算法在合成基准测试和领导者选举协议的执行理解方面的优异表现。
Jun, 2018
本文主要介绍了一种用于从有限集的正面和负面例子中学习复杂系统可解释性描述的算法,通过在 IEEE 标准时间逻辑 PSL (Property Specification Language) 中学习公式来解决此问题,并比较了与现有 LTL 学习算法的效果。
Feb, 2020
该论文提出了两种算法:第一种使用 MaxSAT 求解器在高噪声数据下推导出最小 LTL 公式,第二种算法则基于第一种算法使用决策树学习算法推导出 LTL 公式的决策树。这些算法能够高效地提取简明的 LTL 描述。
Apr, 2021
本文探讨黑盒系统建模中使用有限状态自动机和线性时态逻辑公式的方法,通过正例学习建立有意义的、最小化的模型。作者提出了符号方法和反例引导方法两种学习方式,并在合成数据上进行评估。
Sep, 2022
本文探讨了神经符号计算中的两个基本问题:深度学习是否能够端到端地解决逻辑中的挑战性问题,以及神经网络是否能够学习逻辑的语义。研究重点是线性时间暂态逻辑(LTL),通过训练 Transformer 来直接预测给定 LTL 公式的解,使用传统求解器产生的经典解决方案生成训练数据,研究表明,使用这些特定的解决方案进行训练已足够。 Transformers 甚至可以预测在文献基准测试中,经典求解器超时的公式的解,它也可以推广到逻辑的语义,虽然与经典求解器找到的解有所不同,但仍可以正确地预测大多数公式的解。
Mar, 2020
本论文提出了一种新的算法来解决线性时间逻辑(LTL)公式学习问题,可以构建比之前更大的公式,并且可实现任意时刻输出结果,性能较好。通过开源实现和公开基准测试来评估算法性能。
Oct, 2021
使用 GPU 加速的基于枚举程序合成的 LTL 学习器在处理追踪数据时比现有技术要快 46 倍,并且可以处理比现有学习器多 2048 倍的追踪数据。
Feb, 2024
本文提出一种基于学习的方法,通过算法生成 LTL 公式,并将其转换为结构化英语进而利用现代大型语言模型的改写功能来合成自然语言命令,从而减少人工数据依赖,以 75%的准确率将自然语言命令翻译成 LTL 规范,并发现该翻译的公式能够用于长视距的,多阶段任务的规划(以 12D 四旋翼为例)。
Mar, 2023