### PREFACE

I am running a mini academic group, VAST, named after Verification and Software Technology, in our BASICS lab. Every research in our group is around formal verification, a complete mathematically analytical methodology for safety-critical systems. Specifically, we perform formal verification on program languages, intelligent systems, and knowledge.

We also pursue candidates interested in theoretical computer sciences and AI for sciences.

Current running projects are introduced as follows:

### PROGRAM VERIFICATION

**Formal Verification for ZKP Circuit Programming **

Program verification on circuit programming based on finite field algebra
Proveable compiler for circuit programming based on theorem proving
**Reference **

Automated Detection of Underconstrained Circuits for Zero-Knowledge Proofs, *PLDI'23*
Practical Security Analysis of Zero-Knowledge Proof Circuits, *USENIX Security'24*
Certifying Zero-Knowledge Circuits with Refinement Types, *S&P'24*
**Representative projects**

**Recent contribution in group **

RNA: R1CS Normalization Algorithm Based on Data Flow Graphs for Zero-Knowledge Proofs. *Formal Aspects of Computing*, 2024
AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs. * CoRR abs/2403.15676 *, 2024

### INTELLIGENT SYSTEM VERIFICATION

**Verification and Security for Non-Uniform Robustness of Deep Neural Networks **

**Formal Verification on Homogeneous Structural Deep Neural Networks **

Modeling potential adversarial attacks on intelligent systems based on non-uniform perturbations
Batch robustness verification technology for intelligent system update processes
Verification technology and tool implementation for robustness of non-uniform perturbations in intelligent systems
**Reference**

Adversarial Robustness with Non-Uniform Perturbations. *NeurIPS'21*
**Representative projects**

Scalable and Certifiable Verification of Deep-Learning Enabled Systems, NSFC-ISF Joint Program, 2021-2024
**Recent contribution in group **

HOBAT: Batch Verification for Homogeneous Structural Neural Networks. *ASE'23*

### KNOWLEDGE VERIFICATION

**Knowledge Argumented Logic System (KALOS)**

**Solving Computationally Intractable Problems in LLM**

**Trustworthy Multi-Model Collaborative Work Platform**

Logic rule mining algorithm based on reinforcement learning for knowledge graphs.
LLM based logic program generation and simulation.
AI4Math, AI4Science, AI4Engineering, AI4Education.
**Reference **

Neural Compositional Rule Learning for Knowledge Graph Reasoning. *ICLR'23*
LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. *Arkiv*, 2023
SoLA: Solver-Layer Adaption of LLM for Better Logic Reasoning. *Arkiv*, 2024
**Representative projects**

**Recent contribution in group **

Zero-Shot Construction of Chinese Medical Knowledge Graph with GPT-3.5-turbo and GPT-4. *ACM Trans. Manag. Inf. Syst. *, 2024
Can Language Models Pretend Solvers? Logic Code Simulation with LLMs. *CoRR abs/2403.16097*, 2024

*Guoqiang Li*

*Last modified: Monday, Oct. 2, 2023. *