Pith. sign in

REVIEW 4 major objections 5 minor 36 references

Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification

T0 review · 4 major / 5 minor · reviewed 2026-08-03 · deepseek-v4-flash

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

Pith's one-line read This paper claims that a reinforcement-learning agent, trained on past verification queries, can learn a splitting policy for ReLU constraints that cuts average verification time by 5.88% to 56.20% compared with static heuristics.

desk verdict Useful proof-of-concept for learning ReLU splits in Marabou, but the abstract's iteration claim is directly contradicted by the paper's own tables and the reported query totals don't add up. read the letter →

arxiv 2512.10747 v2 pith:YFBMVHMH submitted 2025-12-11 cs.LO

Maya Swisa , Guy Katz This is my paper
classification cs.LO
keywords neuralnetworkverificationbranch-and-boundsplittingheuristicreinforcementlearningDQfDReLUACASXuMarabou
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 argues that the order in which a neural-network verifier splits ReLU constraints can be learned from past verification queries rather than fixed by a hand-crafted rule. It trains a Deep Q-learning-from-Demonstrations (DQfD) agent inside the Marabou verifier, using existing heuristics as expert demonstrations, and evaluates on ACAS Xu safety and robustness queries. The claimed result is a measurable reduction in average verification time and in the number of solver iterations compared with established splitting heuristics, with the largest gains on hard instances. If correct, the approach turns repeated verification of the same network into a learning task that speeds up future queries.

What carries the argument

The load-bearing mechanism is a Double DQN agent trained from demonstrations, paired with a reward function that charges a delayed penalty equal to the ratio of actual splits taken inside a subtree to the maximum possible splits in a full binary tree of that remaining depth (actual(n)/full(n)). This normalized penalty teaches the agent to prefer splits that prune the search early. The agent's state representation combines per-ReLU bounds, phase, and the scores of three existing heuristics with global search statistics, letting it mimic the best heuristic on easy nodes and deviate on hard ones.

What would settle it

Recompute both benchmarks' average verification times on the subset of queries solved by all methods, excluding timeouts, and compare the agent to Polarity; if Polarity is faster on that subset, the paper's headline reduction in average time depends on the timeout-counting convention.

Watch

Extended reading notes

Core claim

The central discovery is that a state-conditioned splitting policy, learned via DQfD and deployed inside a branch-and-bound verifier, can outperform static heuristics on repeated queries over the same network. The agent observes the current node in the search tree — including per-ReLU bounds, phase, and the SoI, polarity, and BaBSR scores — and selects which ReLU to split next, receiving a delayed penalty proportional to the size of the subtree its split induces. Trained on about 5% of the benchmark queries, the policy transfers to unseen properties and networks, solving more instances and achieving lower average verification time than Pseudo-Impact, Polarity, and BaBSR.

Load-bearing premise

The central comparison assumes that a timed-out query should be counted as exactly one hour in the average; if timeouts were handled differently (e.g., excluded or weighted differently), the reported reduction in average verification time could disappear.

Editorial extensions

If this is right

  • On the ACAS Xu safety benchmarks, the learned policy reduces average verification time by 5.88% to 56.20% relative to the static baselines, with the largest gains on harder instances.
  • The learned policy solves more instances within a 1-hour timeout than any single static heuristic, reducing the number of timeouts by up to 22 compared with Polarity on the robustness setup.
  • A single training session on a small subset of queries transfers to unseen properties and networks, so the agent does not need to be retrained for each new query.
  • The policy can be inserted into an existing verifier as a drop-in replacement for its branching heuristic, since it only changes the order of splits, not the soundness or completeness of the underlying search.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same training recipe could plausibly extend to other piecewise-linear activations (e.g., leaky ReLU or max-pooling) by redefining the action space and state features; the paper does not test this, but the formulation is not ReLU-specific.
  • Because the agent closely tracks the strongest baseline on easy instances and diverges on hard ones, the practical value may be concentrated in the long tail of hard queries; a per-instance speedup analysis (excluding timeout effects) would clarify where the gains really come from.
  • If the learned policy could be distilled into a lightweight scoring rule, the overhead of running a deep network at every node might be avoided, making the approach scalable to larger networks with many ReLUs.
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

