Formal Logic Enhanced AI and Deep Learning

How can formal specifications be integrated into learning-based AI to improve robustness, fairness, safety, and security in intelligent systems?

We proposed a federated learning training paradigm, called FedSTL, which enhances personalized client performance by encouraging model predictions to align with automatically inferred temporal logic properties. This approach enables collaboration among clients that share similar symbolic characteristics, improving robustness under heterogeneous and non-IID data distributions.

In addition, we incorporated signal temporal logic constraints to guide deep learning predictors toward fairer outputs. In this work, fairness properties related to demographic factors, such as age and median household income, were formally encoded for urban service allocation.

Building upon these contributions, my ongoing research extends the role of formal specifications from post-hoc analysis to a preventative security mechanism for cyber-physical systems. Specifically, I aim to develop a novel deep learning framework that integrates formal specifications into generative and diffusion-based models. This framework is designed to repair compromised or adversarially perturbed inputs by projecting them back onto the logical constraint set before downstream prediction. By embedding specification-driven correction into the learning pipeline, this approach moves beyond post-hoc detection toward proactive security, safety, and fairness guarantees in AI-enabled cyber-physical systems.

Related Publications

  • Formal Logic-Guided Harnessing Heterogeneous Fairness Rules in Smart Cities
    Ziyan An, Yiqi Zhao, Xuqing Gao, Ayan Mukhopadhyay, and Meiyi Ma
    ACM Transactions on Cyber-Physical Systems, 2025
  • Formal Logic Enabled Personalized Federated Learning through Property Inference
    Ziyan An, Taylor T. Johnson, and Meiyi Ma
    Proceedings of the AAAI Conference on Artificial Intelligence, 2024
  • FairGuard: Harness Logic-Based Fairness Rules in Smart Cities
    Yiqi Zhao, Ziyan An, Xuqing Gao, Ayan Mukhopadhyay, and Meiyi Ma
    Proceedings of the 8th ACM/IEEE Conference on Internet of Things Design and Implementation (IoTDI), 2023
FedSTL framework
Figure 1: FedSTL infers temporal logic properties from each client's data, then uses them to group clients with similar behavior and guide aggregation and client selection during federated training.
FairGuard training and deployment pipeline
Figure 2: The FairGuard pipeline combats unfair model behavior by incorporating fairness requirements during training and enforcing them through Static and Dynamic FairGuard, producing fair predictions at both training and deployment time.