PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial Inequalities

Constraints solvers play a significant role in the analysis, synthesis, and formal verification of complex cyber-physical systems. In this article, we study the problem of designing a scalable constraints solver for an important class of constraints named polynomial constraint inequalities (also known as nonlinear real arithmetic theory). In this article, we introduce a solver named PolyARBerNN that uses convex polynomials as abstractions for highly nonlinears polynomials. Such abstractions were previously shown to be powerful to prune the search space and restrict the usage of sound and complete solvers to small search spaces. Compared with the previous efforts on using convex abstractions, PolyARBerNN provides three main contributions namely (i) a neural network guided abstraction refinement procedure that helps selecting the right abstraction out of a set of pre-defined abstractions, (ii) a Bernstein polynomial-based search space pruning mechanism that can be used to compute tight estimates of the polynomial maximum and minimum values which can be used as an additional abstraction of the polynomials, and (iii) an optimizer that transforms polynomial objective functions into polynomial constraints (on the gradient of the objective function) whose solutions are guaranteed to be close to the global optima. These enhancements together allowed the PolyARBerNN solver to solve complex instances and scales more favorably compared to the state-of-the-art nonlinear real arithmetic solvers while maintaining the soundness and completeness of the resulting solver. In particular, our test benches show that PolyARBerNN achieved 100X speedup compared with Z3 8.9, Yices 2.6, and PVS (a solver that uses Bernstein expansion to solve multivariate polynomial constraints) on a variety of standard test benches. Finally, we implemented an optimizer called PolyAROpt that uses PolyARBerNN to solve constrained polynomial optimization problems. Numerical results show that PolyAROpt is able to solve high-dimensional and high order polynomial optimization problems with higher speed compared to the built-in optimizer in the Z3 8.9 solver.

约束求解器在复杂信息物理系统的分析、综合和形式验证中起着重要作用。在本文中，我们研究了为一类重要的约束（称为多项式约束不等式，也称为非线性实算术理论）设计可扩展约束求解器的问题。在本文中，我们介绍了一种名为PolyARBerNN的求解器，它使用凸多项式作为高度非线性多项式的抽象。先前已表明这种抽象在削减搜索空间以及将可靠且完备的求解器的使用限制在较小搜索空间方面是很有效的。与先前使用凸抽象的工作相比，PolyARBerNN提供了三个主要贡献，即（i）一种神经网络引导的抽象细化过程，它有助于从一组预定义的抽象中选择正确的抽象；（ii）一种基于伯恩斯坦多项式的搜索空间削减机制，可用于计算多项式最大值和最小值的精确估计，这些估计可作为多项式的额外抽象；（iii）一种优化器，它将多项式目标函数转换为多项式约束（关于目标函数的梯度），其解保证接近全局最优值。这些增强功能共同使PolyARBerNN求解器能够解决复杂实例，并且与最先进的非线性实算术求解器相比扩展性更好，同时保持所得求解器的可靠性和完备性。特别是，我们的测试平台表明，在各种标准测试平台上，与Z3 8.9、Yices 2.6和PVS（一种使用伯恩斯坦展开来解决多元多项式约束的求解器）相比，PolyARBerNN实现了100倍的加速。最后，我们实现了一种名为PolyAROpt的优化器，它使用PolyARBerNN来解决有约束的多项式优化问题。数值结果表明，与Z3 8.9求解器中的内置优化器相比，PolyAROpt能够以更高的速度解决高维和高阶多项式优化问题。