Pith. sign in

REVIEW 4 major objections 5 minor 1 cited by

Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces

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

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

Pith's one-line read Machine-checked proofs show a loss for linear temporal logic on finite traces (LTLf) matches the boolean semantics, verifies its derivative, and generates OCaml code that steers learned trajectories to obey constraints.

desk verdict A credible, machine-checked formalisation of tensor-based LTLf with a verified loss and derivative; the formal core deserves referee time, while the empirical claims are only demonstrations and the missing artifacts are the main gap. read the letter →

arxiv 2501.13712 v1 pith:CXEAQTRE submitted 2025-01-23 cs.AI cs.LGcs.LO

Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot This is my paper · ORCID
classification cs.AIcs.LGcs.LO
keywords LTLftensorsemanticsformalverificationIsabelle/HOLneurosymboliclearningdifferentiablelossfunctioncodegenerationtrajectoryplanning
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 tries to establish that logical constraints can be given a machine-checked, provably correct implementation for neural training. It formalises linear temporal logic on finite traces (LTLf) over tensors in the Isabelle/HOL proof assistant, defines a smooth loss function $L$ and its derivative $dL$, and proves that $L$ tends to zero as the smoothing parameter $\gamma$ tends to zero exactly when the constraint's boolean semantics evaluate to true. Because executable OCaml code is generated from the same formal specification, the optimiser used inside PyTorch inherits the proofs, removing the manual step of re-implementing logic in a language like Python. The approach matters because it converts statements such as "avoid a region", "eventually reach a point", or "loop back on itself" into gradients a neural network can follow, with mathematical certainty about what the loss actually measures. Trajectory-planning experiments show the constraints visibly changing learned paths.

What carries the argument

The load-bearing object is a tensor-based encoding of LTLf semantics paired with a smoothed counterpart. A trace is an order-$n$ real tensor with time as its first dimension; the boolean semantics $\mathrm{eval}(\rho, T, t)$ recurses over the constraint and the temporal index, returning a boolean tensor over the batch dimensions, while the loss $L(\rho, T, t, \gamma)$ mirrors $\mathrm{eval}$ case by case, replacing conjunction and disjunction with the log-sum-exp soft functions $\max_\gamma(a, b) = \gamma \ln(e^{a/\gamma} + e^{b/\gamma})$ and $\min_\gamma(a, b) = -\gamma \ln(e^{-a/\gamma} + e^{-b/\gamma})$, atomic inequality with $\max_\gamma(\phi_1 - \phi_2, 0)$, and inequality-of-values with a Gaussian $e^{-a^2/2\gamma^2}$. The derivative $dL$ is defined by recursion using the chain rule, with a backsubt indicator tensor acting as the derivative of the subtensor-extraction operation, and every derivative case is formally proved. Code equations then bridge the gap between proofs and performance: formally proved equivalent redefinitions, such as a case-split version of $\max_\gamma$ that avoids exponent overflow, give efficient executable code that still satisfies the verified properties.

What would settle it

Run the generated OCaml implementation of $L$ and $dL$ inside PyTorch on adversarial traces: for each temporal operator, search for a trace where the boolean $\mathrm{eval}$ is true but $L$ is bounded away from zero, or vice versa, across $\gamma$ values such as 0.001 to 0.5. Also compare, at machine precision, PyTorch's autograd gradient of the implemented $L$ against the code-generated $dL$ on random traces; a single mismatch would show the verified derivative does not govern the actual optimisation.

Watch

Extended reading notes

Core claim

The paper's central claim is that a differentiable loss function for LTLf constraints can be specified, proved correct, and compiled within a single formal framework. Isabelle/HOL formalises a boolean evaluation function $\mathrm{eval}$ over tensors representing batches of finite traces, and a smooth loss $L$ built from soft versions of max and min, each carrying a smoothing parameter $\gamma$. Two formal theorems carry the argument: $\mathrm{lookup}(i, L(\rho, T, t, \gamma))$ is non-negative at $\gamma = 0$, and it tends to 0 as $\gamma$ tends to 0 if and only if $\mathrm{lookup}(i, \mathrm{eval}(\rho, T, t))$ is true, establishing that minimising the smooth loss coincides with satisfying the logic. A further formal theorem proves that $dL$, defined recursively through the chain rule, is the derivative of $L$ with respect to every element of the input trace tensor. Isabelle's code generation turns both $L$ and $dL$ into OCaml functions that act as the forward and backward passes of a PyTorch optimiser, and experiments with dynamic movement primitives show learned trajectories changing so as to satisfy constraints such as avoidance, patrolling, and a double loop.

