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.
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.
