Pith. sign in

REVIEW 3 major objections 5 minor 53 references

Refactoring Neural Networks for Verification

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read DNN refactoring for verification makes previously inapplicable verifiers work and speeds up safety checks.

desk verdict A useful refactoring-based approach with a soundness problem in one of its two key case studies; worth a major revision, not acceptance as-is. read the letter →

arxiv 1908.08026 v1 pith:XSVPC2O3 submitted 2019-08-06 cs.NE cs.LGcs.SE

David Shriver , Dong Xu , Sebastian Elbaum , Matthew B. Dwyer This is my paper · ORCID
classification cs.NEcs.LGcs.SE
keywords neuralnetworkverificationknowledgedistillationarchitecturetransformationsafety-criticalsystemsautonomousdrivingscalabilitycomplexitysweetspotdeepnetworks
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

R4V claims that a neural network too complex for existing verifiers can be replaced, for safety analysis, by a smaller network produced through automated architecture transformations and knowledge distillation. The transformation removes or shrinks layers and rewrites structures such as residual blocks into forms verifiers accept; distillation trains the smaller student network to reproduce the original's outputs. Case studies on two autonomous-driving networks show verifiers that could not handle the originals proving properties of the refactored versions, often much faster. The aim is to let developers navigate the tradeoff between accuracy and verifiability and find a network that is both accurate enough and checkable within budget.

What carries the argument

The central mechanism is the R4V pipeline: a transformation specification triggers drop, scale, and linearize operations that reshape the teacher architecture into a verifier-friendly student architecture, and then a distillation stage trains that student against the teacher's outputs. The drop operation removes layers, scale shrinks neurons or kernels by a factor, and linearize strips the identity path from residual blocks, with inter-layer shapes updated automatically. Knowledge distillation, training the student to match the teacher's output vectors rather than only the original labels, carries behavioral knowledge across the architectural gap. The paper's organizing concept is the complexity sweet spot: enough complexity to keep error acceptable, little enough to keep verification within the time budget.

What would settle it

Run the original and the refactored network on the same inputs sampled from a property's input region and check whether the student satisfies the property while the teacher violates it, or vice versa, at low relative mean-squared error; a single pair of inputs with opposite answers would show the verification result does not transfer.

Watch

Extended reading notes

Core claim

The central claim is that DNN refactoring for verification expands the applicability and scalability of existing DNN verifiers without discarding the network's learned behavior. Refactoring is defined by two coupled operations: a developer-specified architectural transformation that drops layers, scales layer sizes, and linearizes residual connections, and knowledge distillation, which trains the transformed architecture to match the original network's outputs on training data. Because the student is smaller and uses only verifier-supported layer types, it falls within reach of tools that fail on the original. The case studies show previously inapplicable verifiers returning true or false answers on refactored networks, an eight-fold speedup in one configuration, and a binary-search procedure that converges to networks satisfying both an error threshold and a verification time budget. The paper is explicit that refactoring does not guarantee functional equivalence; it preserves accuracy rather than exact behavior, and verification conclusions are drawn about the refactored network that is deployed.

Load-bearing premise

The load-bearing premise is that verifying the refactored, distilled network gives assurance about the system, even though refactoring only preserves accuracy and does not guarantee that the original and refactored networks behave the same on any given input.

Editorial extensions

If this is right

  • Verifiers that reject unsupported layer types become applicable: after convolutional layers are dropped, a fully-connected-only verifier proved all ten properties of a refactored DAVE-2 network in under a minute each.
  • Verification time drops sharply: one verifier moved from roughly 339 minutes per property with all results unknown on the original DAVE-2 to about 41 minutes per property with all properties proved on the refactored network, while another verifier went from 24-hour timeouts on DroNet to completing three property checks.
  • Developers can locate the complexity sweet spot by binary-searching the number of dropped layers, using relative mean-squared error as the fidelity check and the verification budget as the upper bound.
  • A refactored network that meets both the error threshold and the verification budget is presented as deployable, positioning refactoring as a route to safety arguments for DNN-based systems.

