Griffith University
The vision of our research group on neural-symbolic reasoning is to pioneer the integration of Large Language Models (LLMs) with Formal Methods (FMs) to develop the next generation of trustworthy AI systems. While LLMs exhibit exceptional language understanding and adaptability, their unreliable outputs pose a major challenge. Conversely, FMs provide rigorous verification and reasoning but suffer from steep learning curves and scalability limitations. Our research aims to bridge this gap by leveraging FMs to enhance the reliability of LLMs -- ensuring AI-generated outputs are logically consistent -- while using LLMs to make FMs more accessible and efficient. This mutual enhancement will transform AI-driven software engineering, healthcare, finance, law and regulations, and mission-critical applications. By unifying these computational paradigms, we seek to advance neural-symbolic AI that is interpretable, verifiable, and practical for real-world deployment.
Read our ICML 2025 paper for technical details.
Deep integration of LLM with SMT solvers to ensure the AI's logical correctness.
Correct-by-construction LLM coder through program refinement calculus.
Fully automated LLM model checking agent for PAT.
Zixiao Zhao, Jing Sun, Zhe Hou, Zhiyuan Wei, Cheng-Hao Cai, Miao Qiao, Jin Song Dong: MaCTG: Multi-Agent Collaborative Thought Graph for Automatic Programming. IEEE/ACM International Conference on Software Engineering (ICSE) 2026.
Zhaoyu Liu, Kan Jiang, Murong Ma, Zhe Hou, Yun Lin, and Jin Song Dong: Few-Shot Precise Event Spotting via Unified Multi-Entity Graph and Distillation. The Annual AAAI Conference on Artificial Intelligence (AAAI), 2026.
Xinyue Zuo, Yifan Zhang, Hongshu Wang, Yufan Cai, Zhe Hou, Jing Sun, Jin Song Dong: PAT-Agent: Autoformalization for Model Checking. IEEE/ACM International Conference on Automated Software Engineering (ASE) 2025.
Yedi Zhang, Yufan Cai, Xinyue Zuo, Xiaokun Luan, Kailong Wang, Zhe Hou, Yifan Zhang, Zhiyuan Wei, Meng Sun, Jun Sun, Jing Sun, Jin Song Dong: Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods. International Conference on Machine Learning (ICML) 2025.
Yufan Cai, Zhe Hou, David Sanan, Xiaokun Luan, Yun Lin, Jun Sun, Jin Song Dong: Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2025.
Xiaokun Luan, David Sanan, Zhe Hou, Qiyuan Xu, Chengwei Liu, Yufan Cai, Yang Liu, Meng Sun: Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle. The ACM International Conference on the Foundations of Software Engineering (FSE) 2025.
Zhaoyu Liu, Kan Jiang, Murong Ma, Zhe Hou, Yun Lin, and Jin Song Dong: F3SET: Towards Analyzing Fast Frequent and Fine-grained Events From Videos. The International Conference on Learning Representations (ICLR), 2025.
Hadrien Bride, Cheng-Hao Cai, Jie Dong, Jin Song Dong, Zhe Hou, Seyedali Mirjalili, Jing Sun: Silas: A High-Performance Machine Learning Foundation for Logical Reasoning and Verification. Expert Systems With Applications, 2021.