4 major / 5 minor

Summary. The paper proposes a reinforcement-learning-based branching heuristic for neural network verification. It models ReLU case splitting as an MDP and trains a Double DQN with demonstrations (DQfD) to choose which unfixed ReLU to split and which phase (active/inactive) to explore first. The policy is trained on a small fraction of ACAS Xu safety and robustness queries and then deployed in the Marabou verifier on the remaining queries. The reported experiments compare the learned agent against Polarity, Pseudo-Impact, and BaBSR, showing lower average verification time and more solved instances in two ACAS Xu setups. The paper also positions the work as addressing repeated queries on the same network, where past experience can guide future branching decisions.

Significance. If the empirical results are confirmed, the paper makes a useful contribution to multi-query neural network verification: it demonstrates a concrete way to combine existing splitting heuristics into a state-conditioned policy and provides a proof-of-concept implementation integrated into Marabou. The public code release and the use of held-out evaluation queries are strengths. However, the paper's central claim is overstated: the abstract's assertion of a reduction in the average number of iterations is directly contradicted by the tables, and the time improvements over Polarity and BaBSR are modest and reported without statistical confidence. The approach is also evaluated only on ACAS Xu and is initialized with demonstrations generated by the same baselines it is compared against, so its general value beyond this setting is not yet established.

major comments (4)
  1. [Abstract; §4.2, Tables 1–2] The abstract's claim of a "substantial reduction ... in the average number of iterations required" is not supported by the reported data. In Table 1, DQfD's average iterations (838,986.76) exceed Polarity (795,486.79) and BaBSR (779,218.49); in Table 2, DQfD (235,690.92) exceed Polarity (222,903.82). Section 4.2 itself concedes that the agent "requires a slightly greater number of iterations" in setup (ii). Because the abstract presents time and iteration reductions as a conjunction, one false conjunct materially weakens the central contribution. The abstract and the corresponding passages in the introduction and conclusion must be corrected, or the iteration claim must be qualified (e.g., against Pseudo-Impact only, or on hard instances).
  2. [§4.2, Tables 1–2] The measurement of "average verification time" is not rigorous enough to support the claimed reduction. The table captions say timeouts are counted as one hour, while the text says averages are computed "across the queries solved by all methods, including those runs that terminated due to a timeout," which is internally inconsistent. Moreover, the reported SAT+UNSAT+Timeout sums are 170 in Table 1 and 2970 in Table 2, leaving 10 and 30 queries unaccounted for, respectively. The time advantage over Polarity is only 10.2% in setup (i) and 5.9% in setup (ii), so the conclusion could depend on the timeout convention and on the handling of missing queries. Please clarify the query set, report the missing queries, and give statistics that separate solved instances from timeout-capped runs (e.g., medians, solved-only averages, or cumulative-distribution plots).
  3. [§4.1 (Training and evaluation)] No variance or significance assessment is reported. The DQfD agent uses randomized ε-greedy exploration, experience replay, and a neural network trained with stochastic gradient updates; a single training run is presented for each setup. Given that the time improvements over Polarity (10.2% and 5.9%) and BaBSR (10.7% and 12.7%) are modest, the results may be within run-to-run variation. The authors should repeat training with multiple seeds and report means with standard deviations or confidence intervals, or explain why the training is effectively deterministic. Without such information, the reader cannot judge the stability of the reported gains.
  4. [§3.2 (Leveraging Expert Demonstrations), §4.2] The agent's demonstrations are generated by the same static heuristics (SoI, pseudo-impact, polarity, BaBSR) that later serve as baselines, and the training queries come from the same ACAS Xu benchmark family used for evaluation. The evaluation is on held-out queries, so it is not circular in the strict sense, but the method's contribution over a simpler policy that adaptively switches among the four static heuristics is not assessed. An ablation that compares DQfD to, for instance, a per-node oracle or a dynamic selection among the baselines would clarify whether the learned value function adds value beyond combining existing heuristics. Without this, the claim that the method "can surpass the performance of static heuristics" remains specific to the ACAS Xu distribution and the chosen demonstration set.
