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.



    • 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


    Guoqiang Li
    Last modified: Monday, Oct. 2, 2023.