Reference. Quantifiers for Differentiable Logics in Rocq (Extended Abstract)
Cite
Cites 25 works (1 here)
With notes (1)
On Quantifiers for Quantitative Reasoning capucci-2024-on
We explore a kind of first-order predicate logic with intended semantics in the reals. Compared to other approaches in the literature, we work predominantly in the multiplicative reals , showing they support three generations of connectives, that we call non-linear, linear additive, and linear multiplicative. Means and harmonic means emerge as natural candidates for bounded existential and universal quantifiers, and in fact we see they behave as expected in relation to the other logical connectives. We explain this fact through the well-known fact that min/max and arithmetic mean/harmonic mean sit at opposite ends of a spectrum, that of p-means. We give syntax and semantics for this quantitative predicate logic, and as example applications, we show how softmax is the quantitative semantics of argmax, and Rényi entropy/Hill numbers are additive/multiplicative semantics of the same formula. Indeed, the additive reals also fit into the story by exploiting the Napierian duality , which highlights a formal distinction between ‘additive’ and ‘multiplicative’ quantities. Finally, we describe two attempts at a categorical semantics via enriched hyperdoctrines. We discuss why hyperdoctrines are in fact probably inadequate for this kind of logic.
External (24)
- Taming differentiable logics with Coq formalisation (2024)
- Programme thesis: Safeguarded AI (V1) (2024)
- Comparing Differentiable Logics for Learning with Logical Constraints (2024)
- Quantitative predicate logic as a foundation for verified ML (ARIA grant) (2024)
- Polynomial Lawvere logic (2024)
- Vehicle: bridging the embedding gap in the verification of neuro-symbolic programs (2024)
- Towards guaranteed safe AI: a framework for ensuring robust and reliable AI systems (2024)
- Propositional Logics for the Lawvere Quantale (2023)
- The Vehicle Tutorial: Neural Network Verification with Vehicle (2023)
- Calculus and optimization (2023)
- Logic of differentiable logics: towards a uniform semantics of DL (2023)
- Neural Network Robustness as a Verification Property: A Principled Case Study (2021)
- On Robustness Metrics for Learning STL Tasks (2020)
- DL2: training and querying neural networks with logic (2019)
- Analytic inequalities (Kazarinoff) (2014)
- Handbook of mathematical fuzzy logic, volume 1 (2011)
- Robust and Non-robust Models in Statistics (2009)
- Proof Theory for Fuzzy Logics (2008)
- Residuated lattices: an algebraic glimpse at substructural logics (2007)
- Mathematical components library (2007)
- First-order Gödel logics (2006)
- New classes of Lp-spaces (2006)
- Metric spaces, generalized logic, and closed categories (1973)
- Analytic Inequalities (1970)