Load-bearing premise

The chain of guarantees holds only if Isabelle's code generation faithfully translates the formal specification into working OCaml, and if the mathematical reals and limits in the proofs behave the same as the floating-point arithmetic PyTorch actually executes at the chosen $\gamma = 0.005$.

Editorial extensions

If this is right

  • Any LTLf constraint expressible in the language becomes a loss whose zero set, in the $\gamma \to 0$ limit, coincides exactly with the traces satisfying the constraint, so gradient descent and logical satisfaction are provably aligned.
  • The same formal pipeline transfers to other temporal or continuous logics: the authors state that signal temporal logic is being formalised next within the same framework.
  • In the demonstrations, constrained training visibly alters learned trajectories to avoid regions, patrol points, respect an until-constraint, and perform a double loop, while the tensor-based formulation runs at least ten times faster than the authors' earlier scalar pipeline.
  • The double-loop experiments show that a logically weaker, conjoined constraint can suffice when trajectories are represented by dynamic movement primitives but not for raw coordinate sequences, so constraint selection and domain representation interact.

Reading between the lines

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

  • A natural stress test is adversarial: soundness is proved for mathematical reals and for the limit $\gamma \to 0$, so behaviour at fixed $\gamma$ and finite precision is an empirical matter; annealing $\gamma$ during training, which the authors list as future work, would directly probe how close to that limit realistic runs sit.
  • The OCaml code is framework-agnostic, so the same verified loss could be dropped into planning or scheduling domains, or into other deep-learning frameworks, without touching the formal proofs.
  • The formal guarantees currently stop at the loss; extending the same treatment to the neural network or the dynamic movement primitive parameters would close the gap the authors acknowledge, where the experimental domain itself sits outside the formal environment.
  • The conjoined-versus-nested constraint result suggests that representation choice changes which constraints are safe to relax, pointing toward a formal criterion for when a relaxation preserves the set of achievable behaviours under gradient descent.
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 presents an Isabelle/HOL formalisation of a tensor-based semantics for linear temporal logic on finite traces (LTLf), together with a smooth loss function L and a derivative function dL. The authors prove in Isabelle that L is non-negative at gamma=0 and that, in the limit gamma->0, L tends to zero exactly when the boolean evaluation eval is true; they also state that dL is the verified derivative of L. They use Isabelle's code generation to produce OCaml code for L and dL, integrate this code into PyTorch, and demonstrate the pipeline on direct trajectory optimisation and on dynamic movement primitive learning with several LTLf constraints.

Significance. The formalisation is a genuinely useful contribution: machine-checked soundness of a differentiable LTLf loss with respect to an independently defined boolean semantics is a high bar, and the verified derivative plus code generation gives a credible route from formal specifications to usable neurosymbolic loss functions. The paper also provides an instructive experiment showing that the choice of trajectory representation (DMP versus pointwise coordinates) affects whether a relaxed LTLf constraint achieves the desired behaviour. The empirical sections are considerably weaker than the formal sections: the reported constraint metric is the soft loss itself, there is no independent boolean evaluation of the final traces, and no statistical information is given. The formal claims also need a precise statement of the derivative theorem and a clear scoping of what the verified code generation actually guarantees at the floating-point level.

