Logical Approximation and Formal Verification of Neural Networks
Resumo
Explainability and formal verification of neural networks may be crucial when using these models to perform critical tasks. Pursuing explainability properties, we present a method for approximating neural networks by piecewise linear functions, which is a step to achieve a logical representation of the network. We also explain how such logical representations may be applied in the formal verification of some properties of neural networks. Furthermore, we present the results of an empirical experiment where the methods introduced are used in a case study.
Referências
Acharya, J., Diakonikolas, I., Li, J., and Schmidt, L. (2016). Fast algorithms for segmented regression. In Proceedings of the 33rd International Conference on International Conference on Machine Learning Volume 48, ICML’16, pages 2878–2886. JMLR.org.
Ansótegui, C., Bofill, M., Manyà, F., and Villaret, M. (2012). Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers. In 2012 IEEE 42nd International Symposium on Multiple-Valued Logic, pages 25–30.
Cignoli, R., D’Ottaviano, I., and Mundici, D. (2000). Algebraic Foundations of Many-Valued Reasoning. Trends in Logic. Springer Netherlands.
Finger, M. and Preto, S. (2020). Probably partially true: Satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Journal of Automated Reasoning, 64(7):1269–1286.
Hughes, R. B. and Anderson, M. R. (1996). Simplexity of the cube. Discret. Math., 158:99–150.
McNaughton, R. (1951). A theorem about infinite-valued sentential logic. Journal of Symbolic Logic, 16:1–13.
Mundici, D. (1994). A constructive proof of McNaughton’s theorem in infinite-valued logic. The Journal of Symbolic Logic, 59(2):596–602.
Preto, S. and Finger, M. (2020). An efficient algorithm for representing piecewise linear functions into logic. Electronic Notes in Theoretical Computer Science, 351:167–186. Proceedings of LSFA 2020, the 15th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2020).
Preto, S. and Finger, M. (2022). Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability. Mathematical Structures in Computer Science, 32(9):1119–1144.
Preto, S. and Finger, M. (2023a). Effective reasoning over neural networks using Łukasiewicz logic. In Hitzler, P., Kamruzzaman Sarker, M., and Eberhart, A., editors, Compendium of Neurosymbolic Artificial Intelligence, volume 369 of Frontiers in Artificial Intelligence and Applications, chapter 28, pages 609–630. IOS Press.
Preto, S. and Finger, M. (2023b). Proving properties of binary classification neural networks via Łukasiewicz logic. Logic Journal of the IGPL, 31(5):805–821.
Weierstrass, K. (1885). Uber die analytische darstellbarkeit sogenannter willkrlicher functionen einer reellen vernderlichen.
Ansótegui, C., Bofill, M., Manyà, F., and Villaret, M. (2012). Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers. In 2012 IEEE 42nd International Symposium on Multiple-Valued Logic, pages 25–30.
Cignoli, R., D’Ottaviano, I., and Mundici, D. (2000). Algebraic Foundations of Many-Valued Reasoning. Trends in Logic. Springer Netherlands.
Finger, M. and Preto, S. (2020). Probably partially true: Satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Journal of Automated Reasoning, 64(7):1269–1286.
Hughes, R. B. and Anderson, M. R. (1996). Simplexity of the cube. Discret. Math., 158:99–150.
McNaughton, R. (1951). A theorem about infinite-valued sentential logic. Journal of Symbolic Logic, 16:1–13.
Mundici, D. (1994). A constructive proof of McNaughton’s theorem in infinite-valued logic. The Journal of Symbolic Logic, 59(2):596–602.
Preto, S. and Finger, M. (2020). An efficient algorithm for representing piecewise linear functions into logic. Electronic Notes in Theoretical Computer Science, 351:167–186. Proceedings of LSFA 2020, the 15th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2020).
Preto, S. and Finger, M. (2022). Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability. Mathematical Structures in Computer Science, 32(9):1119–1144.
Preto, S. and Finger, M. (2023a). Effective reasoning over neural networks using Łukasiewicz logic. In Hitzler, P., Kamruzzaman Sarker, M., and Eberhart, A., editors, Compendium of Neurosymbolic Artificial Intelligence, volume 369 of Frontiers in Artificial Intelligence and Applications, chapter 28, pages 609–630. IOS Press.
Preto, S. and Finger, M. (2023b). Proving properties of binary classification neural networks via Łukasiewicz logic. Logic Journal of the IGPL, 31(5):805–821.
Weierstrass, K. (1885). Uber die analytische darstellbarkeit sogenannter willkrlicher functionen einer reellen vernderlichen.
Publicado
21/07/2024
Como Citar
LOBO, João; FINGER, Marcelo; PRETO, Sandro.
Logical Approximation and Formal Verification of Neural Networks. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 5. , 2024, Brasília/DF.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2024
.
p. 1-8.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2024.2347.