Reading between the lines

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

  • An implication the paper leaves implicit is that a property proved on the student does not automatically transfer to the teacher; a natural next step would be to certify a pointwise output bound between teacher and student and propagate the property through that bound.
  • The relative mean-squared-error stopping rule treats average fidelity as sufficient, but an adversarial or distributionally shifted input could expose a large local divergence that the threshold misses, making local robustness of the student a testable extension.
  • The binary search over dropped layers could be automated into an architecture search whose objective explicitly includes verification time, turning the sweet-spot idea into design-time optimization rather than a manual loop.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper proposes R4V, a framework for 'refactoring' deep neural networks to make them more amenable to formal verification. R4V applies automated architectural transformations (drop layers, scale layers, linearize residual blocks) and then trains the transformed student network via knowledge distillation from the original teacher. The paper presents three case studies on two realistic autonomous-driving networks (DAVE-2 and DroNet) with four verifiers (ReLuplex, ERAN, Neurify, Planet), claiming that R4V enables previously inapplicable verifiers, speeds up verification, and lets developers navigate an accuracy-verifiability tradeoff. The authors explicitly acknowledge that refactoring does not guarantee functional equivalence and instead aims to preserve accuracy, measured by relative mean squared error (MSE) on validation data.

Significance. If the technical issues were resolved, R4V would be a practically useful contribution: it automates a set of simple and parameterizable architecture transformations, couples them with distillation, and provides initial empirical evidence on larger networks than are typical in the DNN verification literature. The paper's strengths include the concrete transformation operators (drop, scale, linearize) in Section III-A, the configurable distillation pipeline, and the breadth of the three case studies spanning four verifiers. The main limitations are that the verification results are obtained on refactored student networks with no formal transfer guarantee to the original network, and that one of the central empirical results, the ERAN false/true classification in Case Study I, rests on an unsound use of an over-approximate abstract domain. The significance of the paper therefore depends on whether these two issues are fixed or the claims are suitably narrowed.

major comments (3)
  1. [Section IV-B, Table II] The procedure used to label ERAN results as 'false' is unsound. The paper states that ERAN was modified to return the lower and upper bounds that it computed for the outputs, and that the authors then checked whether these bounds were within the bounds specified by the property. Since ERAN with the DeepPoly domain computes an over-approximation of the reachable output set, an output interval that is not fully contained in the allowed interval does not imply that there exists a concrete input in the perturbation set violating the property; it may simply be due to abstraction imprecision. As reported, Table II lists 12 false and 0 unknown results for R4V(DroNet)/ERAN. Because this case study is presented as the paper's most significant finding, the classification must be corrected: either report non-contained over-approximate intervals as 'unknown' or provide a concrete counterexample before labeling a property false.
  2. [Sections I and III-B] There is no formal relationship established between the original network and the refactored student network, yet the paper's conclusions transfer verification results from the student to the system. The manuscript explicitly states that refactoring 'does not guarantee functional equivalence' and that behavior preservation is sought only via relative MSE on validation data. Consequently, a property verified on the refactored network does not imply that the original network satisfies the same property. The concluding statement in Section VI that refactored DNNs can be 'subjected to property verification and have acceptable accuracy for deployment' overstates what is shown: at most, the verification applies to the refactored network as a deployed artifact, and even then the relative MSE metric does not bound pointwise deviations or deviations inside the perturbation region used in the properties. The authors should either restrict the safety-related claims to the refactored networks themselves or provide a concrete output-closeness bound (for example, a Lipschitz-style bound over the input region) that makes transfer sound.
  3. [Section V-C and Fig. 5] The 'complexity sweet spot' and the claim that R4V can 'navigate the accuracy-verifiability tradeoff' are based on a single network (DAVE-2), a single verifier (Neurify), and 10 randomly generated properties, with the acceptable-error threshold chosen by the authors. This is acceptable as an exploratory case study, but the conclusion should be phrased as evidence from one artifact rather than a general capability. The paper should also report whether any of the 12 'false' results in Case Study I correspond to actual counterexamples or are artifacts of the over-approximation, since that directly affects the interpretation of the tradeoffs presented in Fig. 5.
