6 papers
Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis
Shichen Huang, Zhenghe Jiang, Yi Jiang +3
Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implem…
MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling
Jiacheng Chen, Xinyu Zhang, Shunkai Zhang +20
We present MaxProof, a population-level test-time scaling framework for competition-level mathematical proof in the MiniMax-M3 series. M3 first trains three proof-oriented capabili…
Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation
Jingyang Li, Xin Chen, Hongfei Fu +1
The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a proba…
Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification
Jingyang Li, Fu Song, Guoqiang Li
Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations, necessitating formal verification for safety-critical deployment. To ad…
SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression
Jingyang Li, Fu Song, Guoqiang Li
Deploying Deep Neural Networks (DNNs) on resource-constrained embedded systems requires aggressive model compression techniques like quantization and pruning. However, ensuring tha…
MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression
Jingyang Li, Guoqiang Li
The rapid development of deep learning has led to challenges in deploying neural networks on edge devices, mainly due to their high memory and runtime complexity. Network compressi…