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.

Our current ongoing projects primarily focus on the integration of formal methods (FM), zero-knowledge proofs (ZK), and code intelligence (CI). A detailed introduction is provided below:

FORMAL METHODS (FM)

Program Invariant Generations

  • Complex invariant generations
  • Invariant generation by LLM

    • Formal Verification for ZKP Circuit Programming

  • Formal verification on ZKVM
  • 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







    • Formal Methods on Intelligence Control Systems

  • Formal verification on DNNs.
  • Formal verification on embodied intelligence systems.
  • Formal verification on autonomous driving systems

    • Representative projects

  • SAT Algorithm Theory and Novel Solvers, NSFC Key Program, 2026-2030
  • Scalable and Certifiable Verification of Deep-Learning Enabled Systems, main contributor, NSFC-ISF Joint Program, 2021-2024
  • Verification Models and Efficient Algorithms of Asynchronously Communicating Programs Based on Basic Parallel Processes, NSFC General Program, 2019-2022

    • Recent contribution in group

  • Array-Carrying Symbolic Execution for Function Contract Generation. FM'26
  • AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs. Formal Aspects of Computing, 2026
  • Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models. Science of Computer Programming, 2026
  • Affine Disjunctive Invariant Generation with Farkas' Lemma. VMCAI'26
  • HOBAT: Batch Verification for Homogeneous Structural Neural Networks. ASE'23

    • ZERO-KNOWLEDGE PROOFS (ZK)

    ZK4FM, ZK4DNN, ZK4LLM

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


    • Dependable ZK Virtual Machine

  • ZKVM and continuously new versions.

    • Representative projects

  • Methodology and Implementation of Formal Verification on Circuit Programs for Zero-Knowledge Proofs, NSFC General Program, 2026-2029
  • Research on Universal Zero-Knowledge Virtual Machines and Efficient Blockchain Accumulators, 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
  • ZKWASM: A ZKSNARK WASM Emulator. IEEE Trans. Serv. Comput., 2024

    • CODE INTELLIGENCE (CI)

    Artificial intelligence generated function (AIGF)

  • Agentic reinforcement learning for codes.
  • Trustworthy code agents.

    • Solving Computationally Intractable Problems in LLM

  • AI4TCS.
  • AI4Math, AI4Science.
  • LLM4FM, LLM4ZK.

    • Code Optimization

    Agent Performance Evaluation Platform


  • LLM/Agent evaluations in various dimensions.

    • Representative projects

    Recent contribution in group

  • DCoL-A: Agentic Dual Chain of Thinking Helps LLMs Pretend Logic Solvers. J. Syst. Archit., 2026
  • 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: Sunday, Mar. 15, 2026.