minor comments (5)
  1. [Section V-B, Table III] The text says 'Planet was able to finish checking three out of the 10 properties,' but Table III reports 1 true and 2 false results and lists 0 unknown for R4V(DroNet)/Planet; since DroNet has 20 properties total (10 steering and 10 collision, per Section IV-A), the paper should clarify which subset of 10 properties is being discussed and why the table row shows 20 properties.
  2. [Section V-B] The timing comparison for Neurify on the original DAVE-2 network relies on 'the best of up to five tries' due to segmentation errors. The 8x speedup claim should include the number of runs, median timings, and variance, since best-of-five is not a robust estimator of typical performance.
  3. [Fig. 5] The visual encoding of verification results (circle size, color, and pattern) is not fully defined in the text; a legend or explicit caption explaining these encodings would improve readability.
  4. [Section III-C] The paper states that implementation and study artifacts 'will be made available before the work is published'; for reproducibility, a repository URL or DOI should be included in the final version.
  5. [Throughout] The network name is written inconsistently as 'DAVE-2' and 'DA VE-2'; please standardize the notation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: R4V's case-study results come from external verifiers and externally defined properties, not from the paper's own definitions or fitted parameters.

full rationale

The paper's central claims are empirical: refactored networks are submitted to four existing verifiers (ReLuplex, ERAN, Neurify, Planet) on safety properties generated from test data and labels, and the reported true/false/unknown outcomes are produced by those verifiers rather than by R4V's transformation or distillation machinery. The relative MSE thresholds (e.g., 0.01) are user-specified stopping and acceptance criteria, not parameters fitted to the verification outcomes; distillation is a standard Hinton et al. procedure with external provenance. The transformations (drop, scale, linearize) are defined independently of the verification results. The paper explicitly disclaims functional equivalence, so treating refactored-network verification as evidence about the original is a limitation of the safety argument, not a definitional circularity. No load-bearing self-citation chain or imported uniqueness theorem is present; the 'complexity sweet spot' is presented as a conceptual framing and explored via an explicit binary search, not derived from itself. The ERAN modification that treats non-contained over-approximate output intervals as falsifications is a soundness concern about the empirical methodology, not a circularity, because the classification depends on ERAN's abstract interpretation rather than on R4V's own outputs.

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

The central claim rests on the practical reliability of distillation as a behavior-preserving transformation and on the meaningfulness of verifying a surrogate network. No new physical or mathematical entities are introduced, and no parameters are fitted to data to support the main conclusion.

assumptions (4)
  • domain assumption Knowledge distillation can train a student network to closely match the teacher's outputs on the training distribution.
    Invoked in Section III-B as the mechanism for preserving accuracy. The paper relies on relative MSE between student and teacher as the measure of behavior preservation, without a formal bound on generalization outside the training set.
  • domain assumption Verifying safety properties on the refactored network provides useful assurance for the deployed system despite the lack of functional equivalence with the original.
    Introduced in Section I and used in Section V, where verification results on refactored networks are presented as the key findings. If this assumption fails, the safety argument does not transfer from the refactored network to the original architecture.
  • domain assumption The randomly generated safety properties (Chebyshev distance 2 around test images, output bounds) are representative of operational conditions.
    Described in Section IV-A. The properties are synthetic and generated from test data; their relevance to real deployment safety is assumed.
  • domain assumption The bias-variance tradeoff and the observation that DNNs tend not to overfit until very high complexity support the existence of a 'complexity sweet spot'.
    Discussed in Section I with references [29], [30], [31]. The paper assumes that reducing the number of neurons generally increases verification speed while keeping error acceptable, which is an empirical tendency rather than a theorem.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Refactoring Neural Networks for Verification." pith.science (2026). https://pith.science/paper/XSVPC2O3

@misc{pith2026190808026,
  author       = {Pith},
  title        = {Pith review of: Refactoring Neural Networks for Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XSVPC2O3}},
  note         = {Machine review of arXiv:1908.08026}
}
read the original abstract

Deep neural networks (DNN) are growing in capability and applicability. Their effectiveness has led to their use in safety critical and autonomous systems, yet there is a dearth of cost-effective methods available for reasoning about the behavior of a DNN. In this paper, we seek to expand the applicability and scalability of existing DNN verification techniques through DNN refactoring. A DNN refactoring defines (a) the transformation of the DNN's architecture, i.e., the number and size of its layers, and (b) the distillation of the learned relationships between the input features and function outputs of the original to train the transformed network. Unlike with traditional code refactoring, DNN refactoring does not guarantee functional equivalence of the two networks, but rather it aims to preserve the accuracy of the original network while producing a simpler network that is amenable to more efficient property verification. We present an automated framework for DNN refactoring, and demonstrate its potential effectiveness through three case studies on networks used in autonomous systems.