minor comments (5)
  1. [Abstract] Typo: "aleaning from demonstrations" should be "a learning from demonstrations"; also "sub-problem" should be "sub-problems".
  2. [§4.2, Table captions] Table 1 caption says "averages overallinstances" — should be "averages over all instances." The phrase "for common (ExampleID, Epsilon)" in Table 2 is unclear; please describe how the 3000 queries were generated and how the common subset was formed.
  3. [§5, Related Work] The text says "Jeong et al. [18]" but reference [18] is by Jaeckle, Lu, and Kumar. The citation name does not match the bibliography entry.
  4. [§4.2] The paper states that averages are computed "across the queries solved by all methods, including those runs that terminated due to a timeout." This is contradictory and should be rewritten to define exactly which queries are included in the average (e.g., all queries, or solved-only, or all with timeouts capped).
  5. [§6, Conclusion] Typo: "Out method" should be "Our method." Additionally, the conclusion repeats the unsupported claim that the method achieves "results superior to those of modern, hand-crafted heuristics" without mentioning the iteration-count discrepancy in the two main tables.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the agent's reported gains are empirical measurements on held-out queries, not a reduction to its inputs.

full rationale

The paper's central claim—that the DQfD splitting heuristic reduces average verification time—is an experimental result, not a derivation that reduces to its inputs. The agent is pretrained on demonstrations generated by the same static heuristics it is later compared against (Section 3.2, 'Leveraging Expert Demonstrations'), but that is a standard DQfD design choice; the learned policy is not defined as a copy or weighted average of those heuristics, and the fine-tuning phase explicitly allows divergence from them. Training uses approximately 5% of the benchmark queries and evaluation is performed on the remaining queries (Section 4.1), so the reported times and iteration counts are measured on held-out instances rather than re-reported fitted values. The reward function depends on the actual number of splits in closed subtrees, not on the baseline heuristics' outputs, so the training objective is not the same object as the comparison claim. The paper relies on self-authored systems (Marabou, SoI, polarity) as baselines, but these are implemented tools and the comparison is a runtime measurement, not a proof step whose only support is a self-citation. No uniqueness theorem, ansatz-smuggling via citation, or renaming of a known result appears. One non-circular issue exists: the Abstract's claim of 'a substantial reduction ... in the average number of iterations required' is contradicted by the paper's own Tables 1 and 2 (e.g., Table 2: Agent 235,690.92 vs. Polarity 222,903.82; Table 1: Agent 838,986.76 vs. BaBSR 779,218.49), and Section 4.2 itself concedes that the agent 'requires a slightly greater number of iterations compared to the Polarity heuristic.' This is a correctness/consistency problem, not a circular derivation, so it does not raise the circularity score.

Assumptions & free parameters 7 free parameters · 6 assumptions · 0 invented entities

The central empirical claim rests on hand-set design choices (γ, ε schedule, initial depth, training budget, timeout counting) and on assumptions that ACAS Xu's training subset is representative and that the MDP state/reward are informative. None of these are independently benchmarked, which limits extrapolation.

free parameters (7)
  • Discount factor γ = 0.9
    Chosen in Section 3.2 to balance long-term credit and stability; set by hand.
  • ε-greedy decay schedule = start 1.0, ×0.95 per iteration, floor 0.05
    Section 3.2; manual schedule.
  • Training budget = 45,000 splitting steps (5k DQfD + 40k DDQN), ~2 hours per setup
    Section 4.1; fixed a priori but arbitrary.
  • Initial-split depth = 3 (Pseudo-Impact for depth ≤ 3)
    Sections 3.2/4.1; adopted to ensure fair comparison, limits agent's control and is hand-set.
  • DQfD/DDQN hyperparameters
    Learning rate, batch size, network architecture, loss weights, replay priorities not reported in the paper; presumably in code. These are standard but influence results.
  • Training-set fraction = ~5% of ACAS Xu queries per setup
    Section 4.1; arbitrary split, but is the basis for the held-out evaluation.
  • Timeout counting convention = 1 hour = 3600 s in averages
    Section 4.2; this convention materially affects the reported average-time advantage.