major comments (4)
  1. [4.2.4 / Table 1] The only constraint metric reported in the experiments is L itself, the same soft loss that is minimised during training. Since L is directly optimised, a low L does not demonstrate LTLf satisfaction, and the soundness theorem in Section 3.2.2 is an asymptotic statement at gamma->0, whereas the experiments use gamma=0.005 and report nonzero L. The manuscript should report eval(rho, Q, 0), or at least a hard violation count, on the final learned trajectories for each of the five tasks. Without such an independent metric, the empirical claim in Section 5.2 that the constraints 'successfully change the training process to match the desired behaviour' is not quantitatively supported.
  2. [3.3 / 3.4] The paper correctly acknowledges in Section 3.3 that properties proved over the mathematical reals may not hold over floating-point numbers, but Sections 2.5 and 3.3 elsewhere state that code generation guarantees that the generated code retains the formally proven properties. The executed code uses IEEE floating-point arithmetic and the alternative code equation for max_gamma, while the soundness and derivative theorems are proved for the original real-valued definitions. The central claim should be restated as applying to the mathematical specification, with the floating-point executable treated as a separate, unverified (or independently validated) artifact; as written, the formal guarantee is narrower than the abstract and Section 5.2 suggest.
  3. [3.2.2 / 3.4] The precise meaning of the claim that dL is the derivative of L is not stated. L returns a tensor of order n-2, whereas dL returns a tensor of the same shape as the input trace T; the paper does not specify whether dL is the gradient of a single per-trace loss, the Jacobian, or the gradient of a sum over a batch. Section 3.4 also does not explain how dL is combined with PyTorch's autograd when L is used as a possibly batched loss. The authors should state the Isabelle theorem precisely, including the scalar or vector whose gradient is computed, and describe the backward-pass composition in enough detail that the claimed verified gradient is unambiguous.
  4. [4.2.2] The formally verified object is L(rho, T, t, gamma), but the experiments minimise L(rho, g(Q), t, gamma), where g is a manually implemented transformation that maps the learned trajectory to distances, velocities, or other derived values used by the constraints. This function g is not part of the Isabelle formalisation, and no theorem covers the composed loss or its derivative. The paper should either formalise g and the composition, or explicitly state that only the L component is verified and that the overall loss used in the experiments is outside the formal guarantee.
minor comments (5)
  1. [3.2.1] In the displayed equivalences, 'eval(Not(Not(rho), T, t)' is missing a closing parenthesis and should read 'eval(Not(Not(rho)), T, t)'.
  2. [3.2.2] In the definition of L(Diamond rho, T, t, gamma), 'min_gamma((L(rho, ...' contains an extra opening parenthesis; the formula should be 'min_gamma(L(rho, T, t, gamma), L(Diamond rho, T, t+1, gamma))'.
  3. [4.2.2] There is a typo in 'proceeded empirically by by testing'; one 'by' should be removed.
  4. [4.2.4 / Table 1] Table 1 reports a single loss value per experiment with no error bars, no number of runs, and no seeds; a brief statement on run-to-run variability would make the empirical results more interpretable.
  5. [General] No link to the Isabelle/HOL theory files or to the generated OCaml code is provided; an artifact appendix or repository link would allow independent replay of the machine-checked claims, which is important for a paper whose central contribution is formal verification.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central soundness and derivative theorems are machine-checked consequences relating independently defined eval and L, and no prediction reduces to a fitted input.

full rationale

The paper's central formal claim is that L is sound with respect to eval and that dL is the derivative of L. eval is defined separately as a boolean tensor semantics (Section 3.2.1) and L is defined in Section 3.2.2 as a smooth variant; the soundness theorem is proved in Isabelle/HOL by induction, not assumed. This counts as independent, machine-checked support under the review rules: the cited Isabelle code-generation layer (Haftmann & Bulwahn 2021) is external, and the definitions do not presuppose the target result. The acknowledged floating-point gap (Section 3.3: 'a property proven to be true over the mathematical reals may not be generally true over floating point numbers') limits runtime fidelity but is not circular. The experiments report the same L that was minimized as the constraint metric and do not independently evaluate eval on final traces (Section 4.2.4), which weakens the empirical demonstration, but this is an evaluation weakness rather than a derivation that reduces to its own inputs. No load-bearing self-citation, imported uniqueness theorem, or hidden ansatz was found; self-citations such as Chevallier et al. (2022) are contextual only. Accordingly, no circular step is exhibited.

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

No free parameters are fitted to data in the formal part: the loss L, its derivative dL, and the smoothing functions max_gamma, min_gamma and gaussian_gamma are defined explicitly, and the theorems are machine-checked in Isabelle/HOL. In the experimental part, the smoothing factor gamma=0.005 is chosen by hand after testing a range (0.5 to 0.001), but it is a hyperparameter of the learning setup, not a number fitted to make the central formal claim hold. The DMP constants alpha and beta and the weighting eta=1.0 are also standard or chosen by hand for the demonstrations. No new axioms or invented entities are introduced: the paper uses standard higher-order logic in Isabelle/HOL, standard mathematical definitions of tensors, and standard LTLf semantics from De Giacomo & Vardi. The claim that the code generator is a trusted translation layer is an assumption, but it is a standard assumption of Isabelle code extraction, not an ad hoc axiom of this paper.

