Minghao Liu

Minghao Liu is a Postdoctoral Research Associate in the Department of Computer Science at the University of Oxford, working under the supervision of Prof. Marta Kwiatkowska and previously with Dr. Andrew Cropper. He is affiliated with the Artificial Intelligence and Machine Learning theme and the FAIR project at Oxford. His research integrates symbolic reasoning with machine learning, focusing on automated reasoning, constraint programming, and combinatorial optimization.

• PhD in Computer Science and Technology, University of Chinese Academy of Sciences (UCAS), 2023
• BSc in Computer Science and Technology, Northeast Normal University (NENU), 2017

His research interests span automated reasoning, constraint programming, combinatorial optimization, and the integration of symbolic reasoning with machine learning. He develops novel algorithms for SMT solving, optimization modulo theories, and neural-symbolic systems, often leveraging machine learning to enhance classical reasoning systems.

The recent publications show a strong trend in hybrid AI systems, particularly using graph neural networks to solve combinatorial problems like MaxSAT and Pseudo-Boolean Satisfiability. There is also a significant focus on improving solvers for nonlinear arithmetic and modal logics, often guided by reinforcement learning or probabilistic methods. His work bridges formal methods with deep learning, aiming to create more robust and scalable reasoning systems.

Notable scientific awards include:

• ACM SIGSOFT Distinguished Paper Award at ISSTA 2023
• Best Student Abstract Honorable Mention Award at AAAI 2023
• 2nd Place in SMT Competition (Nonlinear Real Arithmetic Track, 2022)
• Gold Medal in ACM-ICPC Asia Regional (2016)
• National Scholarship of China (2014)

Minghao Liu has been actively involved in academic service and teaching. He has served as a Class Tutor for Logic and Proof and Knowledge Representation and Reasoning, a Practical Demonstrator for Design and Analysis of Algorithms, and a Student Project Supervisor for Group Design Practical at Oxford. He was also a Teaching Assistant for Theoretical Computer Science at UCAS. He has received multiple scholarships and honors, reflecting his academic excellence. His service includes being a PC member for AAAI (2023–2025), ECAI 2024, and ICTAI 2023, and a reviewer for IEEE TNNLS, IEEE TKDE, and CSSE.

He is actively involved in research projects such as FAIR and maintains open-source implementations of his work on GitHub, including solvers for MaxSAT, SMT(NRA), and Holey Latin Squares, demonstrating strong software engineering and reproducibility practices.