形式逻辑与机器学习实验室（Formal Logic and Machine Learning），旨在探索基于形式逻辑的人工智能与基于机器学习的人工智能的结合。在以计算为本质特征的计算机这样的“大脑”之上，能否将形式逻辑与机器学习有机结合以辅助或者替代人的某些智能活动？如何将二者有机结合？这都是值得探索的问题。目前，实验室开展的工作包括：

基于Petri网与时序逻辑的并发系统模型检测研究。开展多纬度的系统建模，包括系统逻辑结构、数据操作、事件发生的时间约束、以及多方交互过程中的认知等，面向多方计算隐私安全协议、实时嵌入式系统、人机物系统等，以计算树逻辑、带有时间约束的计算树逻辑、带有知识/策略的计算树逻辑作为系统待验证性质的描述语言，开展相关的模型检测算法，特别是结合OBDD状态压缩技术的模型检测算法，开发相应的自动检测工具。

分布式实时操作系统研究。面向无人机协同系统，开展基于RUST语言的分布式实时操作系统内核的设计、开发与验证，注重异构多核、强实时、异步并发。

基于机器学习的多智能体研究。面向无人机协同系统，开展机器学习（特别是强化学习）、博弈论的多智能体研究，并实现向无人机真实场景的迁移。

基于机器学习的网络交易欺诈检测研究。从网络交易大数据中，使用机器学习挖掘合法/欺诈交易的行为模式与特征，自动检测欺诈交易。

机器学习的可解释性研究。特别是针对图神经网络，结合形式逻辑，研究模型的可解释性，为模型的预测结果提供合理的解释。