Pith. sign in

REVIEW 2 major objections 5 minor 76 references

A General Framework for Property-Driven Machine Learning

T0 review · 2 major / 5 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read This paper unifies adversarial training and differentiable logics into a single minimax objective that trains neural networks to satisfy logical properties of the form ∀x.

desk verdict A useful unification of adversarial training and differentiable logics, with a nice drone case study, but the advertised generality is narrower than claimed and the empirical satisfaction numbers are attack-dependent estimates. read the letter →

arxiv 2505.00466 v2 pith:WGGFSALT submitted 2025-05-01 cs.LG cs.LO

Thomas Flinkow , Marco Casadio , Colin Kessler , Rosemary Monahan , Ekaterina Komendantskaya This is my paper · ORCID
classification cs.LGcs.LO
keywords property-drivenmachinelearningadversarialtrainingdifferentiablelogicshyper-rectanglesneuralnetworkverificationneuro-symbolicAIconstraintsatisfactioncontrollers
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

Neural networks trained only on data routinely violate safety and correctness properties, so the paper asks whether one training loop can enforce such properties directly. Its answer is a single minimax objective: minimize the usual data loss plus the worst-case differentiable-logic loss of the postcondition over all inputs satisfying the precondition. The precondition is compiled into a union of hyper-rectangles (generalized epsilon-cubes), and the postcondition is compiled into a real-valued logical loss; adversarial training and logical-constraint training become special cases of the same equation. On MNIST and on a glider-drone controller, the paper reports that property-driven training lifts adversarial constraint satisfaction from near zero to above 90 percent in the studied configurations, at the cost of prediction or regression accuracy.

What carries the argument

The load-bearing object is the minimax loss of Eq. (6), built from two translations. The first, $\llbracket P(x)\rrbracket$, maps a logical precondition into one or more hyper-rectangles, sets $\{x \in \mathbb{R}^m : l_i \le x_i \le u_i \text{ for all } i\}$, using union, intersection, and complement; a hyper-rectangle generalizes the $\epsilon$-cube of adversarial training to arbitrary per-dimension bounds. The second, $\llbracket Q(f(x))\rrbracket$, compiles the postcondition into a differentiable-logic loss such as DL2 or fuzzy-logic operators. The inner maximization over $\llbracket P(x)\rrbracket$ is approximated by projected-gradient descent (PGD/AutoPGD), which supplies adversarial examples for the property rather than for a label.

What would settle it

Run a complete neural-network verifier on the trained MNIST and drone models over the same hyper-rectangles used in training and compare its satisfaction verdicts with the paper's PGD-based constraint-security percentages; any violation the verifier finds where the attack found none would show that the reported numbers overestimate property compliance.

Watch

Extended reading notes

Core claim

