PREFACE

I am running a mini academic group called VAST, named after Verification And Software Technology, within our BASICS lab. All research conducted in our group revolves around formal verification, a comprehensive mathematically rigorous methodology for safety-critical systems. Specifically, we carry out formal verification on programming languages, intelligent systems, and knowledge bases.

Furthermore, we actively seek candidates with an interest in theoretical computer science and AI for sciences.

The current ongoing projects are introduced as follows:

PROGRAM VERIFICATION

FM4ZK: 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
  • Efficient counting solver implementation for circuit programming verification







    • ZK4FM, ZK4LLM

  • Logic derivation trees in ZKs
  • Proving LLM inference in extended ZAWA

    • Dependable ZK Virtual Machine

  • Batch host ZK proof with guest VM proofs

    • Reference

  • zkGPT: An Efficient Non-interactive Zero-knowledge Proof Framework for LLM Inference, USENIX Security'25
  • Proving UNSAT in Zero Knowledge, CCS'22
  • 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

  • Research on Universal Zero-Knowledge Virtual Machines and Efficient Blockchain Accumulators, main contributor, Special Project on Key Technologies in Blockchain, Shanghai Science and Technology Innovation Action Plan, 2024-2025

    • 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
  • ZKWASM: A ZKSNARK WASM Emulator. IEEE Trans. Serv. Comput., 2024

    • INTELLIGENT SYSTEM VERIFICATION

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

  • Modeling potential adversarial attacks on intelligent systems based on non-uniform perturbations
  • Verification technology and tool implementation for robustness of non-uniform perturbations in intelligent systems



    • Formal Verification on Homogeneous Structural Deep Neural Networks

  • Batch robustness verification technology for intelligent system update processes



    • Formal Verification on Intelligent Control 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) in Vertical Domains

  • Logic rule mining algorithm based on reinforcement learning for knowledge graphs.
  • AI4Engineering, AI4Education.



    • Solving Computationally Intractable Problems in LLM

  • LLM based language generation and simulation.
  • AI4Math, AI4Science.
  • LLM4FM, LLM4ZK.

    • Trustworthy Multi-Model Collaborative Work Platform



    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

  • DCE-LLM: Dead Code Elimination with Large Language Models. NAACL'25
  • Zero-Shot Construction of Chinese Medical Knowledge Graph with GPT-3.5-turbo and GPT-4. ACM Trans. Manag. Inf. Syst. , 2024
  • PIRTRE-C: A Two-Stage Retrieval and Reranking Enhanced Framework for Improving Chinese Psychological Counseling. MedAI'24 , 2024
  • Can Language Models Pretend Solvers? Logic Code Simulation with LLMs. SETTA'24

    • Guoqiang Li
    Last modified: Sunday, Aug. 25, 2024.