![[Berkeley Seminar] Shaowei Lin | Safety by Shared Synthesis @ToposInstitute](https://i.ytimg.com/vi/N1qZhOU5OWo/maxresdefault.jpg)
Uploaded October 2024 | Updated September 2026, 2 weeks ago
Title: Safety by Shared Synthesis
Abstract: Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the foreseeable future. Deploying formal verification (FV) across critical cyber physical systems would dramatically improve safety and security, but has historically been too costly to use outside the simplest or most critical subsystems. AI could allow widespread use of FV in years not decades, shifting cyber risks strongly in favor of defense. In this talk, I will outline our report with Atlas Computing on AI-enabled tools for scaling formal verification (atlascomputing.org/ai-assisted-fv-toolchain.pdf). I will also discuss some lessons that I learnt along the way, especially about shared synthesis - the collaborative construction of formal specifications, implementations and proofs.
https://topos.site/events/berkeley-seminar/
Title: Safety by Shared Synthesis
Abstract: Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the foreseeable future. Deploying formal verification (FV) across critical cyber physical systems would dramatically improve safety and security, but has historically been too costly to use outside the simplest or most critical subsystems. AI could allow widespread use of FV in years not decades, shifting cyber risks strongly in favor of defense. In this talk, I will outline our report with Atlas Computing on AI-enabled tools for scaling formal verification (atlascomputing.org/ai-assisted-fv-toolchain.pdf). I will also discuss some lessons that I learnt along the way, especially about shared synthesis - the collaborative construction of formal specifications, implementations and proofs.
https://topos.site/events/berkeley-seminar/
![[Berkeley Seminar] Shaowei Lin | Safety by Shared Synthesis](https://i.ytimg.com/vi/N1qZhOU5OWo/mqdefault.jpg "[Berkeley Seminar] Shaowei Lin | Safety by Shared Synthesis
Title: Safety by Shared Synthesis
Abstract: Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the foreseeable future. Deploying formal verification (FV) across critical cyber physical systems would dramatically improve safety and security, but has historically been too costly to use outside the simplest or most critical subsystems. AI could allow widespread use of FV in years not decades, shifting cyber risks strongly in favor of defense. In this talk, I will outline our report with Atlas Computing on AI-enabled tools for scaling formal verification (https://atlascomputing.org/ai-assisted-fv-toolchain.pdf). I will also discuss some lessons that I learnt along the way, especially about shared synthesis - the collaborative construction of formal specifications, implementations and proofs.
https://topos.site/events/berkeley-seminar/")
![[Oxford Seminar] David Jaz Myers | Preservation of 2-algebraic structure by pseudo-functors](https://i.ytimg.com/vi/NIhGTjTPnlY/mqdefault.jpg "[Oxford Seminar] David Jaz Myers | Preservation of 2-algebraic structure by pseudo-functors
Oxford Seminar, 31st of January 2025
If universal algebra is the study of sets equipped with the structure of some operations satisfying universally quantified equations, then 2-algebra is the study of *categories* equipped with the structure of some operations, some natural transformations between these operations, and some equations between these. Examples of 2-algebras include symmetric monoidal categories and categories with finite products. Just as the functorial semantics (due to Lawvere) for algebra lets us interpret algebraic theories in categories other than sets (so long as they have finite products), the functorial semantics for 2-algebra (due to Power, Lack, and others) lets us interpret 2-algebraic structure in 2-categories other than Cat. For example, instead of symmetric monoidal categories, we can consider symmetric monoidal double categories. Any strict 2-functor that preserves finite products will push forward 2-algebraic structure. But 2-functors are often only functorial up to coherent isomorphism. What 2-algebraic structure do such cartesian pseudo-functors preserve? In this talk, well ask the question and put forward an answer: so long as the 2-algebraic theory is *flexible*, in the sense that it only asks for equations between transformations and not between operations, then it will be preserved by cartesian pseudo-functors.")
![[Oxford Seminar] Mirco Giacobbe | Neural certificates](https://i.ytimg.com/vi/O9T1zHj1cAA/mqdefault.jpg "[Oxford Seminar] Mirco Giacobbe | Neural certificates
Oxford Seminar, 13th of March 2025
Model checking aims to derive rigorous proofs for the correctness of
systems and has traditionally relied on symbolic reasoning methods. In
this talk, I will argue that model checking can also be effectively
addressed using machine learning too. I will present a realm of
approaches for formal verification that leverage neural networks to
represent correctness certificates of systems, known as neural
certificates. This approach trains certificates from synthetic
executions of the system and then validates them using symbolic
reasoning techniques. Building upon the observation that checking a
correctness certificate is much simpler than finding one, and that
neural networks are an appropriate representation for such
certificates, this results in a machine learning approach to model
checking that is entirely unsupervised, formally sound, and practically
effective. I will demonstrate the principles and experimental results
of this approach in safety assurance of software, probabilistic
systems, and control.
About the speaker:
Mirco Giacobbe is an Associate Professor at the University of Birmingham. He previously held research positions at the University of Oxford and Fondazione Bruno Kessler, and obtained his PhD at the Institute and Science and Technology Austria. His research interests lie between formal methods and artificial intelligence, where he develops automatic techniques to assure that algorithmic systems are safe and trustworthy.")
![[DOTS Lectures] 14. Applying the representability theorem: examples of compositional behaviours](https://i.ytimg.com/vi/RNwCljKiP24/mqdefault.jpg "[DOTS Lectures] 14. Applying the representability theorem: examples of compositional behaviours
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.
Some material from these lectures can be found in Davids book on categorical systems theory:
https://www.davidjaz.com/Papers/DynamicalBook.pdf")
![[Berkeley Seminar] CB Aberle: All Concepts are Essentially Algebraic](https://i.ytimg.com/vi/RmiTOa4b0bA/mqdefault.jpg "[Berkeley Seminar] CB Aberle: All Concepts are Essentially Algebraic
Title: All Concepts are Essentially Algebraic
Abstract: Lawveres categorical formulation of algebraic theories enables one to study some of the most common structures found in mathematics – e.g. groups, rings, etc. – at a high level of precision and generality. However, many significant mathematical concepts, including categories, topological spaces, etc., turn out not to be algebraic, in this sense. Notably, the very framework used by Lawvere to describe algebraic theories and their models – categories with finite products and product-preserving functors between them – cannot be described as an algebraic theory, and so it seems that algebra alone cannot encompass the whole of mathematics (nor even itself). There is, however, a deeper sense in which all of mathematics is essentially algebraic. What is needed to reveal this fact is to adapt the classical notion of algebraic theories, which are fundamentally simply typed, to an appropriate notion of dependently typed algebraic theories. At this level of generality, one is capable of defining not only individual mathematical structures, but structures that themselves encompass whole universes of mathematics, including topoi, models of type theory, etc. In particular, the theory of dependently-typed algebraic theories is itself describable as a dependently-typed algebraic theory. This fact has many profound consequences, of which I shall highlight just one: using the framework of dependently-typed algebraic theories, one can construct a type theory whose types themselves correspond to type theories, with functions between these types corresponding to translations between the corresponding type theories.
https://topos.site/events/berkeley-seminar/")
![[Berkeley Seminar] David Espinosa: Monad translations compose](https://i.ytimg.com/vi/Snvwc4JVIYc/mqdefault.jpg "[Berkeley Seminar] David Espinosa: Monad translations compose
Title: Monad Translations Compose
Abstract: Many people have observed that monad translations compose. We give this idea a try using the ML module system and see what mileage we can get out of it.
https://topos.site/events/berkeley-seminar/")
