| The WhitePaper Reading Club | SEP 2025 |
|---|---|
| Dynamic ZK-Snarks: Deep Prove | Kashish Shah (Lagrange), Rongxin (WPRC) |
Summary
Dynamic zk-SNARKs make cryptographic proofs updatable, enabling Lagrange’s DeepProve to provide real-time, verifiable AI inferences for evolving large language models (LLMs).
Why This Is Important
AI systems retrain constantly—dynamic proofs allow users, regulators, and stakeholders to trust outputs without recomputing heavy proofs from scratch, unlocking verifiable AI in finance, healthcare, defense, and beyond.
Question: What is the thing that it’s trying to prove? That the LLM computation ran through the model’s weights correctly?
Key Innovation
Traditional zk-SNARKs are static; every data/model change requires a full proof recomputation. Dynamic zk-SNARKs introduce an update algorithm that incrementally modifies proofs when inputs shift slightly (e.g., small weight updates in an LLM). Integrated into DeepProve, this means AI verifiability can keep pace with live model retraining and inference
Overview
Dynamic zk-SNARKs (Wang, Papamanthou, Srinivasan, Papadopoulos, IACR 2024/1566) extend classic SNARKs with an efficient update step: given a valid proof for an old state, you can update it to a new state in sublinear/polylogarithmic time if changes are small. Lagrange uses these in DeepProve to scale zero-knowledge proofs from static MLP/CNN models to full transformer LLMs like GPT-2 and LLAMA. The result: a system where AI outputs can be provably correct, private, and auditable in real-time without bottlenecking performance
Background
(i) zk-SNARKs: Succinct zero-knowledge proofs that allow verifiable computation. (ii) Static vs Dynamic: Groth16/Plonk require recomputation per update; dynamic SNARKs allow incremental updates. (iii) Dynamo / Dynaverse / Dynalog: Building blocks enabling relaxed permutation proofs and polylogarithmic update times . (iv) DeepProve: Lagrange’s zkML system that proves full LLM inference (token-by-token, autoregressive) with dedicated inference engines
Team
Opinions
(To be added)
Components
(Key Innovations - focus on the innovations, and key parts)
| Dynamo – Relaxed Permutation Proofs | (i) Dynamo is a zk-SNARK designed for relaxed permutation relations - instead of proving a perfect permutation, it proves an “almost permutation” with “localized differences”. (ii) This lets proofs update efficiently when only small portions of data change (e.g., a few rows in a matrix or weights in a neural net). (iii) Dynamo serves as the foundation for dynamic updates, making the otherwise global effect of changes localized to specific vectors.Question Are model updates usually small adjustments to the model weights? |
|---|---|
| Dynaverse – Sublinear Updates | (i) Builds on Dynamo by separating “ vectors” into smaller parts, so updates touch only a fraction of the total proof. (ii) Achieves O(n log n) update time - instead of recomputing for all n constraints, updates scale much slower. (iii) Keeps proof sizes constant (O(1)) through compression with static zk-SNARKs. Question How does it generate static proofs?(iv) Practical example: if a blockchain state changes slightly, the proof update time depends only on the number of changed accounts, not the entire ledger. |
| Dynalog | (i) Uses a hierarchical “waterfall” data structure to keep track of updates across multiple levels. (ii) Guarantees polylogarithmic update time (O(log³n)) while proofs remain succinct. (iii) Ensures that even for large datasets like LLM weights (billions of parameters), small local updates can be efficiently adjusted in proofs without recomputation. (iv) This is critical for ML retraining cycles, where only subsets of weights change. |
| DeepProve Integration – Full LLM zkML | (i) Dynamic zk-SNARKs extend DeepProve from handling static models (CNNs, MLPs) to transformers like GPT-2 and LLAMA . (ii) New proof-friendly layers were introduced: Softmax, LayerNorm, GELU, QKV attention, embedding layers—all provable under zero-knowledge. (iii) Adds support for GGUF, a widely used LLM format - developers can import real-world models from HuggingFace into DeepProve and generate proofs of inference without special pipelines. Note:Huge for developer experience. (iv) A dedicated LLM inference engine handles “token-by-token autoregressive computation” - proving full sequence outputs. |
| Real-world Applications (Sectoral Use Cases) | (i) Finance: Regulators or auditors can verify that model-driven trading complies with fairness and risk policies without exposing proprietary models. (ii) Healthcare: Medical AI decisions can be audited for compliance and bias while protecting sensitive patient data. (iii) Defense & Infrastructure: Ensure AI follows constraints (e.g., in mission-critical or autonomous control) without leaking operational parameters. (iv) AI-as-a-Service: Cloud providers offering inference APIs can prove correctness to customers, avoiding trust assumptions. |
| Competitive Landscape+Barriers & Challenges: | (i) Other approaches like recursive SNARKs or specialized zkML systems (e.g., zkLLM research) exist, but they are often either too slow (linear-time updates) or lack strong security guarantees (heuristics with recursion). Lagrange’s approach provides provable efficiency + security under q-DLOG assumptions . (ii) Projects like zkML Coprocessors or MPC-based verifiability are adjacent, but dynamic zk-SNARKs are unique in offering real-time updatability.(a) Proof generation for full LLM inference is still heavy — even with optimizations, scaling to GPT-4 class models remains a long-term goal. (Market education: most enterprises don’t yet understand zkML, so adoption may follow high-regulation sectors first (finance, defense, healthcare). (b) Hardware requirements: Distributed proving (GPU farms, cloud-scale provers) may be necessary for industrial adoption |
Questions
Q: What is the thing that it’s trying to prove? That the LLM computation ran through the model’s weights correctly?
A: DeepProve can be used to prove that the output of the LLM came from running the correct model by ensuring privacy of the underlying model
Q: Are model updates usually small adjustments to the model weights?
A: Yes, generally during retraining or fine-tuning the updates involve small adjustments using optimization methods to iteratively improve performance and efficiency. That is also the case for sequential token generation through inference where each token updates state in the transformer which can be treated as a small change in witness data. Whenever the changes aren't small, there is always an option to recompute the proof.
Q: How does it generate static proofs?
A: It generates static proofs using a static zk-SNARK like Groth16 by aggregating sqrt(m) subproofs into a single succint proof.