assumptions (6)
  • domain assumption Marabou's branch-and-bound and LP-based subproblem solving are sound and complete for ReLU networks.
    Used implicitly in Sections 2.2 and 4.1; the measured iteration/time counts are meaningful only if the solver is correct.
  • ad hoc to paper The MDP state features (bounds, phase, SoI, polarity, BaBSR scores, depth, counts) are sufficient for a value function that predicts split quality.
    Section 3.2 lists features deliberately; if important information is omitted, the learned Q-values may be poor.
  • ad hoc to paper Expert demonstrations generated by SoI/PI/Polarity/BaBSR are useful supervision and do not cap performance.
    Section 3.2 seeds replay with these heuristics; if the experts are too weak or the demonstrations unrepresentative, the agent cannot learn.
  • ad hoc to paper The delayed subtree reward R = -actual(n)/full(n) is well-defined and aligns with verification time.
    Section 3.2; requires completing subtree search to compute actual(n); under timeouts this reward is truncated, which is not discussed.
  • domain assumption ACAS Xu queries in the remaining 95% are drawn from the same distribution as the 5% training queries.
    Section 4.1; if not, the held-out evaluation does not measure generalization.
  • domain assumption Double DQN with prioritized replay converges to a policy that improves over the expert demonstrations.
    Relies on the empirical success of DQfD [16]; no convergence guarantees are given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification." pith.science (2026). https://pith.science/paper/YFBMVHMH

@misc{pith2026251210747,
  author       = {Pith},
  title        = {Pith review of: Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YFBMVHMH}},
  note         = {Machine review of arXiv:2512.10747}
}
read the original abstract

Modern neural network verifiers often encode neural network verification as constraint satisfaction problems. When dealing with standard piecewise-linear activation functions, such as ReLUs, verifiers typically employ branching heuristics that break a complex constraint satisfaction problem into multiple, simpler problems. The verifier's performance depends heavily on the order in which this branching is performed: a poor selection may give rise to exponentially many sub-problems, hampering scalability. Here, we focus on the setting in which many related verification queries must be solved for the same neural network. The core idea is to use past experience to make good branching decisions, expediting verification. We present a reinforcement-learning-based branching heuristic that achieves this, by applying Deep Q-learning from Demonstrations (DQfD). Our experimental evaluation demonstrates a substantial reduction in average verification time and in the average number of iterations required, compared to modern splitting heuristics. These results highlight the great potential of reinforcement learning in the context of neural network verification.

Figures

Figures reproduced from arXiv: 2512.10747 by the authors.