Figures

Figures reproduced from arXiv: 1908.08026 by the authors.

Figure 1
Figure 1. Conceptual diagram depicting (a) the bias-variance [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. The R4V Approach emax and who is willing to wait tmax for verification results. Conceptually, these constraints define a lower bound on DNN complexity, i.e., the complexity necessary to achieve lower error than emax, and an upper bound on DNN complexity, i.e., the complexity beyond which verification time exceeds tmax. These bounds define a complexity sweet spot within which a DNN is both accurate and verifiable. In… view at source ↗
Figure 3
Figure 3. DNN Distillation output, y, is used to drive a gradient-descent process, called backpropagation, which updates the network weights based on their degree of contribution to the loss. The term training parameters refers collectively to the set of choices made in instantiating this training process, including: how the (x, y) are sampled from D, the loss function (e.g., mean squared error, cross entropy), and when to st… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Refactoring the DroNet DNN. C. Network Distillation Hinton et al. [36] introduced knowledge distillation as a general approach to addressing the differing requirements in training and deploying DNNs (e.g., less computation, lower energy consumption). Distillation has p…
Figure 5
Figure 5. Figure 5: Results for Case Study III seconds, and in all cases it returns unknown. When R4V is applied to refactor DAVE-2 by removing the fully-connected layer labeled as ’7’ resulting in 0123456 89A (second row in the graph), we observe a 2.1x speedup in verification time and a…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 39 canonical work pages

  1. [1]

    Imagenet classification with deep convolutional neural networks,

    A. Krizhevsky, I. Sutskever, and G. E. Hinton, “Imagenet classification with deep convolutional neural networks,” in Advances in Neural Information Processing Systems 25 , F. Pereira, C. J. C. Burges, L. Bottou, and K. Q. Weinberger, Eds. Curran Associates, Inc., 2012, pp. 1097–1105. [Online]. Available: http://papers.nips.cc/paper/ 4824-imagenet-classifica...

    2012

  2. [2]

    R. Duda, P. Hart, and D. Stork, Pattern classification , ser. Pattern Classification and Scene Analysis: Pattern Classification. Wiley, 2001. [Online]. Available: https://books.google.com/books?id= YoxQAAAAMAAJ

    work page 2001

  3. [3]

    Playing atari with deep reinforcement learn- ing,

    V . Mnih, K. Kavukcuoglu, D. Silver, A. Graves, I. Antonoglou, D. Wier- stra, and M. Riedmiller, “Playing atari with deep reinforcement learn- ing,” in NIPS Deep Learning Workshop , 2013

    2013

  4. [4]

    Human-level control through deep reinforcement learning,

    V . Mnih, K. Kavukcuoglu, D. Silver, A. A. Rusu, J. Veness, M. G. Bellemare, A. Graves, M. A. Riedmiller, A. Fidjeland, G. Ostrovski, S. Petersen, C. Beattie, A. Sadik, I. Antonoglou, H. King, D. Kumaran, D. Wierstra, S. Legg, and D. Hassabis, “Human-level control through deep reinforcement learning,” Nature, vol. 518, no. 7540, pp. 529–533,

    work page

  5. [5]

    Autonomous naviga- tion of uav by using real-time model-based reinforcement learning,

    N. Imanberdiyev, C. Fu, E. Kayacan, and I. Chen, “Autonomous naviga- tion of uav by using real-time model-based reinforcement learning,” in 2016 14th International Conference on Control, Automation, Robotics and Vision (ICARCV) , Nov 2016, pp. 1–6

    work page 2016

  6. [6]

    Controller design for quadrotor uavs using reinforcement learning,

    H. Bou-Ammar, H. V oos, and W. Ertel, “Controller design for quadrotor uavs using reinforcement learning,” in 2010 IEEE International Confer- ence on Control Applications , Sept 2010, pp. 2130–2135

    work page 2010

  7. [7]

    An analysis of iso 26262: Machine learning and safety in automotive software,

    R. Salay, R. Queiroz, and K. Czarnecki, “An analysis of iso 26262: Machine learning and safety in automotive software,” in SAE Technical Paper . SAE International, 04 2018. [Online]. Available: https://doi.org/10.4271/2018-01-1075

    work page doi:10.4271/2018-01-1075 2018

  8. [8]

    Reluplex: An efficient SMT solver for verifying deep neural networks,

    G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks,” in Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I , 2017, pp. 97–117. [Online]. Available: https://doi.org/10.1007/978-3-319-63387-9 5

    doi:10.1007/978-3-319-63387-9 2017

Show all 53 references
  1. [9]

    Formal verification of piece-wise linear feed-forward neural networks,

    R. Ehlers, “Formal verification of piece-wise linear feed-forward neural networks,” in Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings , 2017, pp. 269–286. [Online]. Available: https://doi....

    2017 doi

  2. [10]

    Output reachable set estimation and verification for multilayer neural networks,

    W. Xiang, H. Tran, and T. T. Johnson, “Output reachable set estimation and verification for multilayer neural networks,” IEEE Transactions on Neural Networks and Learning Systems, vol. 29, no. 11, pp. 5777–5783, Nov 2018

    2018

  3. [11]

    Ai2: Safety and robustness certification of neural networks with abstract interpretation,

    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 (SP), May 2018, pp. 3–18

    2018

  4. [12]

    Reachability analysis of deep neural networks with provable guarantees,

    W. Ruan, X. Huang, and M. Kwiatkowska, “Reachability analysis of deep neural networks with provable guarantees,” in IJCAI. ijcai.org, 2018, pp. 2651–2659

    2018

  5. [13]

    Fast and effective robustness certification,

    G. Singh, T. Gehr, M. Mirman, M. P ¨uschel, and M. Vechev, “Fast and effective robustness certification,” in Advances in Neural Information Processing Systems 31 , S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, Eds. Curran Associates, Inc., 2...

    2018

  6. [14]

    Evaluating robustness of neural networks with mixed integer programming,

    V . Tjeng, K. Y . Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,” in International Conference on Learning Representations , 2019. [Online]. Available: https://openreview.net/forum?id=HyGIdiRqtm

    2019

  7. [15]

    Measuring neural net robustness with constraints,

    O. Bastani, Y . Ioannou, L. Lampropoulos, D. Vytiniotis, A. V . Nori, and A. Criminisi, “Measuring neural net robustness with constraints,” in Proceedings of the 30th International Conference on Neural Information Processing Systems , ser. NIPS’16. USA: Curran Associates Inc.,...

    2016

  8. [16]

    A dual approach to scalable verification of deep networks,

    K. Dvijotham, R. Stanforth, S. Gowal, T. Mann, and P. Kohli, “A dual approach to scalable verification of deep networks,” in Proceedings of the Thirty-Fourth Conference Annual Conference on Uncertainty in Artificial Intelligence (UAI-18). Corvallis, Oregon: AUAI Press, 2018, pp. 162–171

    2018

  9. [17]

    Provable defenses against adversarial examples via the convex outer adversarial polytope,

    E. Wong and J. Z. Kolter, “Provable defenses against adversarial examples via the convex outer adversarial polytope,” in ICML, ser. Proceedings of Machine Learning Research, vol. 80. PMLR, 2018, pp. 5283–5292

    2018

  10. [18]

    Certified defenses against adversarial examples,

    A. Raghunathan, J. Steinhardt, and P. Liang, “Certified defenses against adversarial examples,” in ICLR. OpenReview.net, 2018

    2018

  11. [19]

    Efficient formal safety analysis of neural networks,

    S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana, “Efficient formal safety analysis of neural networks,” in NeurIPS, 2018, pp. 6369–6379

    2018

  12. [20]

    Formal security analysis of neural networks using symbolic intervals,

    ——, “Formal security analysis of neural networks using symbolic intervals,” in USENIX Security Symposium . USENIX Association, 2018, pp. 1599–1614

    2018

  13. [21]

    Towards fast computation of certified robustness for relu networks,

    T. Weng, H. Zhang, H. Chen, Z. Song, C. Hsieh, L. Daniel, D. S. Boning, and I. S. Dhillon, “Towards fast computation of certified robustness for relu networks,” in ICML, ser. Proceedings of Machine Learning Research, vol. 80. PMLR, 2018, pp. 5273–5282

    2018

  14. [22]

    Safety verification of deep neural networks,

    X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks,” in CAV (1), ser. Lecture Notes in Computer Science, vol. 10426. Springer, 2017, pp. 3–29

    2017

  15. [23]

    Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks,

    A. Boopathy, T.-W. Weng, P.-Y . Chen, S. Liu, and L. Daniel, “Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks,” in AAAI, Jan 2019

    2019

  16. [24]

    Output range analysis for deep feedforward neural networks,

    S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output range analysis for deep feedforward neural networks,” in NFM, ser. Lecture Notes in Computer Science, vol. 10811. Springer, 2018, pp. 121–138

    2018

  17. [25]

    A unified view of piecewise linear neural network verification,

    R. R. Bunel, I. Turkaslan, P. H. S. Torr, P. Kohli, and P. K. Mudigonda, “A unified view of piecewise linear neural network verification,” in NeurIPS, 2018, pp. 4795–4804

    2018

  18. [26]

    End to end learning for self- driving cars,

    M. Bojarski, D. D. Testa, D. Dworakowski, B. Firner, B. Flepp, P. Goyal, L. D. Jackel, M. Monfort, U. Muller, J. Zhang, X. Zhang, J. Zhao, and K. Zieba, “End to end learning for self- driving cars,” CoRR, vol. abs/1604.07316, 2016. [Online]. Available: http://arxiv.org/abs/1604.07316

    2016 arXiv

  19. [27]

    Dronet: Learning to fly by driving,

    A. Loquercio, A. I. Maqueda, C. R. D. Blanco, and D. Scaramuzza, “Dronet: Learning to fly by driving,” IEEE Robotics and Automation Letters, 2018

    2018

  20. [28]

    Neural networks and the bias/variance dilemma,

    S. Geman, E. Bienenstock, and R. Doursat, “Neural networks and the bias/variance dilemma,” Neural Computation , vol. 4, no. 1, pp. 1–58, 1992

    1992

  21. [29]

    Non- vacuous generalization bounds at the imagenet scale: A pac-bayesian compression approach,

    W. Zhou, V . Veitch, M. Austern, R. P. Adams, and P. Orbanz, “Non- vacuous generalization bounds at the imagenet scale: A pac-bayesian compression approach,” in Proceedings of the International Conference on Learning Representations (ICLR) , 2019, to appear

    2019

  22. [30]

    Towards understanding the role of over-parametrization in generalization of neural networks,

    B. Neyshabur, Z. Li, S. Bhojanapalli, Y . LeCun, and N. Srebro, “Towards understanding the role of over-parametrization in generalization of neural networks,” in Proceedings of the International Conference on Learning Representations (ICLR) , 2019, to appear

    2019

  23. [31]

    Model compression and acceleration for deep neural networks: The principles, progress, and challenges,

    Y . Cheng, D. Wang, P. Zhou, and T. Zhang, “Model compression and acceleration for deep neural networks: The principles, progress, and challenges,” IEEE Signal Processing Magazine, vol. 35, no. 1, pp. 126– 136, 2018

    2018

  24. [32]

    Fowler, Refactoring: improving the design of existing code

    M. Fowler, Refactoring: improving the design of existing code . Addison-Wesley Professional, 2018

    2018

  25. [33]

    Automated refactoring for testability,

    M. ´O. Cinn´eide, D. Boyle, and I. H. Moghadam, “Automated refactoring for testability,” in 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops. IEEE, 2011, pp. 437–443

    2011

  26. [34]

    Refactoring as testability transformation,

    M. Harman, “Refactoring as testability transformation,” in 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops. IEEE, 2011, pp. 414–421

    2011

  27. [35]

    Exploiting refactoring in formal ver- ification,

    X. Yin, J. Knight, and W. Weimer, “Exploiting refactoring in formal ver- ification,” in 2009 IEEE/IFIP International Conference on Dependable Systems & Networks . IEEE, 2009, pp. 53–62

    2009

  28. [36]

    Distilling the knowledge in a neural network,

    G. Hinton, O. Vinyals, and J. Dean, “Distilling the knowledge in a neural network,” in NIPS Deep Learning and Representation Learning Workshop, 2015. [Online]. Available: http://arxiv.org/abs/1503.02531

    2015 arXiv

  29. [37]

    Goodfellow, Y

    I. Goodfellow, Y . Bengio, and A. Courville, Deep Learning. MIT Press, 2016, http://www.deeplearningbook.org

    2016

  30. [38]

    Deep residual learning for image recognition,

    K. He, X. Zhang, S. Ren, and J. Sun, “Deep residual learning for image recognition,” in 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV , USA, June 27-30, 2016, 2016, pp. 770–778

    2016

  31. [39]

    Algo- rithms for verifying deep neural networks,

    C. Liu, T. Arnon, C. Lazarus, C. Barrett, and M. J. Kochenderfer, “Algo- rithms for verifying deep neural networks,” CoRR, vol. abs/1903.06758, 2019

    1903 arXiv

  32. [40]

    An abstract domain for certifying neural networks,

    G. Singh, T. Gehr, M. P ¨uschel, and M. T. Vechev, “An abstract domain for certifying neural networks,” PACMPL, vol. 3, no. POPL, pp. 41:1– 41:30, 2019

    2019

  33. [41]

    Boosting robustness certification of neural networks,

    G. Singh, T. Gehr, M. P ¨uschel, and M. Vechev, “Boosting robustness certification of neural networks,” in Proceedings of the International Conference on Learning Representations (ICLR) , 2019

    2019

  34. [42]

    Ef- ficient neural network robustness certification with general activation functions,

    H. Zhang, T.-W. Weng, P.-Y . Chen, C.-J. Hsieh, and L. Daniel, “Ef- ficient neural network robustness certification with general activation functions,” in Advances in Neural Information Processing Systems (NuerIPS), dec 2018

    2018

  35. [43]

    Fitnets: Hints for thin deep nets,

    A. Romero, N. Ballas, S. E. Kahou, A. Chassang, C. Gatta, and Y . Bengio, “Fitnets: Hints for thin deep nets,” in Proceedings of the International Conference on Learning Representations (ICLR) , 2015

    2015

  36. [44]

    Learning efficient object detection models with knowledge distillation,

    G. Chen, W. Choi, X. Yu, T. Han, and M. Chandraker, “Learning efficient object detection models with knowledge distillation,” in Advances in Neural Information Processing Systems 30 , I. Guyon, U. V . Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, E...

    2017

  37. [46]

    Preston-Werner, “TOML,” https://github.com/toml-lang/toml, 2013

    T. Preston-Werner, “TOML,” https://github.com/toml-lang/toml, 2013

    2013

  38. [47]

    Open Neural Network Exchange,

    ONNX, “Open Neural Network Exchange,” https://github.com/onnx/ onnx, 2017

    2017

  39. [48]

    Automatic differentiation in pytorch,

    A. Paszke, S. Gross, S. Chintala, G. Chanan, E. Yang, Z. DeVito, Z. Lin, A. Desmaison, L. Antiga, and A. Lerer, “Automatic differentiation in pytorch,” in NIPS-W, 2017

    2017

  40. [49]

    Efficient formal safety analysis of neural networks,

    S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana, “Efficient formal safety analysis of neural networks,” in Advances in Neural Information Processing Systems 31 , S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, Eds. Curran Associates, Inc....

    2018

  41. [50]

    Deepxplore: Automated whitebox testing of deep learning systems,

    K. Pei, Y . Cao, J. Yang, and S. Jana, “Deepxplore: Automated whitebox testing of deep learning systems,” in Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28-31, 2017 , 2017, pp. 1–18. [Online]. Available: https://doi.org/10.1145/3...

    2017

  42. [51]

    Self driving car,

    Udacity, “Self driving car,” https://github.com/udacity/self-driving-car, 2016

    2016

  43. [52]

    Efficient neural architecture search via parameter sharing,

    H. Pham, M. Y . Guan, B. Zoph, Q. V . Le, and J. Dean, “Efficient neural architecture search via parameter sharing,” in Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm¨assan, Stockholm, Sweden, July 10-15, 2018 , 2018, pp. 4092–4101

    2018

  44. [2015]

    Available: https://doi.org/10.1038/nature14236

    [Online]. Available: https://doi.org/10.1038/nature14236

    doi

  45. [2017]

    Available: http://arxiv.org/abs/1704.04861

    [Online]. Available: http://arxiv.org/abs/1704.04861

    arXiv

Pith tools

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