Paper 2021/1436

Efficient Representation of Numerical Optimization Problems for SNARKs

Sebastian Angel and Andrew J. Blumberg and Eleftherios Ioannidis and Jess Woods

Abstract

This paper introduces Otti, a general-purpose compiler for SNARKs that provides language-level 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 constraints satisfiability (R1CS) instances that express a succinct transformation of those pro- grams whose correct execution implies the optimality of the solution to the original optimization problem. Our experimental evaluation on real numerical solver benchmarks used by commercial LP, SDP, and SGD solvers shows that Otti, instantiated with the Spartan proof system, can prove the optimality of solutions in as little as 300 ms---over 4 orders of magnitude faster than existing approaches.