From the 1 of 5 linked papers with an AI index.
5 papers
Adequate Losses via Quantitative Linear Logic
Matteo Capucci, Robert Atkey, Charles Grellois +2
The paper proposes a family of quantitative linear logics (pQLL) that combine logical specifications with differentiable loss functions for neural components, proving cut‑eliminati…
Data Provenance as Automatic Differentiation
Robert Atkey, Roly Perera
Automatic differentiation (AD) computes the derivative of a program alongside the program itself, as a linear map between tangent spaces, propagated forwards or backwards along an…
Compiling High-Level Neural Network Specifications into VNN-LIB Queries
Matthew L. Daggitt, Wen Kokke, Robert Atkey
The formal verification of traditional software has been revolutionised by verification-orientated languages such as Dafny and F* which enable developers to write high-level specif…
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
Matthew L. Daggitt, Wen Kokke, Robert Atkey +3
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodolog…
A Semantic Proof of Generalised Cut Elimination for Deep Inference
Robert Atkey, Wen Kokke
Multiplicative-Additive System Virtual (MAV) is a logic that extends Multiplicative-Additive Linear Logic with a self-dual non-commutative operator expressing the concept of "befor…