Fall 2024

Mechanistic interpretability of neural networks aims at the discovery of interpretable subgroups of model weights, or circuits. Well-known examples include both low-level and high-level features in images. We will review recent progress in the automated discovery of circuits in LLMs. Our aim is to then explore potential applications of this technology to mathematics. For example, can theorems and lemmas from Lean's Mathlib be transcribed into RASP (a programming language mapped to components of a Transformer), enabling automatic circuit discovery for these building blocks? Could modularity of circuits lead to proofs represented entirely within Transformer activations, increasing LLM accuracy in proof generation? What implications would this have for automated formalization and automated theorem building?

colab.research.google.com/drive/19ecdH70YduhGJulQ-1uiXuivAmN672Pq?usp=sharing#scrollTo=VUgn_2xCUFbT 

One of the main features of non-classical logics is the fact that their algebraic semantics may contain more than just two truth values (true/false). And very often, these truth values are ordered in one way or another and the fundamental operations respect or reverse this order. Sometimes, this order is definable in terms of the algebraic operations, and thus the study of such partially ordered algebras (po-algebras) falls into the realm of Universal Algebra. But, when the order is not term-definable, the tools and techniques of Universal Algebra may prove insufficient. For that reason, D. Pigozzi initiated the study of a genuine theory of po-algebras. He proved several results that show that the universal theory of po-algebras runs in parallel to classical Universal Algebra. In this talk, we continue this development, showing that Jónsson’s Lemma—one of the most celebrated results of Universal Algebra—also holds, mutatis mutandis, for partially-ordered varieties.

In this talk, I will characterize the polyadic algebra arising from algebraic implicative predicate logic, and prove a functional representation theorem. Then the connection between non-classical polyadic algebra and cylindric algebra will be discussed.

Reasoning about information, its potential incompleteness, uncertainty, and contradictoriness need to be dealt with adequately. To reason with conflicting information, positive and negative support---evidence in favour and evidence against---a statement can be quantified separately in the semantics. This two-dimensionality gives rise to logics interpreted over twist-product algebras or bi-lattices, the well known Belnap-Dunn logic of First Degree Entailment being a prominent example. Belnap-Dunn logic with its bilateral semantics can in turn be taken as a base logic for defining various uncertainty measures on de Morgan algebras, e.g. Belnapian (non-standard) probabilities or belief functions.

In this talk, we first show how to expand Łukasiewicz or Gödel many-valued logics with a de Morgan negation and interpret the resulting logics over twist-product algebras based on the [0,1] real interval, which can account for the two-dimensionality of positive and negative component of (the degree of) belief or likelihood based on potentially contradictory information, quantified by an uncertainty measure. The resulting logics inherit both (finite) standard completeness, decidability and complexity properties from the original logic in question, and allow for an efficient reasoning using the constraint tableaux calculi formalism. Second, we utilise the apparatus of two-layered modal logics: Many-valued logics with a two-dimensional semantics mentioned above are used on the outer layer to reason about Belnapian probability measure or a belief function, building on Belnap-Dunn logic as an inner logic of the underlying evidence.

- Reasoning with belief functions over Belnap--Dunn logic, MB, S. Frittella, D. Kozhemiachenko, O. Majer, and S. Nazari, Annals of Pure and Applied Logic, 2023. https://arxiv.org/abs/2203.01060 

- Two-layered logics for probabilities and belief functions over Belnap--Dunn logic, MB, S. Frittella, D. Kozhemiachenko, O. Majer, submitted. https://arxiv.org/abs/2402.12953

In this talk I explain the main ideas of our project on non-standard probabilities based on paraconsistent logics. I will focus on discussing the differences of approach depending on different logic systems, and finally I suggest some examples of applications.

References

[1] A. Rodrigues and J. Bueno-Soler and W. Carnielli. Measuring evidence: a probabilistic approach to an extension of Belnap-Dunn logic. Synthese 2021. https://doi.org/10.1007/s11229-020-02571-w 

[2] W. Carnielli and J. Bueno-Soler. Paraconsistent probabilities, their significance and their uses. In C. Caleiro and F. Dionisio and P. Gouveia and P. Mateus and J. Rasga (eds). Essays in Honour of Amilcar Sernadas. College Publications, 2017.

[3] J. Bueno-Soler and W. Carnielli. Paraconsistent Probabilities: Consistency, Contradictions and Bayes' Theorem. Entropy, 2016. https://doi.org/10.3390/e18090325 

Universal algebra is traditionally positioned within set theory and first-order logic, although many of the main results are formulated in higher-order logic and some results have been extended and generalized to category theory in the form of Lawvere theories, monads and (categorical formulations of) algebraic theories. Recent efforts to formalize mathematics in interactive theorem prover libraries are mostly based on (various) dependent type theories, so it is natural to compare how the mathematical libraries of Agda, Lean, Rocq and Rzk aim to capture the unifying insights of universal algebra. In this informal talk I will survey some of the ideas and design decisions that are part of this landscape.