Figure 1
Figure 1. A toy neural network with two inputs [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Cumulative instances solved vs. time (log scale) on setup (i). [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. Cumulative instances solved vs. time (log scale) on setup (ii). [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

36 extracted references · 5 linked inside Pith

  1. [1]

    G. Amir, D. Corsi, R. Yerushalmi, L. Marzari, D. Harel, A. Farinelli, and G. Katz. Verifying Learning-Based Robotic Navigation Systems. InProc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 607–627, 2023

    2023

  2. [2]

    G. Amir, O. Maayan, T. Zelazny, G. Katz, and M. Schapira. Verifying the Gener- alization of Deep Learning to Out-of-Distribution Domains.Journal of Automated Reasoning (JAR), 68(17):1–60, 2024

    2024

  3. [3]

    Bassan, G

    S. Bassan, G. Amir, D. Corsi, I. Refaeli, and G. Katz. Formally Explaining Neural Networks within Reactive Systems. InProc. 23rd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 10–22, 2023

    2023

  4. [4]

    Bassan, Y

    S. Bassan, Y. Elboher, T. Ladner, M. Althoff, and G. Katz. Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations. InProc. 42nd Int. Conf. on Machine Learning (ICML), 2025

    2025

  5. [5]

    C. Brix, S. Bak, T. Johnson, and H. Wu. The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results, 2024. Technical Report. https://arxiv.org/abs/2412.19985

    arXiv 2024

  6. [6]

    Bunel, J

    R. Bunel, J. Lu, I. Turkaslan, P. H. S. Torr, P. Kohli, and M. P. Kumar. Branch and Bound for Piecewise Linear Neural Network Verification.Journal of Machine Learning Research, 21(42):1–39, 2020

    2020

  7. [7]

    Carlini and D

    N. Carlini and D. Wagner. Towards Evaluating the Robustness of Neural Networks. InProc. IEEE Symposium on Security and Privacy (S&P), pages 39–57, 2017

    2017

  8. [8]

    Casadio, E

    M. Casadio, E. Komendantskaya, M. L. Daggitt, W. Kokke, G. Katz, G. Amir, and I. Refaeli. Neural Network Robustness as a Verification Property: A Principled Case Study. InProc. 34th Int. Conf. on Computer Aided Verification (CA V), pages 219–231, 2022

    2022

Show all 36 references
  1. [9]

    Desmartin, O

    R. Desmartin, O. Isac, G. Passmore, E. Komendantskaya, K. Stark, and G. Katz. A Certified Proof Checker for Deep Neural Network Verification in Imandra. In Proc. 16th Int. Conf. on Interactive Theorem Proving (ITP), pages 1:1–1:21, 2025

    2025

  2. [10]

    Elboher, E

    Y. Elboher, E. Cohen, and G. Katz. On Applying Residual Reasoning within Neu- ral Network Verification.Int. Journal on Software and Systems Modeling (SoSyM), 2023

    2023

  3. [11]

    Elboher, R

    Y. Elboher, R. Elsaleh, O. Isac, M. Ducoffe, A. Galametz, G. Pov´ eda, R. Bouma- zouza, N. Cohen, and G. Katz. Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing. InProc. 43rd Digital Avionics Systems Conf. (DASC), pages 1–6, 2024

    2024

  4. [12]

    Elboher, O

    Y. Elboher, O. Isac, G. Katz, T. Ladner, and H. Wu. Abstraction-Based Proof Production in Formal Verification of Neural Networks. InProc. 8th Int. Symposium on AI Verification (SAIV), 2025

    2025

  5. [13]

    Ferrari, M

    C. Ferrari, M. N. Muller, N. Jovanovic, and M. Vechev. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound, 2022. Technical Report. https://arxiv.org/abs/2205.00263

    2022 arXiv

  6. [14]

    Goodfellow, J

    I. Goodfellow, J. Shlens, and C. Szegedy. Explaining and Harnessing Adversarial Examples. InProc. Int. Conf. on Learning Representations (ICLR), 2015

    2015

  7. [15]

    K. He, X. Zhang, S. Ren, and J. Sun. Deep Residual Learning for Image Recogni- tion. InProc. IEEE Conf. on Computer Vision and Pattern Recognition (CVPR), pages 770–778, 2016

    2016

  8. [16]

    Hester, M

    T. Hester, M. Vecerik, O. Pietquin, M. Lanctot, T. Schaul, B. Piot, D. Horgan, J. Quan, A. Sendonaris, I. Osband, G. Dulac-Arnold, J. Agapiou, J. Z. Leibo, and A. Gruslys. Deep Q-learning from Demonstrations.Proc. AAAI Conf. on Artificial Intelligence, 32(1), 2018

    2018

  9. [17]

    O. Isac, I. Refaeli, H. Wu, C. Barrett, and G. Katz. Proof Minimization in Neural Network Verification. InProc. 27th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2026

    2026

  10. [18]

    Jaeckle, J

    F. Jaeckle, J. Lu, and M. P. Kumar. Neural Network Branch-and-Bound for Neural Network Verification, 2021. Technical Report. https://arxiv.org/abs/2107.12855

    2021 arXiv

  11. [19]

    Julian, M

    K. Julian, M. Kochenderfer, and M. Owen. Deep Neural Network Compression for Aircraft Collision Avoidance Systems.Journal of Guidance, Control, and Dynam- ics, 42(3):598–608, 2019

    2019

  12. [20]

    G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. Reluplex: A Calculus for Reasoning about Deep Neural Networks.Formal Methods in System Design (FMSD), 2021

    2021

  13. [21]

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. InProc. Int. Conf. on Computer Aided Verification (CA V), pages 97–117, 2017

    2017

  14. [22]

    G. Katz, D. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zelji´ c, D. Dill, M. Kochenderfer, and C. Barrett. The Marabou Frame- work for Verification and Analysis of Deep Neural Networks. InProc. 31st Int. Conf. on Computer Aided Verificatio...

    2019

  15. [23]

    G. Katz, N. Levy, I. Refaeli, and R. Yerushalmi. DEM: A Method for Certify- ing Deep Neural Network Classifier Outputs in Aerospace. InProc. 43rd Digital Avionics Systems Conf. (DASC), pages 1–8, 2024

    2024

  16. [24]

    Kessler, E

    C. Kessler, E. Komendantskaya, M. Casadio, I. M. Viola, T. Flinkow, A. A. Oth- man, A. Malhotra, and R. McPherson. Neural Network Verification for Gliding Drone Control: A Case Study. InProc. Int. Symposium on AI Verification (SAIV), 2025

    2025

  17. [25]

    Lahav and G

    O. Lahav and G. Katz. Pruning and Slicing Neural Networks using Formal Ver- ification. InProc. 21st Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 183–192, 2021

    2021

  18. [26]

    Mandal, G

    U. Mandal, G. Amir, H. Wu, I. Daukantas, F. Newell, U. Ravaioli, B. Meng, M. Durling, M. Ganai, T. Shim, G. Katz, and C. Barrett. Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. In Proc. 15th Int. Conf. on Formal Methods in Comput...

    2024

  19. [27]

    Mandal, G

    U. Mandal, G. Amir, H. Wu, I. Daukantas, F. Newell, U. Ravaioli, B. Meng, M. Durling, K. Hobbs, M. Ganai, T. Shim, G. Katz, and C. Barrett. Safe and Reliable Training of Learning-Based Aerospace Controllers. InProc. 43rd Digital Avionics Systems Conf. (DASC), pages 1–10, 2024

    2024

  20. [28]

    OpenAI. ChatGPT. https://chatgpt.com, 2022

    2022

  21. [29]

    Q. Qu, X. Li, Y. Zhou, J. Zeng, M. Yuan, J. Wang, J. Lv, K. Liu, and K. Mao. An Improved Reinforcement Learning Algorithm for Learning to Branch, 2022. Technical Report. https://arxiv.org/abs/2201.06213

    2022 arXiv

  22. [30]

    R. S. Sutton and A. G. Barto.Reinforcement Learning: An Introduction. MIT Press, 2018

    2018

  23. [31]

    Swisa and G

    M. Swisa and G. Katz. Learning to Split: A Reinforcement-Learning- Guided Splitting Heuristic for Neural Network Verification (Code). https://github.com/mayaswissa/LearningToSplit, 2025

    2025

  24. [32]

    Szegedy, W

    C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. Intriguing Properties of Neural Networks, 2013. Technical Report. https://arxiv.org/abs/1312.6199

    2013 arXiv

  25. [33]

    van Hasselt, A

    H. van Hasselt, A. Guez, and D. Silver. Deep Reinforcement Learning with Double Q-Learning.Proc. AAAI Conf. on Artificial Intelligence, 30(1):2094–2100, 2016

  26. [34]

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and Z. Kolter. Beta- CROWN: Efficient Bound Propagation with Per-Neuron Split Constraints for Neu- ral Network Robustness Verification. InProc. 35th Conf. on Neural Information Processing Systems (NeurIPS), 2021

    2021

  27. [35]

    H. Wu, A. Ozdemir, A. Zelji´ c, K. Julian, A. Irfan, D. Gopinath, S. Fouladi, G. Katz, C. S. Pasareanu, and C. Barrett. Parallelization Techniques for Verifying Neural Networks. InProc. Formal Methods in Computer-Aided Design (FMCAD), pages 128–137, 2020

    2020

  28. [36]

    H. Wu, A. Zelji´ c, G. Katz, and C. Barrett. Efficient Neural Network Analysis with Sum-of-Infeasibilities. InProc. 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 143–163, 2022

    2022

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.