Volume 6 • Issue 1 • PP: 32–39 • 2026
Residuation–Galois Calculus for Exact Safety Preimages of Monotone Max–Plus Neural Networks
Open Access & Copyright
© 2026 The Author(s). Published by ASPG. This article is licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0).
View PDF Abstract
A proof-only calculus is developed for exact set abstraction and backward safety certification of monotone neural operators. A Galois insertion between concrete sets and interval boxes yields the best correct interval transformer. For every coordinatewise monotone map F, this transformer maps [ℓ,u] exactly to [F(ℓ),F(u)]; hence layerwise interval propagation is hull-exact for networks with nonnegative weights and isotone activations. The analysis is sharpened for max–plus layers T(x) =W ⊗x⊕b. Their upper safety preimages are either empty or principal ideals generated by the residualW\y, where (W\y)i = inf j:Wji>−∞(yj−Wji). Reverse residual propagation through a depth-L network computes the greatest input vector satisfying a prescribed upper output bound. Consequently, the largest weighted ℓ∞ radius around a nominal input is obtained in closed form, without optimization, branching, sampling, or relaxation. Soundness, maximality, compositionality, exactness, homogeneous collapse, and target-bound stability are proved. Four open problems concern signed architectures, two-sided class margins, residuated transformer attention, and completeness beyond boxes.
Keywords
References
[1] P. Cousot and R. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, pp. 238–252.
[2] P. Cousot and R. Cousot, “Systematic design of program analysis frameworks,” in Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1979, pp. 269–282.
[3] P. Cousot and R. Cousot, “Comparing the galois connection and widening/narrowing approaches to abstract interpretation,” in Programming Language Implementation and Logic Programming, ser. Lecture Notes in Computer Science, vol. 631. Springer, 1992, pp. 269– 295.
[4] P. Cousot and R. Cousot, “A galois connection calculus for abstract interpretation,” in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014, pp. 3–4.
[5] T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “ai2: Safety and robustness certification of neural networks with abstract interpretation,” in 2018 IEEE Symposium on Security and Privacy, 2018, pp. 3–18.
[6] M. Mirman, T. Gehr, and M. Vechev, “Differentiable abstract interpretation for provably robust neural networks,” in Proceedings of the 35th International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, vol. 80, 2018, pp. 3578–3586.
[7] G. Singh, T. Gehr, M. Mirman, M. Püschel, andM. Vechev, “Fast and effective robustness certification,” in Advances in Neural Information Processing Systems, vol. 31, 2018.
[8] G. Singh, T. Gehr, M. Püschel, and M. Vechev, “An abstract domain for certifying neural networks,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 41:1–41:30, 2019.
[9] H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” in Advances in Neural Information Processing Systems, vol. 31, 2018.
[10] S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “β-CROWN: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,” in Advances in Neural Information Processing Systems, vol. 34, 2021, pp. 29 909– 29 921.
[11] Z. Wang, A. Albarghouthi, G. Prakriya, and S. Jha, “Interval universal approximation for neural networks,” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–29, 2022.
[12] M. N. Müller, M. Fischer, R. Staab, and M. Vechev, “Abstract interpretation of fixpoint iterators with applications to neural networks,” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 786– 810, 2023.
[13] C. Zhou, R. A. Shaikh, Y. Li, and A. Farjudian, “A domain-theoretic framework for robustness analysis of neural networks,” Mathematical Structures in Computer Science, vol. 33, no. 2, pp. 68–105, 2023.
[14] J. Sill, “Monotonic networks,” in Advances in Neural Information Processing Systems, vol. 10, 1997, pp. 661– 667.
[15] S. You, D. Ding, K. Canini, J. Pfeifer, and M. Gupta, “Deep lattice networks and partial monotonic functions,” in Advances in Neural Information Processing Systems, vol. 30, 2017.
[16] D. Mikulincer and D. Reichman, “Size and depth of monotone neural networks: Interpolation and approximation,” in Advances in Neural Information Processing Systems, vol. 35, 2022, pp. 5522–5534.
[17] D. Runje and S. M. Shankaranarayana, “Constrained monotonic neural networks,” in Proceedings of the 40th International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, vol. 202, 2023, pp. 29 338–29 353.
[18] D. Sartor, A. Sinigaglia, and G. A. Susto, “Advancing constrained monotonic neural networks: Achieving universal approximation beyond bounded activations,” in Proceedings of the 42nd International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, vol. 267, 2025, pp. 52 995–53 018.
[19] L. Zhang, G. Naitzat, and L.-H. Lim, “Tropical geometry of deep neural networks,” in Proceedings of the 35th International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, vol. 80, 2018, pp. 5824–5832.
[20] P. Misiakos, G. Smyrnis, G. Retsinas, and P. Maragos, “Neural network approximation based on hausdorff distance of tropical zonotopes,” in International Conference on Learning Representations, 2022.
[21] P. Lezeau, T. Walker, Y. Cao, S. Bhatia, and A. Monod, “Tropical expressivity of neural networks,” arXiv preprint arXiv:2405.20174, 2024.
[22] J. Gunawardena, “An introduction to idempotency,” in Idempotency, J. Gunawardena, Ed. Cambridge University Press, 1998, pp. 1–49.
[23] P. Butkoviˇc, Max-Linear Systems: Theory and Algorithms, ser. Springer Monographs in Mathematics. Springer, 2010.
[24] N. Galatos, P. Jipsen, T. Kowalski, and H. Ono, Residuated Lattices: An Algebraic Glimpse at Substructural Logics, ser. Studies in Logic and the Foundations of Mathematics. Elsevier, 2007, vol. 151.
Cite This Article
Choose your preferred format
Publisher's Note
The statements, opinions, and data presented in this article are solely those of the author(s) and do not necessarily represent those of ASPG, the journal, or its editors. ASPG and the editors disclaim responsibility for any harm arising from the use of any ideas, methods, instructions, or products described in this article, to the fullest extent permitted by applicable law.