Fuqi Jia (贾富琦)

State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
#4 South Fourth St., Zhong Guan Cun
Beijing, China 100190
Email: jiafq@ios.ac.cn

Fuqi Jia

Short Bio

I am currently a PhD student in Computer Science and Technology at the University of Chinese Academy of Sciences (UCAS) and doing my research at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, under the supervision of Prof. Jian Zhang. From 2024 to 2025, I servied as a visiting PhD student at Stanford University, supervised by Clark Barrett. Before that, I received my B.S. degree in Computer Science and Technology from Jilin University (JLU) in 2020.

My research interests include the theory, algorithm and application of automated reasoning, constraint solving and optimization, as well as the integration of symbolic reasoning and machine learning.

Education

University of Chinese Academy of Sciences
Ph.D. Student
2020-2026 (Expected)
Stanford University
Visiting Ph.D. Student
2024-2025
Jilin University
B.S. Student
2016-2020

Recent News

Publications

(* indicates equal contribution)

A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic
Fuqi Jia, Yuhang Dong, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, Jian Zhang
AAAI Conference on Artificial Intelligence (AAAI), 2025
PDF Code
A Theory-Agnostic SMT Sampling Framework
Fuqi Jia, Clark Barrett, Pei Huang, Feifei Ma and Jian Zhang
Formal Methods in Computer-Aided Design (FMCAD, Student Forum), 2024
PDF Code
Automatic Construction of HD Maps for Simulation-Based Testing of Autonomous Driving Systems
Siqi Wang, Changwen Li, Tiantian Sun, Fuqi Jia, Rongjie Yan, Jun Yan
Theoretical Aspects of Software Engineering (TASE), 2024
PDF Code
Parallel Verification for δ-Equivalence of Neural Network Quantization
Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia, Clark Barrett
International Symposium on AI Verification (SAIV), 2024
PDF Code
Investigating the Existence of Holey Latin Squares via Satisfiability Testing
Minghao Liu, Rui Han, Fuqi Jia, Pei Huang, Feifei Ma, Hantao Zhang, Jian Zhang
Pacific Rim International Conference on Artificial Intelligence (PRICAI), 2023
PDF Code
Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
Fuqi Jia*, Yuhang Dong*, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang
Conference on Neural Information Processing Systems (NeurIPS), 2023
PDF Code
Improving Bit-Blasting for Nonlinear Integer Constraints
Fuqi Jia, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, Jian Zhang
ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2023
🏅 ACM SIGSOFT Distinguished Paper Award
PDF Code
PSMT: Satisfiability Modulo Theories Meets Probability Distribution
Fuqi Jia*, Rui Han*, Xutong Ma, Baoquan Cui, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang
IEEE/ACM International Conference on Automated Software Engineering (ASE, NIER Track), 2023
PDF Code
NRAgo: Solving SMT(NRA) Formulas with Gradient-based Optimization
Minghao Liu*, Kunhang Lv*, Pei Huang, Rui Han, Fuqi Jia, Yu Zhang, Feifei Ma, Jian Zhang
IEEE/ACM International Conference on Automated Software Engineering (ASE, Tool Demo Track), 2023
PDF Code
Can Graph Neural Networks Learn to Solve the MaxSAT Problem?
Minghao Liu, Pei Huang, Fuqi Jia, Fan Zhang, Yuchen Sun, Shaowei Cai, Feifei Ma, Jian Zhang
AAAI Conference on Artificial Intelligence (AAAI), Student Abstract and Poster Program, 2023
🏅 Best Student Abstract Honorable Mention Award
PDF Code
ε-weakened Robustness of Deep Neural Networks
Pei Huang*, Yuting Yang*, Minghao Liu, Fuqi Jia, Feifei Ma, Jian Zhang
ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2022
PDF Code
Word Level Robustness Enhancement: Fight Perturbation with Perturbation
Pei Huang*, Yuting Yang*, Fuqi Jia, Minghao Liu, FeiFei Ma, Jian Zhang
AAAI Conference on Artificial Intelligence (AAAI), 2022
PDF Code

Open Source Projects

SMTParser
A frontend for parsing and processing SMT-LIB / OMT format formulas, supporting C++ interfaces.
Code
BLAN
BLAN: Bit-bLAsting solving Non-linear integer constraints.
Code
CDCL(OCAC)
CDCL(OCAC): A complete algorithm for optimization modulo nonlinear real arithmetic.
Code
Splitwise-MILP
The Splitwise-like algorithm for sharing expenses using MILP encoding.
Code

Selected Awards & Scholarships

Outstanding Doctoral Student, Chinasoft 2023, 2023.11.
National Scholarship of China, 2023.10.
First Prize Scholarship of UCAS, 2023.10.
SMT Competition, QF_NIA Single Query / Model Validation Track, 2nd Place (Main Author), 2023.08.
ACM SIGSOFT Distinguished Paper Award, ISSTA 2023, 2023.07.

Presentations

Conference Talk Improving Bit-Blasting for Nonlinear Integer Constraints, ISSTA 2023, Virtual Event.
Conference Talk PSMT: Satisfiability Modulo Theories Meets Probability Distribution, ASE 2023, Luxembourg.
Conference Talk NRAgo: Solving SMT(NRA) Formulas with Gradient-based Optimization, ASE 2023, Luxembourg.
Seminar Talk Satisfiability and Deep Learning, Applied Mathematics Seminar for Youth, Peking University, Beijing, China.
Seminar Talk Solving Reasoning Problems with Neuro-Symbolic Methods, Dagstuhl Seminar 23471, Dagstuhl, Germany.
Seminar Talk Improving SMT Solving via Incorporating More Techniques, Dagstuhl Seminar 23471, Dagstuhl, Germany.
Conference Talk A Theory-Agnostic SMT Sampling Framework (Poster), FMCAD 2024, Prague, Czech Republic.

Last updated: 06/11/2025