可微分的时间逻辑公式推理
本文探讨了神经符号计算中的两个基本问题：深度学习是否能够端到端地解决逻辑中的挑战性问题，以及神经网络是否能够学习逻辑的语义。研究重点是线性时间暂态逻辑（LTL），通过训练 Transformer 来直接预测给定 LTL 公式的解，使用传统求解器产生的经典解决方案生成训练数据，研究表明，使用这些特定的解决方案进行训练已足够。 Transformers 甚至可以预测在文献基准测试中，经典求解器超时的公式的解，它也可以推广到逻辑的语义，虽然与经典求解器找到的解有所不同，但仍可以正确地预测大多数公式的解。
Mar, 2020
我们提出了一种新的框架，无缝提供神经网络（学习）和符号逻辑（知识和推理）的关键属性，每个神经元都有权重实值逻辑公式的组成部分，得到了高度可解释的分离表示，推理是全向的而不是集中在预定义的目标变量上，对应于逻辑推理，包括经典的一阶逻辑定理证明作为特殊情况。
Jun, 2020
本研究旨在提高对不一致和不确定数据的推理能力，并着重探讨历史科学中常见的带时间间隔的知识图形数据。我们提出了关于新的时间马尔科夫逻辑网络（TMLN）的语义原理，旨在实现高效的最大后验推理，并扩展马尔科夫逻辑网络（MLN）以涵盖不确定的时间事实和规则，并研究了不同时间公式之间的全局和局部时间（不）一致性关系。然后，我们提出了新的时间参数语义，可以组合多个子函数，使用不同的评估策略。最后，我们介绍了语义必须遵守的限制，以满足我们的原则。
Nov, 2022
TLINet 是一个神经符号框架，用于学习 Signal Temporal Logic 公式。该框架不仅学习 STL 公式的结构，还学习参数，具有解释性、紧凑性、表达能力丰富和计算效率高等优势。
May, 2024
本文提出了一种基于定理证明的方法，在神经网络的训练中规范和生成时间逻辑约束。通过 Isabelle 定理证明器的高阶逻辑，形式化嵌入线性时间逻辑，提出了一个损失函数，并使用 OCaml 版本制作的 PyTorch 模型进行了训练。结果表明，该算法在动态运动中达到预期效果，且避免了直接在 Python 这种编程语言中实现逻辑方面带来的许多风险。
Jul, 2022
本文讨论了在 Markov 决策过程中，使用 LTL 的公式作为代理规划的规范，通过形成多目标优化问题，从 MDP 中演示的行为轨迹中推断 LTL 规范，利用遗传编程解决该问题的有效性进行了证明。
Oct, 2017
介绍了一种将深度强化学习与时间逻辑相结合的神经符号代理，以实现形式化规定指令的系统性零射 (就是指未曾见过的情况)。研究证明，卷积层的架构在泛化新指令时发挥了关键作用，并证明通过学习少量训练样例，可以从抽象操作符中实现系统化的学习。
Jun, 2020
提出自回归模型，从系统追踪中生成线性时间逻辑公式，用于解决规范挖掘问题，并使用多种架构和度量方法进行实验证明其有效性。
May, 2024
本文提供了一种系统的方法来合成时序逻辑公式的语法结构和参数，其中利用了一种新颖的进化算法来学习公式的结构，然后对候选公式的平均鲁棒性执行参数综合，以应对动力系统的异常轨迹检测和无效呼吸努力的表征两个案例研究。
Nov, 2017