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:


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


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