Abstract
We consider the problem of binary image generation with given properties. This problem arises in a number of practical applications, including generation of artificial porous medium for an electrode of lithium-ion batteries, for composed materials, etc. A generated image represents a porous medium and, as such, it is subject to two sets of constraints: topological constraints on the structure and process constraints on the physical process over this structure. To perform image generation we need to define a mapping from a porous medium to its physical process parameters. For a given geometry of a porous medium, this mapping can be done by solving a partial differential equation (PDE). However, embedding a PDE solver into the search procedure is computationally expensive. We use a binarized neural network to approximate a PDE solver. This allows us to encode the entire problem as a logical formula. Our main contribution is that, for the first time, we show that this problem can be tackled using decision procedures. Our experiments show that our model is able to produce random constrained images that satisfy both topological and process constraints.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Arunachalam, H., Korneev, S., Battiato, I., Onori, S.: Multiscale modeling approach to determine effective lithium-ion transport properties. In: 2017 American Control Conference (ACC), pp. 92–97, May 2017
Battiato, I., Tartakovsky, D.: Applicability regimes for macroscopic models of reactive transport in porous media. J. Contam. Hydrol. 120–121, 18–26 (2011)
Hermann, H., Elsner, A.: Geometric models for isotropic random porous media: a review. Adv. Mater. Sci. Eng. 2014 (2014)
Pyrcz, M., Deutsch, C.: Geostatistical reservoir modeling (2014)
Hornung, U. (ed.): Homogenization and Porous Media. Interdisciplinary Applied Mathematics, vol. 6. Springer, New York (1997). https://doi.org/10.1007/978-1-4612-1920-0
Goodfellow, I.J., Pouget-Abadie, J., Mirza, M., Xu, B., Warde-Farley, D., Ozair, S., Courville, A.C., Bengio, Y.: Generative adversarial nets. In: Ghahramani, Z., Welling, M., Cortes, C., Lawrence, N.D., Weinberger, K.Q. (eds.) Advances in Neural Information Processing Systems 27: Annual Conference on Neural Information Processing Systems 2014, 8–13 December 2014, Montreal, Quebec, Canada, pp. 2672–2680 (2014)
Goodfellow, I.J.: NIPS 2016 tutorial: generative adversarial networks. CoRR abs/1701.00160 (2017)
Osokin, A., Chessel, A., Salas, R.E.C., Vaggi, F.: GANs for biological image synthesis. In: 2017 IEEE International Conference on Computer Vision (ICCV), pp. 2252–2261, October 2017
Korneev, S.: Using convolutional neural network to calculate effective properties of porous electrode. https://sccs.stanford.edu/events/sccs-winter-seminar-dr-slava-korneev
Arunachalam, H., Korneev, S., Battiato, I.: Using convolutional neural network to calculate effective properties of porous electrode. J. Electrochem. Soc. (2018, in preparation to submit)
Radford, A., Metz, L., Chintala, S.: Unsupervised representation learning with deep convolutional generative adversarial networks. CoRR abs/1511.06434 (2015)
Chintala, S.: How to train a GAN? Tips and tricks to make GANs work. https://github.com/soumith/ganhacks
Luke de Oliveira, M.P., Nachman, B.: Tips and tricks for training GANs with physics constraints. In: Workshop at the 31st Conference on Neural Information Processing Systems (NIPS), Deep Learning for Physical Sciences, December 2017
Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. CoRR abs/1709.06662 (2017)
Hubara, I., Courbariaux, M., Soudry, D., El-Yaniv, R., Bengio, Y.: Binarized neural networks. In: Lee, D.D., Sugiyama, M., Luxburg, U.V., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29, pp. 4107–4115. Curran Associates Inc., Red Hook (2016)
Cheng, C., Nührenberg, G., Ruess, H.: Verification of binarized neural networks. CoRR abs/1710.03107 (2017)
Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: an efficient SMT solver for verifying deep neural networks. arXiv preprint arXiv:1702.01135 (2017)
Cheng, C.-H., Nührenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 251–268. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_18
Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3–29. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_1
Dao, T., Duong, K., Vrain, C.: Constrained clustering by constraint programming. Artif. Intell. 244, 70–94 (2017)
Ganji, M., Bailey, J., Stuckey, P.J.: A declarative approach to constrained community detection. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 477–494. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_31
Guns, T., Dries, A., Nijssen, S., Tack, G., Raedt, L.D.: Miningzinc: a declarative framework for constraint-based mining. Artif. Intell. 244, 6–29 (2017)
Luke de Oliveira, M.P., Nachman, B.: Generative adversarial networks for simulation. In: 18th International Workshop on Advanced Computing and Analysis Techniques in Physics Research, August 2017
Hu, Y., Gibson, E., Lee, L.-L., Xie, W., Barratt, D.C., Vercauteren, T., Noble, J.A.: Freehand ultrasound image simulation with spatially-conditioned generative adversarial networks. In: Cardoso, M.J., et al. (eds.) CMMI/SWITCH/RAMBO -2017. LNCS, vol. 10555, pp. 105–115. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67564-0_11
Ravanbakhsh, S., Lanusse, F., Mandelbaum, R., Schneider, J.G., Póczos, B.: Enabling dark energy science with deep generative models of galaxy images. In: Singh, S.P., Markovitch, S. (eds.) Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 4–9 February 2017, San Francisco, California, USA, pp. 1488–1494. AAAI Press (2017)
Deng, L., Jiao, P., Pei, J., Wu, Z., Li, G.: Gated XNOR networks: deep neural networks with ternary weights and activations under a unified discretization framework. CoRR abs/1705.09283 (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Korneev, S., Narodytska, N., Pulina, L., Tacchella, A., Bjorner, N., Sagiv, M. (2018). Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. In: Beyersdorff, O., Wintersteiger, C. (eds) Theory and Applications of Satisfiability Testing – SAT 2018. SAT 2018. Lecture Notes in Computer Science(), vol 10929. Springer, Cham. https://doi.org/10.1007/978-3-319-94144-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-319-94144-8_27
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94143-1
Online ISBN: 978-3-319-94144-8
eBook Packages: Computer ScienceComputer Science (R0)