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
Data-Flow-Based Normalization Generation Algorithm of R1CS for Zero-Knowledge Proof. PRDC'23
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)
Trusted Multi-Model Collaborative Work Platform
Logic rule mining algorithm based on reinforcement learning for knowledge graphs.
LLM based logic program generation and simulation.
AI4Math, AI4Sciences, AI4Engineering.
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.
Guoqiang Li
Last modified: Monday, Oct. 2, 2023.