assumptions (5)
  • standard math The Isabelle/HOL logic is consistent and the LCF kernel is sound, so theorems proved in Isabelle/HOL are valid in standard higher-order logic.
    The paper relies on Isabelle's small trusted kernel (Section 2.5) as the basis for all confidence in the formal proofs.
  • domain assumption The standard semantics of LTLf over finite traces, as presented by De Giacomo & Vardi (2013), is the reference semantics that tensor-based eval formalises.
    Section 2.3 introduces LTLf informally and cites De Giacomo & Vardi; the formalisation is intended to match this semantics, including the convention that an empty trace evaluates to false.
  • domain assumption Isabelle's code generation translation layer (Haftmann & Bulwahn) preserves the mathematical meaning of the formal definitions in the target language OCaml.
    Section 3.3 explains that generated code retains proven properties via a thin trusted translation layer; this is the standard assumption of all Isabelle code extraction and is acknowledged as a small trusted piece.
  • domain assumption The mapping from mathematical reals in Isabelle to floating point numbers in OCaml preserves the practical validity of the soundness theorem during training.
    Section 3.3 states that properties proven over mathematical reals 'may not be generally true over floating point numbers', explicitly flagging this caveat. The paper mitigates overflow but does not formally verify floating-point behaviour.
  • domain assumption The DMP (Dynamic Movement Primitive) equations from Ijspeert et al. (2013) adequately model the class of trajectories used in the experiments.
    Section 4.2 defines the DMP model and relies on its differentiability with respect to neural network parameters for backpropagation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces." pith.science (2026). https://pith.science/paper/CXEAQTRE

@misc{pith2026250113712,
  author       = {Pith},
  title        = {Pith review of: Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CXEAQTRE}},
  note         = {Machine review of arXiv:2501.13712}
}
read the original abstract

We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf), with formal proofs of correctness carried out in the theorem prover Isabelle/HOL. We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the LTLf constraints, and automatically generating an implementation that integrates with PyTorch. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints. Our approach offers a fully rigorous framework for constrained training, eliminating many of the inherent risks of ad-hoc, manual implementations of logical aspects directly in an "unsafe" programming language such as Python, while retaining efficiency in implementation.

Figures

Figures reproduced from arXiv: 2501.13712 by the authors.

