arxiv: 2603.23878 · v2 · submitted 2026-03-25 · 💻 cs.LG · cs.AI· cs.LO

Recognition: no theorem link

The Luna Bound Propagator for Formal Analysis of Neural Networks

Haoze Wu, Henry LeCates

Authors on Pith no claims yet

Pith reviewed 2026-05-15 00:54 UTC · model grok-4.3

classification 💻 cs.LG cs.AIcs.LO

keywords neural network verificationbound propagationabstract interpretationalpha-CROWNC++ implementationformal analysisVNN-COMPDeepPoly

0 comments

The pith

A new C++ bound propagator called Luna computes tighter and faster bounds for neural network verification than the existing Python alpha-CROWN.

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

This paper presents Luna, a C++ implementation of abstract-interpretation methods for verifying properties of neural networks. Luna supports interval bound propagation, DeepPoly/CROWN analysis, and parameterized alpha-CROWN over general computational graphs. The reported result is that it produces tighter bounds and runs faster than the leading Python alpha-CROWN on VNN-COMP 2025 benchmarks. The advance matters because C++ code integrates more readily into production verifiers and long-term systems than Python. A reader focused on reliable AI would see the work as reducing the practical cost of formal analysis.

Core claim

Luna is a C++ bound propagator that implements Interval Bound Propagation, DeepPoly/CROWN, and alpha-CROWN analysis on general computational graphs, and it outperforms the state-of-the-art Python alpha-CROWN implementation in both bound tightness and computational efficiency on supported VNN-COMP 2025 benchmarks.

What carries the argument

The Luna bound propagator, a C++ reimplementation of the parameterized CROWN (alpha-CROWN) method that computes certified bounds for neural network outputs across multiple analysis modes.

If this is right

Existing DNN verifiers gain easier integration through the C++ interface.
Verification runs on supported benchmarks finish with tighter certified bounds and shorter computation times.
A single framework now covers interval, DeepPoly/CROWN, and alpha-CROWN analyses on general graphs.
Public release allows direct incorporation into production verification pipelines.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Safety-critical applications such as autonomous systems could incorporate tighter formal guarantees at lower overhead.
Extensions to additional network layers or new bound-propagation variants become feasible once the C++ base is in place.
Re-implementations in other performance-oriented languages could be compared directly against Luna to isolate language-specific gains.

Load-bearing premise

The C++ implementation correctly and faithfully reproduces the mathematical behavior of the original Python alpha-CROWN without introducing numerical or algorithmic discrepancies that affect the reported tightness or speed gains.

What would settle it

Running the identical VNN-COMP 2025 benchmark networks through both Luna and the reference Python alpha-CROWN and checking whether Luna indeed returns strictly tighter bounds at lower runtimes.

Figures

Figures reproduced from arXiv: 2603.23878 by Haoze Wu, Henry LeCates.

**Figure 1.** Figure 1: High-level overview of Luna’s system architecture. bounds L(x, α) ≤ f(x) ≤ U(x, α) where L(x, α) and U(x, α) are affine in x for fixed α. The choice of α is then optimized (once for lower bound and once for upper bound) by solving max α∈A min x∈X L(x, α), min α∈A max x∈X U(x, α), where A represents the valid ranges of α (e.g., [0, 1] for ReLU lower bound). In practice, this nonconvex optimization problem i… view at source ↗

