Pith. sign in

REVIEW 2 major objections 4 minor 40 references

Interval Certifications for Multilayered Perceptrons via Lattice Traversal

T0 review · 2 major / 4 minor · reviewed 2026-07-13 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Adversarial robustness for ReLU MLPs reduces to lattice traversal over intervals containing a given input, yielding both maximal sound and minimal complete certifications.

desk verdict Clean lattice reduction of interval robustness with a genuinely new dual (complete certificates) and a sharp poly-vs-intractable asymmetry; theory holds, experiments are tiny but only corroborative. read the letter →

arxiv 2607.08773 v1 pith:YDMXWNAP submitted 2026-04-09 cs.AI cs.LG

Merkouris Papamichail , Konstantinos Varsos , Giorgos Flouris , João Marques-Silva This is my paper
classification cs.AIcs.LG
keywords adversarialrobustnessintervalcertificationlatticetraversalMLPverificationsoundandcompletecertificatesReLUnetworksalgebra
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper shows that certifying the adversarial robustness of a multilayered perceptron can be recast as systematic movement through the lattice of all axis-aligned hyper-rectangles that contain a given input point. Two dual notions of certification are defined: a sound interval inside which the network’s prediction is guaranteed never to change, and a complete interval outside which the prediction is guaranteed to change. The authors introduce lattice operators that enlarge or shrink intervals by including or excluding counter-examples returned by a formal verifier; iterating these operators produces maximal sound certificates and the unique minimal complete certificate. They further prove an asymmetry in the associated optimisation problems: the minimal complete certificate can be recovered with a polynomial number of verifier calls, while computing a maximum-volume sound certificate is strongly intractable. When attention is restricted to symmetric (ℓ∞) balls the same problems become solvable by logarithmic binary search. An open-source implementation, ParallelepipedoNN, demonstrates the approach on MNIST and Fashion-MNIST networks.

What carries the argument

The ⊤-operator (bottom-up join of decision-surface points) that yields the unique minimal complete certification, the dual ⊥-operator (top-down exclusion of counter-examples) that yields a non-trivial sound certification, and the maximal-closure operator that expands any sound interval to a maximal one.

What would settle it

Run the complete-certification algorithm on a ReLU network whose decision region for the true class is known to be unbounded (for example a linear classifier with an open half-space); if the algorithm still returns a finite minimal interval, the compactness premise is unnecessary and the claim collapses.

Watch

Extended reading notes

Core claim

The space of all intervals containing a fixed input forms a complete lattice under inclusion; adversarial robustness is exactly the problem of traversing that lattice with a small family of refinement operators until a maximal sound or minimal complete element is reached, and the complete certificate is unique while the sound one is not.

Load-bearing premise

Every decision region of the classifier is assumed compact; if a region is unbounded the operators that produce a finite minimal complete certificate may fail to terminate or may return an infinite set.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper reduces adversarial robustness certification for ReLU MLPs to lattice traversal over the complete lattice of axis-aligned intervals containing a fixed input x. It defines sound certifications (perturbations inside I preserve the label) and the novel dual notion of complete certifications (exiting I is guaranteed to flip the label). Lattice operators (⊤ for unique minimal complete, ⊥ for non-trivial sound, and maximal closure) are realized by refine-and-verify loops that call a sound-and-complete verifier (Marabou). Complexity asymmetries are proved: minimal complete certificates are obtained in polynomially many oracle calls, while maximal sound certificates are strongly intractable (even ignoring verifier cost); both become logarithmic under the uniform-interval restriction. The open-source ParallelepipedoNN system implements the operators and is evaluated on two small MNIST/Fashion-MNIST MLPs.

Significance. If the claims hold, the work supplies a clean algebraic foundation for interval robustness that unifies existing sound-certification algorithms, introduces the previously unexamined complete-certification problem, and exhibits a sharp complexity dichotomy. The appendix contains fully explicit potential-function and reduction proofs (q-MER / Independent Set); the accompanying code and ONNX interface make the operators reproducible. These are genuine strengths for the AI-safety / formal-verification community. The experimental section is only corroborative, yet the theoretical guarantees already constitute a solid contribution.