The paper's central claim is that property-driven training for properties $\forall x. P(x) \rightarrow Q(f(x))$ reduces to the optimization objective $\theta^* = \arg\min_\theta \mathbb{E}_{(x,y)\sim\mathcal{D}}[\lambda L(x,y;f_\theta) + (1-\lambda) \max_{x'\in\llbracket P(x)\rrbracket} \llbracket Q(f(x))\rrbracket(x,x',y;f_\theta)]$, where $\llbracket P(x)\rrbracket$ is the set of hyper-rectangles obtained by interpreting $P$ as a Boolean combination of per-dimension bounds $l_i \le x_i \le u_i$, and $\llbracket Q(f(x))\rrbracket$ is the real-valued loss obtained by interpreting $Q$ in a differentiable logic. The inner maximization searches the hyper-rectangle for the input that most violates the property, in the spirit of adversarial training; the outer minimization adjusts the network weights to reduce that worst-case loss. The paper shows that standard robustness (epsilon-cubes around data points) and ACAS Xu property $\varphi_2$ (a global constraint on sensor readings and advisories) are subcases, and experimentally that the objective raises constraint security on MNIST and on four properties of a learned drone controller.

Load-bearing premise

The inner maximization in the training objective is approximated by projected-gradient attacks, so the reported constraint-security numbers are only as strong as the attack's ability to find near-worst-case inputs inside each hyper-rectangle.

Editorial extensions

If this is right

  • If the objective is correct, then standard local robustness and global properties like ACAS Xu's 'do not advise clear-of-conflict for a distant, slow intruder' are trained by the same code path, so a safety engineer needs one method rather than two.
  • On MNIST, the reported best runs raise constraint security from 0.49% (baseline) to 92.38% (DL2) and 92.18% (fuzzy logic), while prediction accuracy falls from 99.30% to 96.96% and 86.27%.
  • For the drone controller, all four studied properties reach 100% constraint accuracy and at least 71.88% constraint security under property-driven training, whereas the baseline is at most 57.81% constraint accuracy and 34.38% constraint security.
  • A user can specify a constraint abstractly once and instantiate it with any supported differentiable logic, decoupling property specification from the choice of loss semantics.
  • The method is not a formal guarantee: the paper positions it as improving the chances that a subsequently verified network passes, not as a replacement for verification.

Reading between the lines

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

  • Because the precondition is restricted to constant per-dimension bounds, properties whose input regions depend on relations between dimensions, such as the drone controller's original half-space constraints, fall outside the framework; extending the inner maximizer to affine or convex preconditions is a natural test of how far the unification goes.
  • The reported constraint-security numbers inherit the strength of the PGD/AutoPGD attack; a complete verification pass over the same hyper-rectangles would likely produce a stricter and possibly lower satisfaction rate, so cross-checking with a verifier is the immediate next experiment.
  • If better inner maximizers are developed, they should automatically strengthen property-driven training under this objective, making progress in adversarial attacks directly usable for logical-constraint satisfaction.
  • The framework suggests a modular route toward certified training: replace the approximate inner maximization with a sound upper bound on the logical loss, turning the soft penalty into a training signal with formal guarantees.
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

2 major / 5 minor

Summary. The paper presents a unified training framework for property-driven machine learning. The central objective, Eq. (6), augments a standard data loss with a worst-case loss term obtained by maximizing a differentiable-logic translation of a postcondition Q(f(x)) over a hyper-rectangle input region derived from a precondition P(x). The authors show that standard robustness and ACAS Xu-style properties are special cases of this construction, describe a PyTorch implementation, and evaluate the method on MNIST and on a neural network controller for a gliding drone. They report that property-driven training substantially improves constraint satisfaction, measured by CAcc and CSec, at the cost of some prediction performance.

Significance. The proposed framework is a clean and useful unification of two existing lines of work: generalized input region specification via hyper-rectangles and differentiable logics for logical constraints. The formal definition is transparent, and the release of a public implementation is a valuable contribution. The principal claims are the subsumption of known robustness properties and the demonstrated empirical gains in constraint satisfaction. However, the empirical evaluation is attack-based: both training and the CSec metric rely on PGD-style inner maximization, so the reported satisfaction improvements are not verified against complete solvers. If the authors can strengthen the evaluation or clearly delimit the claims, the paper would be a solid contribution to neuro-symbolic ML.

major comments (2)
  1. [§3.1, §3.3, Tables 2–3] The optimization objective in Eq. (6) and the Constraint Security metric in Eq. (21) both depend on the inner maximization over the hyper-rectangle being approximated well by the modified PGD/AutoPGD attack. Since the same attack family is used for both training and evaluation, the reported CSec values (e.g., 92.38% on MNIST, up to 98.44% on the drone properties) may overestimate true property compliance if the attack misses violating points. The paper itself concedes in §5.2 that loss-based methods provide "(almost) no formal guarantees." Please add an independent assessment, for example by running a complete verifier (e.g., an exact branch-and-bound or MILP solver) on the small trained networks, or at least by comparing CSec with a stronger or independent attack and reporting attack convergence evidence. Without this, the headline empirical improvements are not robustly established.
  2. [§3.1] The definition of LP(x)M for arbitrary Boolean preconditions uses complement, union, and intersection, but these operations do not preserve hyper-rectangles: a complement of a box or a disjunction of two boxes is generally not a hyper-rectangle, and may be disconnected or non-convex. This conflicts with the earlier statement that P is limited to constraints with constant lower and upper bounds per dimension, and with the implementation description in §3.3 that the PGD attack works with hyper-rectangles. Please either restrict the formal translation to conjunctions of interval bounds (and state that the framework currently covers only such preconditions), or explain how the attack handles non-rectangular Boolean combinations of boxes.
minor comments (5)
  1. [Eq. (6)] The notation JQ(f(x))K(x,x',y;fθ) suggests the postcondition loss always depends on both x and x', but for several properties (e.g., ϕ1–ϕ3 in the drone case) Q depends only on the new input x'. Please clarify the intended roles of x and x' in the general formulation.
  2. [§3.1] The phrase "translation function L·M from a precondition P(x) into a hyper-rectangle" is inaccurate when P contains negation or disjunction; consider calling the result a "region" or "set" unless these cases are explicitly excluded.
  3. [Table 2 and §4.1] The criterion for the "best-performing experiment" is stated as maximizing the product of PAcc, CAcc, and CSec, but the table only indicates a single boldfaced row; please make the selection rule explicit and reproducible.
  4. [§4.2] The drone properties are defined locally for an input x0, but the manuscript does not specify how x0 is chosen during training and evaluation. Please state whether each training sample serves as an x0, how the corresponding hyper-rectangles are formed, and how the test metrics aggregate over these regions.
  5. [Eq. (20)] CAcc is computed using a single random sample xrnd per test point, which can yield a high-variance estimate of the true fraction of the region satisfying the property. Reporting multiple random samples per test point or confidence intervals would strengthen the evaluation.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: Eq. (6) is a definitional union of hyper-rectangle preconditions and differentiable-logic losses; the same-attack CSec evaluation is a validity caveat, not a derivation-level circularity.

full rationale

The paper's central object, Eq. (6), is introduced as a definition of a training objective rather than derived from a theorem. Its ingredients — hyper-rectangle preconditions LP(x)M from Section 3.1 and differentiable-logic postconditions JQ(f(x))K from Section 3.2 — are combined by an inner maximization over the region, explicitly generalizing Eq. (5) from the authors' earlier differentiable-logic library. The demonstrations that ACAS Xu and standard robustness are special cases are genuine instantiations of the definitions, not conclusions assumed into the definitions. The self-citations ([11], [12], [25], [36]) supply background, evaluation metrics, the prior library, and the drone case study; none is invoked as a theorem that forces Eq. (6), and the central unifying claim does not reduce to those citations. The one point that resembles circularity is evaluative: CSec (Eq. 21) measures satisfaction on PGD-found adversarial samples, while training (Eq. 6) uses a modified PGD attack for the inner maximization. A high CSec therefore measures performance against the same attack family used at training time rather than a formal guarantee of worst-case satisfaction. However, the paper explicitly concedes that 'loss-based methods provide (almost) no formal guarantees' (Section 5.2) and lists certified training as future work, so CSec is not presented as a verification result. The residual concern is attack completeness and evaluation validity, not a derivation that assumes its own conclusion; accordingly, it does not rise to a circular step under the stated rules. The mild score reflects the prominent self-citations and the same-family attack evaluation, while the framework itself remains a self-contained definitional contribution.

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

The framework introduces no new physical or mathematical entities. It relies on prior hyper-rectangle representations, differentiable logics, and PGD. The central claim depends on the bounded-region assumption and the quality of the PGD approximation, neither of which is formally verified.

free parameters (4)
  • MNIST epsilon = 0.3
    Hand-chosen perturbation bound for the standard robustness property; experimental setting, not fitted to data.
  • MNIST delta = 0.05
    Hand-chosen output deviation bound in Eq. (13); experimental setting, not fitted to data.
  • Drone Lipschitz constant L = 0.3
    Hand-chosen Lipschitz bound in property phi4 (Eq. 17); a larger L would be easier to satisfy, so this choice affects the reported constraint satisfaction.
  • Drone property thresholds = 0.187, 0.184, 0.19, -0.12, -0.3, etc.
    Numerical thresholds in Eqs. (14)-(17) and the predicates in Eqs. (22)-(27) are chosen by hand from the output range and input ranges. They define the properties to be learned and directly determine CAcc/CSec values.
assumptions (3)
  • domain assumption The input space is bounded by default lower and upper bounds lmin and umax, inferred from data, and complements of hyper-rectangles are taken relative to this bounding box.
    Footnote 9 states this assumption. It is needed to make the complement operation in the translation of P well-defined and to keep the inner maximization bounded for PGD.
  • domain assumption PGD/AutoPGD over a hyper-rectangle finds points that adequately approximate the true maximum of the differentiable-logic loss in Eq. (6).
    The inner maximization is not solved exactly; Section 3.3 describes a modified AutoPGD. The training and evaluation both rely on this approximation.
  • domain assumption The chosen differentiable logics (DL2, fuzzy logics, STL) provide smooth loss functions whose gradients guide the network toward satisfying the logical postcondition.
    This is the standard assumption for differentiable-logic-based training, inherited from prior work [24, 64, 25]. The paper does not prove any convergence guarantee.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A General Framework for Property-Driven Machine Learning." pith.science (2026). https://pith.science/paper/WGGFSALT

@misc{pith2026250500466,
  author       = {Pith},
  title        = {Pith review of: A General Framework for Property-Driven Machine Learning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WGGFSALT}},
  note         = {Machine review of arXiv:2505.00466}
}
abstract

Neural networks have been shown to frequently fail to learn critical safety and correctness properties purely from data, highlighting the need for training methods that directly integrate logical specifications. While adversarial training can be used to improve robustness to small perturbations within $\epsilon$-cubes, domains other than computer vision -- such as control systems and natural language processing -- may require more flexible input region specifications via generalised hyper-rectangles. Differentiable logics offer a way to encode arbitrary logical constraints as additional loss terms that guide the learning process towards satisfying these constraints. In this paper, we investigate how these two complementary approaches can be unified within a single framework for property-driven machine learning, as a step toward effective formal verification of neural networks. We show that well-known properties from the literature are subcases of this general approach, and we demonstrate its practical effectiveness on a case study involving a neural network controller for a drone system. Our framework is made publicly available at https://github.com/tflinkow/property-driven-ml.

Figures

Figures reproduced from arXiv: 2505.00466 by the authors.

Figure 1
Figure 1. A visualisation of ϵ-cubes (Fig. 1a), hyper-rectangles relative to each data point (Fig. 1b), and a global hyper-rectangle (Fig. 1c). Red dots represent training data, and blue dots represent test data. As noted in [11], verification of neural networks has focused primarily on robustness verification, which requires a classification network f : R m → R n to assign the same class label for each element in each subspa… view at source ↗
Figure 2
Figure 2. Training on MNIST without differentiable logics (baseline), with DL2, and [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. An overview of the Alsomitra-inspired drone controller. The aim of the neural network controller is for the gliding drone to follow a desired trajectory in two-dimensional space (shown in Fig. 3b). The path of the drone is simulated with a two-dimensional aerodynamic model for falling plates with displaced centre of mass [42], whereby the controller actuates the position of the centre of mass to alter the drone traj… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: A scatter plot of predicted vs. true values for all elements in the test set [PITH_FULL_IMAGE:figures/full_fig_p018_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

76 extracted references · 30 canonical work pages

  1. [1]

    Taming Differentiable Logics with Coq Formalisation

    Affeldt, R., Bruni, A., Komendantskaya, E., Ślusarz, N., Stark, K.: Taming Dif- ferentiable Logics with Coq Formalisation (Mar 2024). https://doi.org/10.48550/ arXiv.2403.13700 A General Framework for Property-Driven Machine Learning 19

    work page Pith review arXiv doi:10.48550/arxiv.2403.13700 2024

  2. [2]

    Proceedings of the AAAI Conference on Artificial Intelligence36(11), 13152–13154 (Jun 2022)

    Ahmed, K., Li, T., Ton, T., Guo, Q., Chang, K.W., Kordjamshidi, P., Srikumar, V., den Broeck, G.V., Singh, S.: PYLON: A PyTorch Framework for Learning with Constraints. Proceedings of the AAAI Conference on Artificial Intelligence36(11), 13152–13154 (Jun 2022). https://doi.org/10.1609/aaai.v36i11.21711

    doi:10.1609/aaai.v36i11.21711 2022

  3. [3]

    In: Advances in Neural Information Processing Systems (Oct 2022)

    Ahmed, K., Teso, S., Chang, K.W., den Broeck, G.V., Vergari, A.: Semantic Prob- abilistic Layers for Neuro-Symbolic Learning. In: Advances in Neural Information Processing Systems (Oct 2022)

    work page 2022

  4. [4]

    https: //doi.org/10.48550/arXiv.2109.10317

    Albarghouthi, A.: Introduction to Neural Network Verification (Oct 2021). https: //doi.org/10.48550/arXiv.2109.10317

    arXiv doi:10.48550/arxiv.2109.10317 2021

  5. [5]

    https://doi.org/10.48550/arXiv.2109.00498

    Bak, S., Liu, C., Johnson, T.: The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results (Aug 2021). https://doi.org/10.48550/arXiv.2109.00498

    arXiv doi:10.48550/arxiv.2109.00498 2021

  6. [6]

    In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W

    Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn Clause Solvers for Program Verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II, vol. 9300, pp. 24–

    work page

  7. [7]

    https://doi.org/10.48550/arXiv.2312.16760

    Brix, C., Bak, S., Liu, C., Johnson, T.T.: The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results (Dec 2023). https://doi.org/10.48550/arXiv.2312.16760

    arXiv doi:10.48550/arxiv.2312.16760 2023

  8. [8]

    Interna- tional Journal on Software Tools for Technology Transfer25(3), 329–339 (Jun 2023)

    Brix, C., Müller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). Interna- tional Journal on Software Tools for Technology Transfer25(3), 329–339 (Jun 2023). https://doi.org/10.1007/s10009-023-00703-4

    doi:10.1007/s10009-023-00703-4 2023

Show all 76 references
  1. [9]

    Journal of Machine Learning Research 21 (2020)

    Bunel, R., Turkaslan, I., Torr, P., Pawan Kumar, M., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21 (2020)

    2020

  2. [10]

    In: Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems

    Casadio, M., Arnaboldi, L., Daggitt, M., Isac, O., Dinkar, T., Kienitz, D., Rieser, V., Komendantskaya, E.: ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification. In: Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Syste...

  3. [11]

    European Journal of Applied Mathematics pp

    Casadio, M., Dinkar, T., Komendantskaya, E., Arnaboldi, L., Daggitt, M.L., Isac, O., Katz, G., Rieser, V., Lemon, O.: NLP verification: Towards a general methodology for certifying robustness. European Journal of Applied Mathematics pp. 1–58 (Apr 2025). https://doi.org/10.1017...

    2025 doi

  4. [12]

    In: Shoham, S., Vizel, Y

    Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural Network Robustness as a Verification Property: A Principled Case Study. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. pp. 219–231. Lecture Notes in Computer Scien...

    2022 doi

  5. [13]

    Certini, D.: Flight of Alsomitra Macrocarpa. Ph.D. thesis, University of Edinburgh (Feb 2023). https://doi.org/10.7488/era/3088

    2023 doi

  6. [14]

    In: Pro- ceedings of the 35th International Conference on Machine Learning

    Chen, Z., Badrinarayanan, V., Lee, C.Y., Rabinovich, A.: GradNorm: Gradient Normalization for Adaptive Loss Balancing in Deep Multitask Networks. In: Pro- ceedings of the 35th International Conference on Machine Learning. pp. 794–803. PMLR (Jul 2018)

    2018

  7. [15]

    In: Proceedings of the 37th International Conference on Machine Learning

    Croce,F.,Hein,M.:Reliableevaluationofadversarialrobustnesswithanensembleof diverse parameter-free attacks. In: Proceedings of the 37th International Conference on Machine Learning. pp. 2206–2216. PMLR (Nov 2020) 20 T. Flinkow et al

    2020

  8. [16]

    International Journal of Computer Vision128(4), 1028–1046 (Apr 2020)

    Croce, F., Rauber, J., Hein, M.: Scaling up the Randomized Gradient-Free Ad- versarial Attack Reveals Overestimation of Robustness Using Established At- tacks. International Journal of Computer Vision128(4), 1028–1046 (Apr 2020). https://doi.org/10.1007/s11263-019-01213-0

    2020 doi

  9. [17]

    In: Kalpa Publications in Computing

    Daggitt, M., Kokke, W., Komendantskaya, E., Atkey, R., Arnaboldi, L., Slusarz, N., Casadio, M., Coke, B., Lee, J.: The Vehicle Tutorial: Neural Network Verification with Vehicle. In: Kalpa Publications in Computing. vol. 16, pp. 1–5. EasyChair (Oct 2023). https://doi.org/10.29007/5s2x

    2023 doi

  10. [18]

    In: Proceedings of the 12th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs

    Daggitt, M.L., Atkey, R., Kokke, W., Komendantskaya, E., Arnaboldi, L.: Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Construc- tively. In: Proceedings of the 12th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs. pp. 1...

    2023

  11. [19]

    https://doi.org/10.48550/ arXiv.2402.01353

    Daggitt, M.L., Kokke, W., Atkey, R.: Efficient compilation of expressive problem space specifications to neural network solvers (Jan 2024). https://doi.org/10.48550/ arXiv.2402.01353

    2024 doi

  12. [20]

    Daggitt, M.L., Kokke, W., Atkey, R., Arnaboldi, L., Komendantskya, E.: Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers (Feb 2022)

    2022

  13. [21]

    https://doi.org/10.48550/arXiv.2401.06379

    Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Jan 2024). https://doi.org/10.48550/arXiv.2401.06379

    2024 doi arXiv

  14. [22]

    Artificial Intelligence244, 143–165 (Mar 2017)

    Diligenti, M., Gori, M., Saccà, C.: Semantic-based regularization for learning and inference. Artificial Intelligence244, 143–165 (Mar 2017). https://doi.org/10.1016/ j.artint.2015.08.011

    2017

  15. [23]

    In: Ferrari, A., Penzenstadler, B

    Farrell, M., Mavridou, A., Schumann, J.: Exploring Requirements for Software that Learns: A Research Preview. In: Ferrari, A., Penzenstadler, B. (eds.) Re- quirements Engineering: Foundation for Software Quality. pp. 179–188. Lec- ture Notes in Computer Science, Springer Natur...

    2023 doi

  16. [24]

    In: Proceedings of the 36th International Conference on Machine Learning

    Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.: DL2: Training and Querying Neural Networks with Logic. In: Proceedings of the 36th International Conference on Machine Learning. pp. 1931–1941. PMLR (May 2019)

    1931

  17. [25]

    Science of Computer Programming244, 103280 (Sep 2025)

    Flinkow, T., Pearlmutter, B.A., Monahan, R.: Comparing differentiable logics for learning with logical constraints. Science of Computer Programming244, 103280 (Sep 2025). https://doi.org/10.1016/j.scico.2025.103280

    2025

  18. [26]

    In: Pro- ceedings of the 40th ACM/SIGAPP Symposium on Applied Computing

    Flood, R., Casadio, M., Aspinall, D., Komendantskaya, E.: Formally Verifying Robustness and Generalisation of Network Intrusion Detection Models. In: Pro- ceedings of the 40th ACM/SIGAPP Symposium on Applied Computing. SAC ’25, Association for Computing Machinery, New York, NY...

    2025

  19. [27]

    In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence

    Giunchiglia, E., Stoian, M.C., Lukasiewicz, T.: Deep Learning with Logical Con- straints. In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence. pp. 5478–5485. International Joint Conferences on Artificial Intelligence Organization, Vien...

    2022

  20. [28]

    Giunchiglia, E., Tatomir, A., Stoian, M.C., Lukasiewicz, T.: CCN+: A neuro- symbolic framework for deep learning with requirements. Int. J. Approx. Reasoning 171(C) (Aug 2024). https://doi.org/10.1016/j.ijar.2024.109124

    2024

  21. [29]

    https://doi.org/10.48550/arXiv.1412.6572 A General Framework for Property-Driven Machine Learning 21

    Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and Harnessing Adversarial Examples (Mar 2015). https://doi.org/10.48550/arXiv.1412.6572 A General Framework for Property-Driven Machine Learning 21

    2015 doi arXiv

  22. [30]

    In: 2019 IEEE/CVF International Conference on Computer Vision (ICCV)

    Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T.A., Kohli, P.: Scalable Verified Training for Provably Robust Image Classification. In: 2019 IEEE/CVF International Conference on Computer Vision (ICCV). pp. 4841–4850 (Oct 2019)...

    2019

  23. [31]

    Computer Science Review37, 100270 (Aug 2020)

    Huang, X., Kroening, D., Ruan, W., Sharp, J., Sun, Y., Thamo, E., Wu, M., Yi, X.: A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Computer Science Review37, 100270 (Aug 2020). https://...

    2020

  24. [32]

    In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC)

    Julian, K.D., Lopez, J., Brush, J.S., Owen, M.P., Kochenderfer, M.J.: Policy compression for aircraft collision avoidance systems. In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC). pp. 1–10 (Sep 2016). https://doi. org/10.1109/DASC.2016.7778091

    2016

  25. [33]

    https://doi.org/10.48550/arXiv.1702.01135

    Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (arXiv:1702.01135) (May 2017). https://doi.org/10.48550/arXiv.1702.01135

    2017 doi arXiv

  26. [34]

    In: Majumdar, R., Kunčak, V

    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 97–117. Lecture Notes in Computer Science, Springer International Publi...

    2017 doi

  27. [35]

    In: Dillig, I., Tasiran, S

    Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.: The Marabou Framework for Verification and Analysis of Deep Neural Networks. In: Dillig, I., Tasiran, S. (eds.) Compute...

    2019 doi

  28. [36]

    https://doi.org/10.48550/arXiv.2505.00622

    Kessler, C., Komendantskaya, E., Casadio, M., Viola, I.M., Flinkow, T., Othman, A.A., Malhotra, A., McPherson, R.: Neural Network Verification for Gliding Drone Control: A Case Study (May 2025). https://doi.org/10.48550/arXiv.2505.00622

    2025 doi arXiv

  29. [37]

    In: Decision Making Under Uncertainty: Theory and Application, pp

    Kochenderfer, M.J., Amato, C., Chowdhary, G., How, J.P., Reynolds, H.J.D., Thornton, J.R., Torres-Carrasquillo, P.A., Ure, N.K., Vian, J.: Optimized Air- borne Collision Avoidance. In: Decision Making Under Uncertainty: Theory and Application, pp. 249–276. MIT Press (2015)

    2015

  30. [38]

    Kochenderfer, M.J., Chryssanthacopoulos, J.P.: Robust Airborne Collision Avoid- ance through Dynamic Programming. Tech. Rep. ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (Jan 2011)

    2011

  31. [39]

    Krizhevsky, A.: Learning Multiple Layers of Features from Tiny Images (2009)

    2009

  32. [40]

    https://doi.org/10.48550/arXiv.2503.19466

    Kurscheidt, L., Morettin, P., Sebastiani, R., Passerini, A., Vergari, A.: A Prob- abilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction (Jun 2025). https://doi.org/10.48550/arXiv.2503.19466

    2025 doi arXiv

  33. [41]

    Proceedings of the IEEE86(11), 2278–2324 (Nov 1998)

    Lecun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proceedings of the IEEE86(11), 2278–2324 (Nov 1998). https://doi.org/10.1109/5.726791

    1998 doi

  34. [42]

    Journal of Fluid Mechanics937, A6 (Apr 2022)

    Li, H., Goodwill, T., Jane Wang, Z., Ristroph, L.: Centre of mass location, flight modes, stability and dynamic modelling of gliders. Journal of Fluid Mechanics937, A6 (Apr 2022). https://doi.org/10.1017/jfm.2022.89

    2022 doi

  35. [43]

    Foundations and Trends in Optimization 4(3-4), 244–404 (Feb 2021)

    Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algo- rithms for Verifying Deep Neural Networks. Foundations and Trends in Optimization 4(3-4), 244–404 (Feb 2021). https://doi.org/10.1561/2400000035 22 T. Flinkow et al

    2021 doi

  36. [44]

    In: Enea, C., Lal, A

    Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: The Neural Network Verification Tool. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 397–412. Springer Nature Switzerland, Cham (2023). https://doi.org/10.1007/ 978-3-031-37703-7_19

    2023

  37. [45]

    In: International Conference on Learning Representations (Sep 2018)

    Loshchilov, I., Hutter, F.: Decoupled Weight Decay Regularization. In: International Conference on Learning Representations (Sep 2018)

    2018

  38. [46]

    In: International Conference on Learning Representations (Feb 2018)

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards Deep Learning Models Resistant to Adversarial Attacks. In: International Conference on Learning Representations (Feb 2018)

    2018

  39. [47]

    In: Advances in Neural Infor- mation Processing Systems

    Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., De Raedt, L.: Deep- ProbLog: Neural Probabilistic Logic Programming. In: Advances in Neural Infor- mation Processing Systems. vol. 31. Curran Associates, Inc. (2018)

    2018

  40. [48]

    In: Proceedings of the 11th Int

    Manzanas Lopez, D., Althoff, M., Benet, L., Blab, C., Forets, M., Jia, Y., Johnson, T.T., Kranzl, M., Ladner, T., Linauer, L., Neubauer, P., Neubauer, S., Schilling, C., Zhang, H., Zhong, X.: ARCH-COMP24 Category Report: Artificial Intelligence and Neural Network Control Syste...

    2024 doi

  41. [49]

    Cambridge Uni- versity Press, 1 edn

    Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge Uni- versity Press, 1 edn. (Jun 2012). https://doi.org/10.1017/CBO9781139021326

    2012 doi

  42. [50]

    In: Proceedings of the 35th International Conference on Machine Learning

    Mirman, M., Gehr, T., Vechev, M.: Differentiable Abstract Interpretation for Prov- ably Robust Neural Networks. In: Proceedings of the 35th International Conference on Machine Learning. pp. 3578–3586. PMLR (Jul 2018)

    2018

  43. [51]

    https://doi.org/10.1007/ 978-3-319-23534-9_2

    Springer International Publishing, Cham (2015). https://doi.org/10.1007/ 978-3-319-23534-9_2

    2015

  44. [52]

    https://doi.org/10.48550/ arXiv.1810.12042

    Mosbach, M., Andriushchenko, M., Trost, T., Hein, M., Klakow, D.: Logit Pairing Methods Can Fool Gradient-Based Attacks (Mar 2019). https://doi.org/10.48550/ arXiv.1810.12042

    2019 doi arXiv

  45. [53]

    https://doi.org/10.48550/arXiv.2212.10376

    Müller, M.N., Brix, C., Bak, S., Liu, C., Johnson, T.T.: The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results (Dec 2022). https://doi.org/10.48550/arXiv.2212.10376

    2022 doi arXiv

  46. [54]

    In: Advances in Neural Information Processing Systems

    Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., Desmaison, A., Kopf, A., Yang, E., DeVito, Z., Raison, M., Tejani, A., Chilamkurthy, S., Steiner, B., Fang, L., Bai, J., Chintala, S.: PyTorch: An Imperativ...

    2019

  47. [55]

    In: International Conference on Learning Representations (Feb 2018)

    Raghunathan, A., Steinhardt, J., Liang, P.: Certified Defenses against Adversarial Examples. In: International Conference on Learning Representations (Feb 2018)

    2018

  48. [56]

    https://doi.org/10.48550/arXiv

    Serafini, L., d’Avila Garcez, A.: Logic Tensor Networks: Deep Learning and Logical Reasoning from Data and Knowledge (Jul 2016). https://doi.org/10.48550/arXiv. 1606.04422

    2016 doi arXiv

  49. [57]

    In:Lahiri,S.K.,Wang,C.(eds.)AutomatedTechnologyforVerificationandAnalysis

    Seshia, S.A., Desai, A., Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Shivakumar, S., Vazquez-Chanlatte, M., Yue, X.: Formal Specification for Deep Neural Networks. In:Lahiri,S.K.,Wang,C.(eds.)AutomatedTechnologyforVerificationandAnalysis. pp. 20–34. Lecture Notes in Comput...

    2018 doi

  50. [58]

    https: //doi.org/10.48550/arXiv.2405.21063

    Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsieh, C.J., Zhang, H.: Neural Network Verification with Branch-and-Bound for General Nonlinearities (May 2024). https: //doi.org/10.48550/arXiv.2405.21063

    2024 doi arXiv

  51. [59]

    In: EPiC Series in A General Framework for Property-Driven Machine Learning 23 Computing

    Ślusarz, N., Komendantskaya, E., Daggitt, M., Stewart, R., Stark, K.: Logic of Differentiable Logics: Towards a Uniform Semantics of DL. In: EPiC Series in A General Framework for Property-Driven Machine Learning 23 Computing. vol. 94, pp. 473–493. EasyChair (Jun 2023). https:...

    2023

  52. [60]

    In: The Thirteenth International Conference on Learning Representations (Oct 2024)

    Stoian, M.C., Giunchiglia, E.: Beyond the convexity assumption: Realistic tabular data generation under quantifier-free real linear constraints. In: The Thirteenth International Conference on Learning Representations (Oct 2024)

    2024

  53. [61]

    https://doi.org/10

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks (Feb 2014). https://doi.org/10. 48550/arXiv.1312.6199

    2014 doi arXiv

  54. [62]

    In: Lahiri, S.K., Wang, C

    Tran, H.D., Yang, X., Manzanas Lopez, D., Musau, P., Nguyen, L.V., Xiang, W., Bak, S., Johnson, T.T.: NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification. ...

    2020

  55. [63]

    In: International Conference on Learning Representations (Sep 2018)

    Tsipras, D., Santurkar, S., Engstrom, L., Turner, A., Madry, A.: Robustness May Be at Odds with Accuracy. In: International Conference on Learning Representations (Sep 2018)

    2018

  56. [64]

    https://doi.org/10.48550/arXiv.2104.02466

    Urban, C., Miné, A.: A Review of Formal Methods applied to Machine Learning (arXiv:2104.02466) (Apr 2021). https://doi.org/10.48550/arXiv.2104.02466

    2021 doi arXiv

  57. [65]

    Artificial Intelligence302, 103602 (Jan 2022)

    van Krieken, E., Acar, E., van Harmelen, F.: Analyzing Differentiable Fuzzy Logic Operators. Artificial Intelligence302, 103602 (Jan 2022). https://doi.org/10.1016/ j.artint.2021.103602

    2022

  58. [66]

    https://doi.org/10.48550/arXiv

    van Krieken, E., Badreddine, S., Manhaeve, R., Giunchiglia, E.: ULLER: A Unified Language for Learning and Reasoning (May 2024). https://doi.org/10.48550/arXiv. 2405.00532

    2024 doi arXiv

  59. [67]

    In: 2020 American Control Conference (ACC)

    Varnai, P., Dimarogonas, D.V.: On Robustness Metrics for Learning STL Tasks. In: 2020 American Control Conference (ACC). pp. 5394–5399 (Jul 2020). https: //doi.org/10.23919/ACC45564.2020.9147692

    2020

  60. [68]

    https://doi.org/10.48550/arXiv.2103.06624

    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 Complete and Incomplete Neural Network Robustness Verification (Oct 2021). https://doi.org/10.48550/arXiv.2103.06624

    2021 doi arXiv

  61. [69]

    In: Proceedings of the 35th International Conference on Machine Learning

    Wong, E., Kolter, Z.: Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In: Proceedings of the 35th International Conference on Machine Learning. pp. 5286–5295. PMLR (Jul 2018)

    2018

  62. [70]

    In: Advances in Neural Information Processing Systems

    Wong, E., Schmidt, F., Metzen, J.H., Kolter, J.Z.: Scaling provable adversarial defenses. In: Advances in Neural Information Processing Systems. vol. 31. Curran Associates, Inc. (2018)

    2018

  63. [71]

    https://doi.org/10.48550/arXiv.2401

    Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks (May 2024). https:...

    2024 doi

  64. [72]

    https://doi.org/ 10.48550/arXiv.1711.11157

    Xu, J., Zhang, Z., Friedman, T., Liang, Y., den Broeck, G.V.: A Semantic Loss Function for Deep Learning with Symbolic Knowledge (Jun 2018). https://doi.org/ 10.48550/arXiv.1711.11157

    2018 doi arXiv

  65. [73]

    https://doi.org/10.48550/arXiv.2002.12920 24 T

    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 (Oct 2020). https://doi.org/10.48550/arXiv.2002.12920 24 T. Flinkow et al

    2020 doi arXiv

  66. [74]

    https://doi.org/10.48550/arXiv

    Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., Hsieh, C.J.: Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers (Mar 2021). https://doi.org/10.48550/arXiv. 2011.13824

    2021 doi arXiv

  67. [75]

    https://doi.org/10.48550/arXiv.2208.05740

    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 (Dec 2022). https://doi.org/10.48550/arXiv.2208.05740

    2022 doi arXiv

  68. [76]

    https://doi.org/10.48550/arXiv.1811.00866

    Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient Neural Network Robustness Certification with General Activation Functions (Nov 2018). https://doi.org/10.48550/arXiv.1811.00866

    2018 doi arXiv

Pith tools

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