**Figure 2.** Figure 2: Example Python API usage: loading an ONNX model, setting input [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

read the original abstract

The parameterized CROWN analysis, a.k.a., alpha-CROWN has emerged as a practically successful abstract interpretation method for neural network verification. However, existing implementations of alpha-CROWN are limited to Python, which complicates integration into existing DNN verifiers and long-term production-level systems. We introduce Luna, a new abstract-interpretation-based bound propagator implemented in C++. Luna supports Interval Bound Propagation, the DeepPoly/CROWN analysis, and the alpha-CROWN analysis over a general computational graph. We describe the architecture of Luna and show that it outperforms the state-of-the-art alpha-CROWN implementation in terms of both bound tightness and computational efficiency on supported benchmarks from VNN-COMP 2025. Luna is publicly available at https://github.com/ai-ar-research/luna.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Luna is a C++ reimplementation of alpha-CROWN that reports better speed and tightness on VNN-COMP 2025, but the tightness numbers rest on an unverified assumption that the C++ version matches the Python reference exactly.

read the letter

Luna ports the alpha-CROWN bound propagator to C++ and claims it runs faster while producing tighter bounds than the existing Python version on the VNN-COMP 2025 benchmarks. The authors also support plain interval propagation and DeepPoly/CROWN over general graphs, and they describe the implementation architecture in enough detail to see how they structured the propagators and the alpha optimization step. The code is public, which is the main practical advance here. For anyone who needs to integrate a bound propagator into a larger C++ verifier or a production pipeline, this removes the Python dependency that has been a recurring pain point. The empirical results are presented directly against the state-of-the-art Python baseline, so the comparison is at least on the right benchmarks. The soft spot is the lack of any reported cross-check that the C++ and Python versions produce identical intermediate results or final bounds on the same small networks. Tightness is sensitive to how the linear relaxations are applied and how the alpha parameters are optimized; small differences in floating-point ordering or optimization loops can shift the numbers without changing the underlying analysis. The paper treats Luna as a faithful reimplementation, so that equivalence step should have been shown explicitly. The citations and the core analyses are standard, with no obvious gaps in the references. This is useful for the neural-network verification crowd that already runs these methods and wants a faster drop-in replacement. It is not a theoretical advance, but the engineering work is concrete and the benchmarks are relevant. I would send it to peer review and ask the referees to check the equivalence tests and the exact alpha-CROWN implementation details against the Python reference.

Referee Report

2 major / 2 minor

Summary. The paper introduces Luna, a C++ implementation of abstract interpretation-based bound propagation supporting Interval Bound Propagation, DeepPoly/CROWN, and alpha-CROWN over general computational graphs for neural network verification. It claims that this implementation outperforms the state-of-the-art Python alpha-CROWN in both bound tightness and computational efficiency on supported VNN-COMP 2025 benchmarks, with the code released publicly at a GitHub repository.

Significance. If the C++ reimplementation faithfully reproduces the mathematical behavior of alpha-CROWN without introducing discrepancies, Luna could enable easier integration of advanced verification techniques into production systems and long-term maintenance, addressing a practical limitation of existing Python tools. The public code release supports reproducibility and potential community adoption.

major comments (2)

[Experimental Evaluation] Experimental section (results on VNN-COMP 2025): the headline claim of tighter bounds and faster runtime for Luna's alpha-CROWN mode rests on direct comparison to an external Python baseline, but no equivalence verification (e.g., matching intermediate alpha parameters, relaxation matrices, or final bounds on identical inputs) is reported; without this, observed differences could stem from unverified algorithmic or numerical deviations rather than genuine improvements.
[Implementation Architecture] Implementation architecture (Section 3): the description of how alpha parameter optimization and linear relaxations are realized in C++ does not include explicit checks or invariants ensuring mathematical equivalence to the reference Python alpha-CROWN, which is load-bearing for interpreting the tightness results as faithful reimplementation gains.

minor comments (2)

[Abstract] Abstract: the phrase 'supported benchmarks from VNN-COMP 2025' is vague; listing the specific networks or properties used would improve clarity without lengthening the text.
Notation: the paper uses 'alpha-CROWN' interchangeably with 'parameterized CROWN' but does not define the exact parameterization (e.g., how alpha variables are initialized or optimized) in a single location, which could confuse readers unfamiliar with the baseline.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which highlight important aspects of reproducibility and faithfulness in our comparison. We address each major comment below and will incorporate revisions to strengthen the manuscript.

read point-by-point responses

Referee: [Experimental Evaluation] Experimental section (results on VNN-COMP 2025): the headline claim of tighter bounds and faster runtime for Luna's alpha-CROWN mode rests on direct comparison to an external Python baseline, but no equivalence verification (e.g., matching intermediate alpha parameters, relaxation matrices, or final bounds on identical inputs) is reported; without this, observed differences could stem from unverified algorithmic or numerical deviations rather than genuine improvements.

Authors: We agree that explicit equivalence verification is necessary to support the claim that performance differences arise from implementation rather than algorithmic deviations. In the revised manuscript we will add a new subsection in the experimental evaluation that reports direct comparisons on small networks and selected VNN-COMP instances, confirming that Luna produces identical alpha parameters, relaxation matrices, and final bounds (within floating-point tolerance) to the reference Python alpha-CROWN implementation when given identical inputs and initialization. This verification will be performed using the same random seeds and optimization settings. revision: yes
Referee: [Implementation Architecture] Implementation architecture (Section 3): the description of how alpha parameter optimization and linear relaxations are realized in C++ does not include explicit checks or invariants ensuring mathematical equivalence to the reference Python alpha-CROWN, which is load-bearing for interpreting the tightness results as faithful reimplementation gains.

Authors: We acknowledge that the current description of the C++ realization lacks explicit statements of the mathematical invariants used. In the revised Section 3 we will add a dedicated paragraph (and accompanying pseudocode) that enumerates the key invariants preserved by our implementation: identical linear relaxation forms for ReLU, identical gradient-based alpha optimization procedure, and identical bound propagation order over the computational graph. We will also describe the unit tests we maintain that assert numerical agreement on these quantities against the reference Python code. revision: yes

Circularity Check

0 steps flagged

No circularity in Luna's implementation claims or benchmark comparisons

full rationale

The paper presents a C++ reimplementation of established bound-propagation techniques (IBP, DeepPoly/CROWN, alpha-CROWN) and reports empirical tightness and speed results on external VNN-COMP 2025 benchmarks. No derivation chain, first-principles result, or fitted parameter is introduced that reduces to a self-defined quantity. All load-bearing claims rest on direct runtime comparisons against an independent Python baseline rather than on quantities defined in terms of Luna's own outputs or prior self-citations. The architecture description and public code release further separate the contribution from any self-referential construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The work relies on the correctness of the ported abstract-interpretation algorithms and on the representativeness of the VNN-COMP benchmarks; no new free parameters, axioms, or invented entities are introduced beyond the standard bound-propagation framework.

pith-pipeline@v0.9.0 · 5425 in / 1008 out tokens · 23636 ms · 2026-05-15T00:54:48.872126+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages · 1 internal anchor

[1]

Bai, J., Lu, F., Zhang, K., et al.: Onnx: Open neural network exchange.https: //github.com/onnx/onnx(2019)

work page 2019
[2]

In: International Conference on Computer Aided Verification

Bak, S., Tran, H.D., Hobbs, K., Johnson, T.T.: Improved Geometric Path Enu- meration for Verifying ReLU Neural Networks. In: International Conference on Computer Aided Verification. pp. 66–96. Springer (2020)

work page 2020
[3]

arXiv preprint arXiv:2412.19985 (2024)

Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neu- ral networks competition (vnn-comp 2024): Summary and results. arXiv preprint arXiv:2412.19985 (2024)

work page arXiv 2024
[4]

In: International Conference on Computer Aided Verification

Duong, H., Nguyen, T., Dwyer, M.B.: Neuralsat: a high-performance verification tool for deep neural networks. In: International Conference on Computer Aided Verification. pp. 409–423. Springer (2025)

work page 2025
[5]

arXiv preprint arXiv:1810.12715 (2018)

Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arand- jelovic, R.,Mann, T.,Kohli, P.: OntheEffectivenessofIntervalBoundPropagation for Training Verifiably Robust Models. arXiv preprint arXiv:1810.12715 (2018)

work page arXiv 2018
[6]

In: International Joint Con- ference on Artificial Intelligence

Henriksen, P., Lomuscio, A.: DEEPSPLIT: An Efficient Splitting Method for Neu- ral Network Verification via Indirect Effect Analysis. In: International Joint Con- ference on Artificial Intelligence. pp. 2549–2555. ijcai.org (8 2021)

work page 2021
[7]

In: Giacomo, G.D., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarín, A., Lang, J

Henriksen, P., Lomuscio, A.R.: Efficient Neural Network Verification via Adap- tive Refinement and Adversarial Search. In: Giacomo, G.D., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarín, A., Lang, J. (eds.) European Conference on Artificial Intelligence. vol. 325, pp. 2513–2520. IOS Press (2020)

work page 2020
[8]

In: Proc

Katz, G., Huang, D., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D., Kochenderfer, M., Barrett, C.: The Marabou Framework for Verification and Analysis of Deep Neural Networks. In: Proc. 31st Int. Conf. on Computer Aided Verification (CAV). pp. 443–452 (2019)

work page 2019
[9]

arXiv preprint arXiv:2512.19007 (2025)

Kaulen, K., Ladner, T., Bak, S., Brix, C., Duong, H., Flinkow, T., Johnson, T.T., Koller, L., Manino, E., Nguyen, T.H., et al.: The 6th international verification of neural networks competition (vnn-comp 2025): Summary and results. arXiv preprint arXiv:2512.19007 (2025)

work page arXiv 2025
[10]

Lopez, D.M., Choi, S.W., Tran, H., Johnson, T.T.: NNV 2.0: The Neural Network VerificationTool.In:Enea,C.,Lal,A.(eds.)InternationalConferenceonComputer Aided Verification. vol. 13965, pp. 397–412. Springer (2023)

work page 2023
[11]

Towards Deep Learning Models Resistant to Adversarial Attacks

Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083 (2017)

work page internal anchor Pith review Pith/arXiv arXiv 2017
[12]

Proceedings of the ACM on Programming Languages6(POPL), 1–33 (2022)

Müller, M.N., Makarchuk, G., Singh, G., Püschel, M., Vechev, M.: Prima: general and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM on Programming Languages6(POPL), 1–33 (2022)

work page 2022
[13]

Advances in neural information processing sys- tems32(2019)

Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., et al.: Pytorch: An imperative style, high- performance deep learning library. Advances in neural information processing sys- tems32(2019)

work page 2019
[14]

Advances in Neural Information Process- ing Systems32, 15098–15109 (2019)

Singh, G., Ganvir, R., Püschel, M., Vechev, M.: Beyond the Single Neuron Convex Barrier for Neural Network Certification. Advances in Neural Information Process- ing Systems32, 15098–15109 (2019)

work page 2019
[15]

Proceedings of the ACM on Programming Languages3(POPL), 1–30 (2019) TheLunaBound Propagator for Formal Analysis of Neural Networks 9

Singh, G., Gehr, T., Püschel, M., Vechev, M.: An Abstract Domain for Certifying Neural Networks. Proceedings of the ACM on Programming Languages3(POPL), 1–30 (2019) TheLunaBound Propagator for Formal Analysis of Neural Networks 9

work page 2019
[16]

In: International Conference on Learning Representations (2019)

Singh, G., Gehr, T., Püschel, M., Vechev, M.: Boosting Robustness Certification of Neural Networks. In: International Conference on Learning Representations (2019)

work page 2019
[17]

In: International Conference on Learning Represen- tations (2019)

Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: International Conference on Learning Represen- tations (2019)

work page 2019
[18]

In: International Confer- ence on Computer Aided Verification

Tran, H.D., Yang, X., Manzanas Lopez, D., Musau, P., Nguyen, L.V., Xiang, W., Bak,S.,Johnson,T.T.:NNV:theNeuralNetworkVerificationToolforDeepNeural Networks and Learning-enabled Cyber-Physical Systems. In: International Confer- ence on Computer Aided Verification. pp. 3–17. Springer (2020)

work page 2020
[19]

Advances in Neural Information Processing Systems 31, 6369–6379 (2018)

Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient Formal Safety Analysis of Neural Networks. Advances in Neural Information Processing Systems 31, 6369–6379 (2018)

work page 2018
[20]

Advances in Neural Information Processing Sys- tems34, 29909–29921 (2021)

Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta- crown: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. Advances in Neural Information Processing Sys- tems34, 29909–29921 (2021)

work page 2021
[21]

arXiv preprint arXiv:2401.14461 (2024)

Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., et al.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. arXiv preprint arXiv:2401.14461 (2024)

work page arXiv 2024
[22]

Advances in Neural Information Processing Systems33, 1129–1141 (2020)

Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K.W., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.J.: Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond. Advances in Neural Information Processing Systems33, 1129–1141 (2020)

work page 2020
[23]

In: Proc

Zelazny, T., Wu, H., Barrett, C., Katz, G.: On Reducing Over-Approximation Er- rors for Neural Network Verification. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). pp. 17–26 (2022)

work page 2022
[24]

Advances in Neural Information Processing Systems35, 1656–1670 (2022)

Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C.J., Kolter, J.Z.: General Cutting Planes for Bound-propagation-based Neural Network Verification. Advances in Neural Information Processing Systems35, 1656–1670 (2022)

work page 2022
[25]

Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient Neural Net- work Robustness Certification with General Activation Functions. Advances in Neural Information Processing Systems31, 4944–4953 (2018) 10 Henry LeCates and Haoze Wu A Architecture and Core Components This appendix records implementation-level details that complement Section ...

work page 2018