PRODeep

PRODeep is a platform for robustness verification of deep neural networks (DNNs). It incorporates constraint-based, abstraction-based, and optimization-based robustness verification algorithms. It has a modular architecture, enabling easy comparison of different algorithms.

Significantly, PRODeep provides a user-friendly GUI, visualizing both inputs and outputs and providing an intuitive way to analyze the robustness properties. It is easy to get started with, so you can easily design some experiments to evaluate the robustness properties of your DNNs.

The screencast on YouTube will show the workflow of our tool; we also provide videos presenting PRODeep and instructions to install it.

Please feel free to contact us for any further information on PRODeep you might need.

Publications

• Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification, Li, J.; Liu, J.; Yang, P.; Chen, L.; Huang, X. and Zhang, L. In SAS, pages 296-319, LNCS 11822, 2019.
• PRODeep: a platform for robustness verification of deep neural networks. Renjue Li, Jianlin Li, Cheng-Chao Huang, Pengfei Yang, Xiaowei Huang, Lijun Zhang, Bai Xue, and Holger Hermanns. In Proceedings of the ESEC/FSE 2020.
• Improving Neural Network Verification through Spurious Region Guided Refinement. Yang, P., Li, R., Li, J., Huang, C. C., Wang, J., Sun, J., Xue, B., Zhang, L. (2020). arXiv preprint arXiv:2010.07722.

External Publications

• An abstract domain for certifying neural networks. Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. 2019. Proc. ACM Program. Lang. 3, POPL, Article 41 (January 2019), 30 pages.
• Certifying geometric robustness of neural networks. Balunovic, M., Baader, M., Singh, G., Gehr, T., & Vechev, M. (2019). In Advances in Neural Information Processing Systems (pp. 15313-15323).
• Formal verification of piece-wise linear feed-forward neural networks. Ehlers, Ruediger. International Symposium on Automated Technology for Verification and Analysis. Springer, Cham, 2017.
• Reluplex: An efficient SMT solver for verifying deep neural networks. Katz, G., Barrett, C., Dill, D. L., Julian, K., & Kochenderfer, M. J. (2017, July). In International Conference on Computer Aided Verification (pp. 97-117). Springer, Cham.