Figure 1
Figure 1. An example trace capturing the x and y coordinates of an agent. From a more formal standpoint, constraints are syntactically represented by LTLf for￾mulae. The smallest constraint possible is an atomic one which extracts relevant mea￾surements ϕn from the trace as real numbers and performs a comparison using them. For example, if we are monitoring the location of a robot in a two dimensional maze, we might be able t… view at source ↗
Figure 2
Figure 2. An example 5×2×4 tensor representing a batch of LTLf traces, highlighting the element indexed by (2,1,0). of ρ (discussed in Section 3.2.1). If we were to include logical negation as a primitive operator, it would mean we could not specify the loss function L using primitive recursion. This would prevent the use of inductive proofs over constraints, as we will discuss further in Section 3.2. Given the above, our tre… view at source ↗
Figure 3
Figure 3. Isabelle-PyTorch neurosymbolic pipeline. [PITH_FULL_IMAGE:figures/full_fig_p020_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Trajectories and velocities for demonstrations with simple trajectories. [PITH_FULL_IMAGE:figures/full_fig_p022_4.png]
Figure 5
Figure 5. Figure 5: Trajectories for the Unconstrained, Avoid, Patrol, Until, Compound and Loop [PITH_FULL_IMAGE:figures/full_fig_p026_5.png]
Figure 6
Figure 6. Figure 6: Example trajectories represented as simple sets of coordinates and speeds, trained [PITH_FULL_IMAGE:figures/full_fig_p028_6.png]
Figure 7
Figure 7. Figure 7: Conjoined double loop constraint using DMPs. The conjoined constraint, al [PITH_FULL_IMAGE:figures/full_fig_p029_7.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. AI Can Learn Scientific Taste

    cs.CL 2026-03 conditional novelty 6.0 of 10

    Reinforcement learning on citation-preference pairs teaches a model to predict which papers will be cited more and to propose ideas that LLM judges rate as likely to be cited more—but "taste" here means citation impact.

Reference graph

Works this paper leans on

43 extracted references · 41 canonical work pages · cited by 1 Pith paper

  1. [1]

    Affeldt, R., Bruni, A., Komendantskaya, E., Ślusarz, N., \ Stark, K. 2024 . Taming differentiable logics with coq formalisation

    work page 2024

  2. [2]

    Badreddine, S., d'Avila Garcez , A., Serafini, L., \ Spranger, M. 2022 . Logic tensor networks \ Artificial Intelligence , 303 , 103649

    work page 2022

  3. [3]

    C., \ Klakow, D

    Bentkamp, A., Blanchette, J. C., \ Klakow, D. 2019 . A formal proof of the expressiveness of deep learning \ Journal of Automated Reasoning , 63 , 347--368

    work page 2019

  4. [4]

    Bulwahn, L. 2012 . Smart testing of functional programs in Isabelle \ In International Conference on Logic for Programming Artificial Intelligence and Reasoning , \ 153--167. Springer

    work page 2012

  5. [5]

    Chevallier, M., Whyte, M., \ Fleuriot, J. D. 2022 . Constrained training of neural networks via theorem proving \ In Short Paper Proceedings of the 4th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis , \ 3311, \ 7--12. CEUR-WS.org

    work page 2022

  6. [6]

    \ \ Blondel, M

    Cuturi, M. \ \ Blondel, M. 2017 . Soft- DTW : a differentiable loss function for time-series \ arXiv preprint arXiv:1703.01541 , 1

    arXiv 2017

  7. [7]

    \ \ Vardi, M

    De Giacomo, G. \ \ Vardi, M. Y. 2013 . Linear temporal logic and linear dynamic logic on finite traces \ In IJCAI'13 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence , \ 854--860. Association for Computing Machinery

    work page 2013

  8. [8]

    Donz \'e , A. 2013 . On signal temporal logic \ In Runtime Verification: 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings 4 , \ 382--383. Springer

    work page 2013

Show all 43 references
  1. [9]

    Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., \ Vechev, M. 2019 . DL2 : Training and querying neural networks with logic \ In International Conference on Machine Learning , \ 1931--1941

    2019

  2. [10]

    Fleuriot, J. D. 2000 . On the mechanization of real analysis in I sabelle/ HOL \ In Aagaard, M. \ \ Harrison, J. , Theorem Proving in Higher Order Logics , \ 145--161. Springer

    2000

  3. [11]

    A., \ Monahan, R

    Flinkow, T., Pearlmutter, B. A., \ Monahan, R. 2024 . Comparing differentiable logics for learning with logical constraints \ arXiv preprint arXiv:2407.03847 , 1

    2024 arXiv

  4. [12]

    Garcez, A. d. \ \ Lamb, L. C. 2023 . Neurosymbolic AI: The 3rd wave \ Artificial Intelligence Review , 56\/ (11), 12387--12406

    2023

  5. [13]

    Gordon, M. J. 1988 . HOL: A proof generating system for higher-order logic \ In VLSI specification, verification and synthesis , \ 73--128. Springer

    1988

  6. [14]

    \ \ Bulwahn, L

    Haftmann, F. \ \ Bulwahn, L. 2021 . Code generation from Isabelle/HOL theories

    2021

  7. [15]

    \ \ Heller, A

    H \"o lzl, J. \ \ Heller, A. 2011 . Three chapters of measure theory in Isabelle/HOL \ In International Conference on Interactive Theorem Proving , \ 135--151. Springer

    2011

  8. [16]

    J., Nakanishi, J., Hoffmann, H., Pastor, P., \ Schaal, S

    Ijspeert, A. J., Nakanishi, J., Hoffmann, H., Pastor, P., \ Schaal, S. 2013 . Dynamical Movement Primitives : Learning Attractor Models for Motor Behaviors \ Neural Computation , 25\/ (2), 328--373

    2013

  9. [17]

    \ \ H \"o lzl, J

    Immler, F. \ \ H \"o lzl, J. 2012 . Numerical analysis of ordinary differential equations in Isabelle/HOL \ In Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings 3 , \ 377--392. Springer

    2012

  10. [18]

    \ \ Ramamoorthy, R

    Innes, C. \ \ Ramamoorthy, R. 2020 . Elaborating on Learned Demonstrations with Temporal Logic Specifications \ In Toussaint, M., Bicchi, A., \ Hermans, T. , Proceedings of Robotics: Science and System XVI

    2020

  11. [19]

    Kingma, D. P. \ \ Ba, J. 2015 . Adam: A method for stochastic optimization \ In Bengio, Y. \ \ LeCun, Y. , 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings

    2015

  12. [20]

    Kolda, T. G. \ \ Bader, B. W. 2009 . Tensor decompositions and applications \ SIAM review , 51\/ (3), 455--500

    2009

  13. [21]

    Krauss, A. 2008 . Isabelle documentation: Defining recursive functions in I sabelle/ HOL

    2008

  14. [22]

    \ \ Popescu, A

    Kun c ar, O. \ \ Popescu, A. 2017 . Safety and conservativity of definitions in HOL and I sabelle/ HOL \ Proceedings of the ACM on Programming Languages , 2\/ (POPL), 1--26

    2017

  15. [23]

    Leung, K., Ar \'e chiga, N., \ Pavone, M. 2023 . Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods \ The International Journal of Robotics Research , 42\/ (6), 356--370

    2023

  16. [24]

    Lim, L.-H. 2013 . Tensors and hypermatrices \ Handbook of linear algebra , 2

    2013

  17. [25]

    Mari \'c , F. 2010 . Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL \ Theoretical Computer Science , 411\/ (50), 4333--4356

    2010

  18. [26]

    Marmsoler, D. 2018 . A framework for interactive verification of architectural design patterns in Isabelle/HOL \ In International Conference on Formal Engineering Methods , \ 251--269. Springer

    2018

  19. [27]

    Mazare, L. 2021 . OCaml-Torch

    2021

  20. [28]

    Milner, R. 1979 . LCF: A way of doing proofs with a machine \ In International Symposium on Mathematical Foundations of Computer Science , \ 146--159. Springer

    1979

  21. [29]

    C., \ Wenzel, M

    Nipkow, T., Paulson, L. C., \ Wenzel, M. 2002 . Isabelle/HOL : a proof assistant for higher-order logic , \ 2283. Springer Science & Business Media

    2002

  22. [30]

    Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., et al. 2019 . PyTorch : An imperative style, high-performance deep learning library \ Advances in neural information processing systems , 32 , 8026--8037

    2019

  23. [31]

    Pitts, A. 1993 . The HOL logic \ In Introduction to HOL : A theorem proving environment for higher order logic , \ 191--232. Cambridge University Press

    1993

  24. [32]

    Pnueli, A. 1977 . The temporal logic of programs \ In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) , \ 46--57

    1977

  25. [33]

    Schaal, S., Peters, J., Nakanishi, J., \ Ijspeert, A. 2005 . Learning movement primitives \ In Robotics research. the eleventh international symposium , \ 561--572. Springer

    2005

  26. [34]

    \ \ d’Avila Garcez, A

    Serafini, L. \ \ d’Avila Garcez, A. S. 2016 . Learning and reasoning with logic tensor networks \ In Conference of the Italian Association for Artificial Intelligence , \ 334--348. Springer

    2016

  27. [35]

    L., \ Stewart, R

    \'S lusarz, N., Komendantskaya, E., Daggitt, M. L., \ Stewart, R. 2022 . Differentiable logics for neural network training and verification \ In International Workshop on Numerical Software Verification , \ 67--77. Springer

    2022

  28. [36]

    L., Stewart, R., \ Stark, K

    \'S lusarz, N., Komendantskaya, E., Daggitt, M. L., Stewart, R., \ Stark, K. 2023 . Logic of differentiable logics: Towards a uniform semantics of dl \ arXiv preprint arXiv:2303.10650 , 1

    2023 arXiv

  29. [37]

    Strecker, M. 2002 . Formal verification of a Java compiler in Isabelle \ In International Conference on Automated Deduction , \ 63--77. Springer

    2002

  30. [38]

    Tverdyshev, S. 2005 . Combination of Isabelle/HOL with automatic tools \ In International Workshop on Frontiers of Combining Systems , \ 302--309. Springer

    2005

  31. [39]

    \ \ Dimarogonas, D

    Varnai, P. \ \ Dimarogonas, D. V. 2020 . On robustness metrics for learning stl tasks \ In 2020 American Control Conference (ACC) , \ 5394--5399. IEEE

    2020

  32. [40]

    Wenzel, M. 1999 . Isar—a generic interpretative approach to readable formal proof documents \ In International Conference on Theorem Proving in Higher Order Logics , \ 167--183. Springer

    1999

  33. [41]

    Xu, J., Zhang, Z., Friedman, T., Liang, Y., \ Broeck, G. 2018 . A semantic loss function for deep learning with symbolic knowledge \ In International conference on machine learning , \ 5502--5511. PMLR

    2018

  34. [42]

    S., \ Shah, M

    Xu, Z., Rawat, Y., Wong, Y., Kankanhalli, M. S., \ Shah, M. 2022 . Don't pour cereal into coffee: Differentiable temporal logic for temporal action segmentation \ Advances in Neural Information Processing Systems , 35 , 14890--14903

    2022

  35. [43]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence '...

Pith tools

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