PREFACE

I am running a mini academic group called VAST, named after Verification And Software Technology. 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

  • Privacy-preserved formal verification
  • LLM inference in ZKVM
  • Privacy-preserved dataset quality estimation


    • Dependable ZK Virtual Machine

  • ZKVM and continuously new versions.

    • 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

  • Methodology and Implementation of Formal Verification on Circuit Programs for Zero-Knowledge Proofs, NSFC General Program, 2026-2029
  • SAT Algorithm Theory and Novel Solvers, NSFC Key Program, 2026-2030
  • 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

  • ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs. ICFEM'25
  • 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

  • Certified Local Transferability for Evaluating Adversarial Attacks. IEEE Trans. Artif. Intell., 2025
  • MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression. CoRR abs/2506.04268
  • HOBAT: Batch Verification for Homogeneous Structural Neural Networks. ASE'23

    • KNOWLEDGE VERIFICATION

    Solving Computationally Intractable Problems in LLM

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

    • Agent Performance Evaluation Platform


  • LLM/Agent evaluations in various dimensions.

    • 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

  • Co-Eval: Augmenting LLM-based Evaluation with Machine Metrics. EMNLP'25
  • CrossPyEval: Enhancing LLM-based Evaluation of Low-Resource Code via Code Translation. ACML'25
  • 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
  • Can Language Models Pretend Solvers? Logic Code Simulation with LLMs. SETTA'24

    • Guoqiang Li
    Last modified: Saturday, Sep. 13, 2025.