major comments (2)
  1. Section 4 and Theorems 3–6 repeatedly invoke compactness of the decision surface Dc to guarantee termination of the refine-and-verify loops and uniqueness of the minimal complete certificate. While the paper works inside a compact feature box F, ReLU decision regions can be unbounded; a short discussion of what fails (or how the operators must be modified) when Dc is unbounded would strengthen the claim that the framework is fully general for MLPs.
  2. Table 3 and the accompanying text report 50–64 % timeouts for TDS / TDS+SDE on both data sets, together with networks of only ~25 k parameters. Because the central claims are theoretical, this does not invalidate them; nevertheless the empirical section currently provides only weak evidence that the lattice operators remain practical beyond toy scale. Either larger networks or a clearer statement that the experiments are merely illustrative would remove the mismatch between theory and practice.
minor comments (4)
  1. Definition 3 (exclusion operator /_δ) and the subsequent complexity statements leave the concrete choice of the infinitesimal δ somewhat informal; a short remark on how δ interacts with floating-point arithmetic in Marabou would help implementers.
  2. Table 1 comparison column “Non-Triv.” is marked ✓ only for the present work; a one-sentence clarification that prior convex-relaxation methods cannot decide non-triviality would make the table self-contained.
  3. Several figures (Fig. 1, Fig. 5, Fig. 6) are referenced before their captions fully explain the colour coding of lower/upper bounds; moving a short legend into the caption would improve readability.
  4. Typographical: “ParallelelpipedoNN” appears once (p. 18) instead of the consistent “ParallelepipedoNN”; also “Reasearch” in the affiliation line.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: lattice operators, uniqueness, and complexity results are derived from first-principles interval algebra and MILP encodings without self-referential fits or load-bearing self-citations.

full rationale

The paper's central reduction of adversarial robustness to traversal of the complete lattice I(d)|F_x (Thm. 1, citing only Sunaga's classical interval algebra) proceeds by explicit definitions of the ⊤, ⊥ and maximal-closure operators (Defs. 6–8) whose correctness is proved directly from the geometry of compact decision surfaces Dc and the soundness/completeness of the MILP verification oracles (eqs. 5–6). Theorems 3–6 establish uniqueness of the minimal complete certificate and the approximation/termination guarantees of the refine-and-verify schemes by elementary arguments on set inclusion and potential functions; the proofs never invoke a prior result of the same authors as an external uniqueness theorem. The complexity asymmetry (Thms. 7–8) is obtained by a standard polynomial-time reduction from the known NP-hard q-MER problem, again without circular appeal. Symmetric-interval algorithms are ordinary dichotomic search. No free parameters are fitted to data and then re-presented as predictions; the sole free parameter δ is an explicit precision constant. Self-citations are limited to background tools (Marabou/Reluplex) that are independently implemented and externally falsifiable. The experimental section merely evaluates the algorithms and does not carry any theoretical claim. Consequently the derivation chain is self-contained and free of the six circularity patterns.

Assumptions & free parameters 2 free parameters · 4 assumptions · 2 invented entities

The paper rests on standard interval algebra, the MILP encoding of ReLU networks, and the existence of sound-and-complete verifiers. The only free parameters are algorithmic precision and resource limits; no data-fitted constants appear in the theorems. Invented entities are the dual certificate notions and the lattice operators themselves, which are fully defined and algorithmically realized.

free parameters (2)
  • precision constant δ = 0.1
    Controls both accuracy and termination of the refine-and-verify loops (set to 0.1 in experiments); appears in every complexity bound.
  • timeout / max iterations = 1 h / 10 000
    Practical cut-offs (1–2 h, 10 000 iterations) that affect empirical completeness but not the theoretical claims.
assumptions (4)
  • standard math The set of closed intervals containing a fixed point x forms a complete lattice under inclusion with join ⊔ and meet ⊓ (Sunaga interval algebra).
    Invoked as Thm. 1; classical result used to justify the traversal operators.
  • domain assumption ReLU MLPs admit an exact MILP encoding (big-M formulation) that is sound and complete for the network’s input-output relation.
    Eq. (2) and the Marabou oracle; standard in the verification literature.
  • domain assumption Decision surfaces Dc are compact subsets of the feature space F.
    Used in every termination and uniqueness proof (Thms. 3–6); necessary for finite radii.
  • domain assumption A sound-and-complete MLP verifier (Marabou) is available as an oracle that either proves a property or returns a counter-example.
    Central to the refine-and-verify scheme; inherits NP-hardness of verification.
