Efficient Representation of Numerical Optimization Problems for SNARKs
Efficient Representation of Numerical Optimization Problems for SNARKs
复制标题
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Sebastian Angel;A. Blumberg;Eleftherios Ioannidis;Jess Woods
中科院分区：
文献类型：
--
作者：
Sebastian Angel;A. Blumberg;Eleftherios Ioannidis;Jess Woods
.本文介绍了Otti，一个通用的编译器（zk）SNARKs，提供支持数值优化问题。Otti为包含优化问题的程序提供了有效的算术化，包括线性规划（LP），半定规划（SDP）和广泛的随机梯度下降（SGD）实例。数值优化是一个基本的算法构建块：应用包括调度和资源分配任务，近似NP难题，以及神经网络的训练。Otti将用C语言子集编写的任意程序作为输入，这些程序包含通过易于使用的API艾德的优化问题。然后，Otti自动生成rank-1约束萨蒂斯性（R1 CS）实例，这些实例表达了这些程序的简洁转换。正确执行转换后的程序意味着原始优化问题的解决方案的最优性。我们对真实的基准测试的评估表明，奥蒂，实例化的斯巴达证明系统，可以证明最优的解决方案在零知识在短短100毫秒超过4个数量级的速度比现有的方法。
. This paper introduces Otti, a general-purpose compiler for (zk)SNARKs that provides support for numerical optimization problems. Otti produces efficient arithmetizations of programs that contain optimization problems including linear programming (LP), semi-definite programming (SDP), and a broad class of stochastic gradient descent (SGD) instances. Numerical optimization is a fundamental algorithmic building block: applications include scheduling and resource allocation tasks, approximations to NP-hard problems, and training of neural networks. Otti takes as input arbitrary programs written in a subset of C that contain optimization problems specified via an easy-to-use API. Otti then automatically produces rank-1 constraint satisfiability (R1CS) instances that express a succinct transformation of those programs. Correct execution of the transformed program implies the optimality of the solution to the original optimization problem. Our evaluation on real benchmarks shows that Otti, instantiated with the Spartan proof system, can prove the optimality of solutions in zero-knowledge in as little as 100 ms—over 4 orders of magnitude faster than existing approaches.