Glaive Research
A non-profit research group applying category theory to AI verification. Our tools are dependently typed theories, theorem provers, and whiteboards.
A non-profit research group applying category theory to AI verification. Our tools are dependently typed theories, theorem provers, and whiteboards.
Glaive is a research group building software infrastructure based on the theory of containers. We pursue three research programmes in this area: typed tactics for interactive theorem proving, structured architectures for machine learning, and Polylang, a programming language we're designing from the ground up. This area of research sits at the intersection of category theory, dependent type theory and programming languages, and has proven to be both remarkably expressive in encoding structure across all of these fields, and concrete enough to actually build software with.
Theorem proving with tactics can be augmented by giving types to goal states, but those types aren't the ones we find in programming as we know it today. A tactic records two pieces of information, first how to convert a goal into a subgoal, and secondly, how to convert proofs from subgoals into proofs of the original goal. The goal/proof pairing acts as the types describing the tactic, and such types are containers. The Typed Tactics project aims to bring this insight into live by incorporating this knowledge into the lean editor experience.
Learn more:Neural networks operate on data with rich algebraic structure, but the programming languages and architectures of mainstream deep learning give researchers no reliable way to reason about that structure, nor to make networks reliably generate it. We are developing architectures based on the theory of containers, expressive enough to recover existing architectures as special cases and principled enough to suggest new ones.
Learn more:The technology underpinning all our work is the category of container and their morphisms as dependent lenses. Because of that, we end up writing a lot of code that represents lenses and containers, but we cannot manipulate them directly. Polylang is our attempt at creating a truly novel programming experience where the unit of computation is the lens and the information they manipulate are containers.
Learn more:Our research is guided by software. We do foundational work where it is needed, but the discipline of having to ship something keeps the theory honest. Everything we produce is open source, and we publish in venues that don't sit behind paywalls.
We think great people do great work when they are freed from mundane constraints and placed in an intellectually stimulating environment. We offer compensation comparable to senior academic positions and a high degree of flexibility in how you work — you are the best judge of your own life, and we are here to support your best work.
If you have an idea and a grant you would like to apply for with Glaive, get in
touch at contact@*website domain*. We strive to provide a welcoming environment to all, and
especially to groups underrepresented in academia.