invented entities (2)
  • complete interval certification independent evidence
    purpose: Dual of the classical sound (robustness) certificate: any exit from the interval forces a label change.
    Explicitly claimed as previously unexamined; defined in Def. 5 and realized by the ⊤-operator.
  • ⊤ / ⊥ / maximal-closure lattice operators independent evidence
    purpose: Systematic expansion/contraction of intervals that guarantee minimality of complete and maximality of sound certificates.
    Defined in Sec. 4; correctness proved via potential functions and Lem. 1.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Interval Certifications for Multilayered Perceptrons via Lattice Traversal." pith.science (2026). https://pith.science/paper/YDMXWNAP

@misc{pith2026260708773,
  author       = {Pith},
  title        = {Pith review of: Interval Certifications for Multilayered Perceptrons via Lattice Traversal},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YDMXWNAP}},
  note         = {Machine review of arXiv:2607.08773}
}
abstract

In this work we present a rigorous theoretical framework to a foundational problem of AI safety, namely adversarial robustness. In particular, we show that the adversarial robustness problem can be reduced to a lattice traversal problem. Each element of this lattice corresponds to an interval, i.e., an axis-aligned hyper-rectangle, containing an input point $\mathbf{x}$. Consider a multilayered perceptron classifier (MLP). An interval $I$ constitutes a sound certification if $\mathbf{x} \in I$ and $\mathbf{x}$ can be freely perturbed in $I$ without changing the MLP's prediction. Complementarily, an interval $I$ constitutes a complete certification if $\mathbf{x} \in I$ and when $\mathbf{x}$ moves outside of $I$ the MLP's prediction is guaranteed to change. While the sound certification problem corresponds to the well-studied adversarial robustness, complete certifications have not been examined in the literature. We develop lattice traversal operators, which we apply in a refine & verify iterative scheme. Using formal MLP verifiers, sound maximality and complete minimality are guaranteed. Moreover, we examine objective optimization problems. There we discover some interesting asymmetries. For complete certifications, the minimum solution is obtained in polynomial oracle calls. This does not hold for sound certifications, where we prove strong intractability results. Additionally, we examine optimization problems in symmetric intervals (i.e., $\ell_\infty$-spheres), where we provide logarithmic algorithms. Finally, we present an empirical evaluation, using the novel ParallelepipedoNN system.

Figures

Figures reproduced from arXiv: 2607.08773 by the authors.

