Home About Publications Software Teaching

Incorrect by Construction: Fine Tuning Neural Networks for Guaranteed Performance on Finite Sets of Examples

I. Papusha, R. Wu, J. Brulé, Y. Kouskoulas, D. Genin, and A. Schmidt

• Manuscript (FoMLAS 2020)
• Toolbox (lantern-smt)

Abstract

There is great interest in using formal methods to guarantee the reliability of deep neural networks. However, these techniques may also be used to implant carefully selected input-output pairs. We present initial results on a novel technique for using SMT solvers to fine tune the weights of a ReLU neural network to guarantee outcomes on a finite set of particular examples. This procedure can be used to ensure performance on key examples, but it could also be used to insert difficult-to-find incorrect examples that trigger unexpected performance. We demonstrate this approach by fine tuning an MNIST network to incorrectly classify a particular image and discuss the potential for the approach to compromise reliability of freely-shared machine learning models.

Citation

I. Papusha, R. Wu, J. Brulé, Y. Kouskoulas, D. Genin, and A. Schmidt. “Incorrect by Construction: Fine Tuning Neural Networks for Guaranteed Performance on Finite Sets of Examples,” Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), part of International Conference on Computer-Aided Verification (CAV), Los Angeles, CA, July 19, 2020.