Figure 1
Figure 1. A sound interval certification [lb, ub], and a complete interval certification [LB, UB], for a MNIST image of “7”. The sound interval certification has been com￾puted using the Algorithm 1 , while its complete counterpart was computed by Algo￾rithm 3 in ℓ∞-spheres. Intuitively, a sound certification I assures that any perturbation of the input x inside I will not change its prediction. On the other hand, a complete … view at source ↗
Figure 2
Figure 2. The structure of I(d)| F x. We adopt the Hasse diagram convention depicting each element higher from the elements it dominates. Dc is shown in the image with a dashed line, because, in general, Dc ∈/ I(d)| F x, and thus, technically, D is not part of the diagram. Moreover, ω(Dc⊥x) ≤ ω(Dc) ≤ ω(Dc⊤x), for an increasing objective ω(·). We call eq. (10a), the Sound Interval Maximization (SIM) problem, while eq. (10b) Co… view at source ↗
Figure 3
Figure 3. Cone Decomposition of R 3 . The polyhedral cones of eq. (8), correspond to pyramids is R 3 . Left: The V 1 , V 1 cones of the x1–axis. Observe that V 1 ∩ V 1 = {0}. Right: The cone decomposition , of the entire R 3 . To gain intuition about the underlying problem, we present the cone decom￾position of R 3 in [PITH_FULL_IMAGE:figures/full_fig_p027_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Left, Middle: The matrices U2 ,U3 ∈ R 4×4 , for the cones V 2 , V 2. It holds that V 2 ∩ V 3 = {x ∈ R d | U23x ≥ 0}. this notation in place, the cones from eq. (8) can now be written equivalently in the form, V i = {x ∈ R d | Uix ≥ 0}, V i = {x ∈ R d | Uix ≥ 0}. (16) E…
Figure 5
Figure 5. Figure 5: Minimum edge length of the certifications computed by each algorithm, per MNIST input point. length for each input and algorithm. Finally, in Tab. 4 presents example images illustrating the computed bounds of the instance 7-4. BUS TDS SDE TDS+SDE B-BUS B-TDS Lower Boun…
Figure 6
Figure 6. Figure 6: Minimum edge length of the certifications computed by each algorithm, per Fashion MNIST input point [PITH_FULL_IMAGE:figures/full_fig_p032_6.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

40 extracted references · 1 linked inside Pith

  1. [1]

    In: López-Ortiz, A

    Backer, J., Keil, J.M.: The mono- and bichromatic empty rectangle and square problems in all dimensions. In: López-Ortiz, A. (ed.) LATIN. Springer (2010)

    2010

  2. [2]

    Chan, T.M.: Faster algorithms for largest empty rectangles and boxes. Discret. Comput. Geom. (2023)

    2023

  3. [3]

    Chazelle, B., III, R.L.S.D., Lee, D.T.: Computing the largest empty rectangle. SIAM J. Comput. (1986)

    1986

  4. [4]

    DeepSeek-AI, :, Bi, X., Chen, D., Chen, G., Chen, S., Dai, D., Deng, C., Ding, H., Dong, K., Du, Q., Fu, Z., Gao, H., Gao, K., Gao, W., Ge, R., Guan, K., Guo, D., Guo, J., Hao, G., Hao, Z., He, Y., Hu, W., Huang, P., Li, E., Li, G., Li, J., Li, Y., Li, Y.K., Liang, W., Lin, F., Liu, A.X., Liu, B., Liu, W., Liu, X., Liu, X., Liu, Y., Lu, H., Lu, S., Luo, F...

    2024

  5. [5]

    IEEE Signal Processing Magazine (2012)

    Deng, L.: The mnist database of handwritten digit images for machine learning research. IEEE Signal Processing Magazine (2012)

    2012

  6. [6]

    In: ATVA (2017)

    Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: ATVA (2017)

    2017

  7. [7]

    IEEE TSSC (1969)

    Fukushima, K.: Visual feature extraction by a multilayered network of analog threshold elements. IEEE TSSC (1969)

    1969

  8. [8]

    In: AISTATS

    Glorot, X., Bengio, Y.: Understanding the difficulty of training deep feedforward neural networks. In: AISTATS. JMLR Proceedings, JMLR.org (2010)

    2010

Show all 40 references
  1. [9]

    In: ICLR (2015)

    Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: ICLR (2015)

    2015

  2. [10]

    In: Ailamaki, A., Bowers, S

    Gutiérrez, G., Paramá, J.R.: Finding the largest empty rectangle containing only a query point in large multidimensional databases. In: Ailamaki, A., Bowers, S. (eds.) SSDBM. Lecture Notes in Computer Science, Springer (2012)

    2012

  3. [11]

    In: AAAI (2024)

    Izza, Y., Ignatiev, A., Stuckey, P.J., Marques-Silva, J.: Delivering inflated expla- nations. In: AAAI (2024)

    2024

  4. [12]

    Kabaha, A., Drachsler-Cohen, D.: Maximal robust neural network specifications viaoracle-guidednumericaloptimization.In:Dragoi,C.,Emmi,M.,Wang,J.(eds.) VMCAI (2023)

    2023

  5. [13]

    In: CAV (2017)

    Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: CAV (2017)

    2017

  6. [14]

    Formal Methods Syst

    Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. (2022)

    2022

  7. [15]

    In: CAV (2019)

    Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.: The marabou framework for verification and analysis of deep neural networks. In: CAV (2019)

    2019

  8. [16]

    In: ICLR (2015)

    Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. In: ICLR (2015)

    2015

  9. [17]

    IEEE TDSC (2022) 20 M

    Li, C., Ji, S., Weng, H., Li, B., Shi, J., Beyah, R., Guo, S., Wang, Z., Wang, T.: Towards certifying the asymmetric robustness for neural networks: Quantification and applications. IEEE TDSC (2022) 20 M. Papamichail et al

    2022

  10. [18]

    IEEE Transactions on Intelligent Transportation Systems (2025)

    Li, D., Auerbach, P., Okhrin, O.: Autonomous driving small-scale cars: A survey of recent development. IEEE Transactions on Intelligent Transportation Systems (2025)

    2025

  11. [19]

    In: ICML

    Liu, C., Tomioka, R., Cevher, V.: On certifying non-uniform bounds against ad- versarial attacks. In: ICML. PMLR (2019)

    2019

  12. [20]

    CoRR (2017)

    Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. CoRR (2017)

    2017

  13. [21]

    In: ICKDDM

    Ma, F., Chitta, R., Zhou, J., You, Q., Sun, T., Gao, J.: Dipole: Diagnosis predic- tion in healthcare via attention-based bidirectional recurrent neural networks. In: ICKDDM. ACM (2017)

    2017

  14. [22]

    In: ICLR

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: ICLR. OpenReview.net (2018)

    2018

  15. [23]

    In: ICLR (2018)

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: ICLR (2018)

    2018

  16. [24]

    IEEE TDSC (2022)

    Meng, M.H., Bai, G., Teo, S.G., Hou, Z., Xiao, Y., Lin, Y., Dong, J.S.: Adversarial robustnessofdeepneuralnetworks:Asurveyfromaformalverificationperspective. IEEE TDSC (2022)

    2022

  17. [25]

    Mirman, M., Baader, M., Vechev, M.T.: The fundamental limits of neural networks for interval certified robustness. Trans. Mach. Learn. Res. (2022)

    2022

  18. [26]

    SIAM (2009)

    Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. SIAM (2009)

    2009

  19. [27]

    Discrete Applied Mathematics (1984)

    Naamad, A., Lee, D.T., Hsu, W.: On the maximum empty rectangle problem. Discrete Applied Mathematics (1984)

    1984

  20. [28]

    In: ICML

    Raghunathan, A., Xie, S.M., Yang, F., Duchi, J.C., Liang, P.: Understanding and mitigating the tradeoff between robustness and accuracy. In: ICML. Proceedings of Machine Learning Research, PMLR (2020)

    2020

  21. [29]

    In: NeurIPS (2019)

    Salman, H., Yang, G., Zhang, H., Hsieh, C.J., Zhang, P.: A convex relaxation barrier to tight robustness verification of neural networks. In: NeurIPS (2019)

    2019

  22. [30]

    Research Association of Applied Geometry (1958)

    Sunaga, T.: Theory of an interval algebra and its application to numerical analysis. Research Association of Applied Geometry (1958)

    1958

  23. [31]

    In: ICLR (2014)

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: ICLR (2014)

    2014

  24. [32]

    In: ICLR (2019)

    Tsipras, D., Santurkar, S., Engstrom, L., Turner, A., Madry, A.: Robustness may be at odds with accuracy. In: ICLR (2019)

    2019

  25. [33]

    In: ICML

    Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: ICML. PMLR (2018)

    2018

  26. [34]

    In: CAV (2024)

    Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A versatile formal analyzer of neural networks. In: CAV (2024)

    2024

  27. [35]

    CoRR (2017),http://arxiv.org/abs/ 1708.07747

    Xiao, H., Rasul, K., Vollgraf, R.: Fashion-mnist: a novel image dataset for bench- marking machine learning algorithms. CoRR (2017),http://arxiv.org/abs/ 1708.07747

    2017 arXiv

  28. [36]

    In: Chaudhuri, K., Salakhut- dinov, R

    Zhang, H., Yu, Y., Jiao, J., Xing, E.P., Ghaoui, L.E., Jordan, M.I.: Theoretically principled trade-off between robustness and accuracy. In: Chaudhuri, K., Salakhut- dinov, R. (eds.) ICML. PMLR (2019)

    2019

  29. [37]

    In: ICLR (2020)

    Zhang, H., Chen, H., Xiao, C., Gowal, S., Stanforth, R., Li, B., Boning, D.S., Hsieh, C.: Towards stable and efficient training of verifiably robust neural networks. In: ICLR (2020)

    2020

  30. [38]

    In: NeurIPS 2018 (2018) Interval Certifications for MLPs via Lattice Traversal 21

    Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: NeurIPS 2018 (2018) Interval Certifications for MLPs via Lattice Traversal 21

    2018

  31. [39]

    ACM (2025)

    Zhu, Y., Wan, C., Steck, H., Liang, D., Feng, Y., Kallus, N., Li, J.: Collabora- tive retrieval for large language model-based conversational recommender systems. ACM (2025)

    2025

  32. [40]

    Government Information Quarterly (2021) A Omitted proofs A.1 Proofs of Section 3 Proposition 2.For an intervalI∈I(d)| F x and the measures of Def

    Zuiderwijk, A., Chen, Y.C., Salem, F.: Implications of the use of artificial intelli- gence in public governance: A systematic literature review and a research agenda. Government Information Quarterly (2021) A Omitted proofs A.1 Proofs of Section 3 Proposition 2.For an interva...

    2021

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.