Gimle goes back more than 20 years to the time of my PhD, since then the core ideas have always been bouncing around in my head and although I made progress a few times there was always a few pieces missing for it to work. However, I think with recent developments in LLMs, mechanical reasoning and the unbelievable increase in compute power, now is the time for it all to come together.
To clarify things a bit in my head I wrote down the backstory and thought it might be useful to share. I apologise in advance for the length of this post and its rambling nature 😊
Also, if you don't know what GImle is have a look at the What is Gimle? page.
The Dream
The motivation behind Gimle is the idea that there is a better way to model dynamical systems by combining the explicit nature of traditional formal methods with learned, statistical methods.
The outcome of this could be fundamental to the world of engineering, finance and most sciences - being able to simulate systems at scale fitted to real world data while simultaneously being able to explicitly understand and manipulate the underlying dynamics could significantly improve work with dynamical systems as well as advance theoretical knowledge about the foundations of the world we live in.
The Beginning
During my PhD under Ursula Martin I was working on generalising and unifying formal reasoning about dynamical systems and computer programs. The aim being to formally reason about physical systems in similar ways to how we can reason about programs with formal systems, like Hoare Logic, Separation Logic, Weakest Precondition Calculus and the likes.
As part of this work I discovered the world of categories, and in particular traced monoidal categories (TMCs). The resulting system was a new way of reasoning about generalised computational systems using TMCs and proof systems similar to Hoare Logic. We called it Abstract Hoare Logic (AHL) and its achievement was to generalise traditional pre-post condition reasoning to more general systems, including dynamical systems.
The bulk of this work was quite theoretical and mainly dealt with the theory of computation at a foundational level but towards the end of my PhD I came across Rutten's work on co-induction and stream calculus. In some of Rutten and his group's work, stream calculus was used to represent functional forms that could be expressed as infinite streams of coefficients. From my perspective, being a category theorist, stream calculus was just another cartesian TMC, which meant that I could apply AHL to it to reason about systems defined by Taylor expansions. This was the first time I started to think about how this type of reasoning system could be applied to dynamical systems - how the category theoretical proof system could be a representation of a physical system for which a stream calculus-style semantics could provide the simulation engine.
This beautifully converged with another obsession of mine at the time: to solve the Navier Stokes millienium problem. I had been playing around with this for a few years at the time and it was incredibly exciting to see the convergence of the two things I was so obsessed about: the idea that there was a way to reason about Navier-Stokes from a proof-theoretic angle. Of course, I never managed to solve Navier-Stokes but maybe, just maybe, Gimle can help me with that one day 😊
As a sidenote, it was during this time that I (quite late in life) discovered Asimov and, in particular, The Foundation series. And like many other young scientists, I found the psychohistory of Hari Seldon incredibly motivating and a perfect complement to this dream of being able to reason about the physical world through formal methods. I just love that book, it is a great motivator for any young or aspiring scientist working on something foundational and a little of the beaten path - it really should be school curriculum 😄
SDEs and Proofs-as-Systems
After finishing my PhD I entered investment banking to work in the field of financial mathematics - in this legendary place. Here I encountered dynamical systems in a new shape: as tools to model financial markets and instruments with through the use of stochastic differential equations (SDEs). This made me return to AHL, thinking that I could use the same approach to model and simulate systems defined by SDEs. Using an approach inspired by Rutten's stream calculus I was able to build a framework for reasoning about and simulating systems defined by SDEs.
This reinforced the idea that TMC based frameworks and their associated proof systems could be viewed both as computational engines to approximate the solutions of equational systems as well as a proof system to reduce or solve, in the closed form sense, equational systems. Or to say it in another way, that there was a way to bridge the strict, formal definition and reasoning about systems, with the approximate, numerical, simulation of systems. They were really just two lenses through views to view the same category theoretical construction. One would be the syntax and the other lens the semantics.
Another insight from this was that most of the reasoning done using such an approach could be done completely agnostic to the underlying calculus(!) - that is, that the reasoning about these systems could happen at a higher, more abstract, proof-theoretical level, disconnected from the specifics of the underlying calculi, be it Riemannian, Stratonovich, Ito etc. Instead the specific calculus used would only need to be decided at the point of simulation, allowing you to then easily swap and even mix types of calculi.
These two points are to me, perhaps in a simplistic form, fundamental insights about the nature of computation and its role in the physical world.
This felt very much like something in the spirit of Curry-Howard and the proofs-as-programs school of thought, ie that there is an isomorphism between the proof-theoretic definition of a dynamical system and a numerical function to simulate and approximate the evolution of the system. In the proof theoretic setting we are decoupled from any specific calculus and can reason at a high-level about the system, finding closed form solutions, equivalent forms, proving properties etc, and in the numerical simulation setting we are talking about a specific calculus and look at simulated, approximative reaslisations of a system.
As part of this work I developed a small C library with a Python extension for running simulations and to do simple reasoning - but the reasonings step were never that successful. I struggled to build a reasoning system that would be able to perform the type of non-trivial rewrites that a real-world example would need to be able to perform non-trivial reasoning.
I think there is another fundamental principle at work here: the difference between trivial proofs, like what you can solve with a typical mechanical proof solver or what you see in a calculus textbook, and non-trivial proofs, which require something different, something creative or what you might call non-linear reasoning. Most parts of these non-trivial proofs are actually trivial except for a few incredibly creative and non-linear step, without which you cannot prove anything non-trivial.
I often think of this in the context of guessing a loop invariant for a program - you can automatically rewrite your program logic but to find a loop invariant you need to almost of out of thin air invent something. In fact to perform non-trivial rewrites of a dynamical system, and especially to find closed form solutions, you also need to find loop invariants - in this case for differential operator feedback in order to remove it and progress the reasoning.
It is also interesting to think of this in the context of Cut and Cut Elimination - cuts are like loop, or for dynamical systems differntial operator feedback, which in turn are traces in a TMC. Now, Gentzen's cut-elimination theorem say that we can always remove cuts to obtain equivalent cut-free proofs, which in the context of TMCs means we can remove traces to produce equivalent, trace-free derivations. Which, then in the context of dynamical systems, means that we can always find a closed form solution! However, we have no guarantee on the length of such a proof, and hence even though it exists it can be unfeasible to compute.
Anyway, back to the story... so I had the basics of how to model physical systems but I couldn't get the reasoning to work well and I was also struggling with the computational complexity of modelling and experimentation, given the compute I had access to at the time.
I knew there had to be a learned element to the reasoning, a way for the system to learn from previous reasoning traces and to use that to explore a new part of the solution space in a non-random, non-greedy way. This clearly would have to be some form of machine learning, but nothing at the time really worked that well for this sort of task. In the end, I ended up doing a few presentations on it (which seem to have disappeared into the ether since then) and then moved on to other things.
Cylindrical Algebraic Decomposition
This part of the story is less important but still interesting.... So, I put my quest to one side and continued working my way around the finance scene and then I re-encountered Cylindrical Algebraic Decomposition (CAD). I was working on a project that involved some sort of guessing of polynomial solutions and I was looking at CAD, which I knew from my PhD days, as a way to perhaps do it.
That didn't work out but I realised that CAD was another way to reason about properties of dynamical systems in an approximate manner using the semantics of streams. Using CAD I could build proofs, using the proof theoretical definition of a dynamical system, of bounding properties of the evolution of a dynamical systems, so I could now reason about properties, like safety or reachability, of a dynamical system. The only downside was that CAD is an incredible computationally expensive operation and in practice, at the time, was really feasible.
However, this brought me back to the world of dynamical systems and the quest to find a way to reason about them in a more principled way.
Working on LLMs and KGs
In 2016 I left investment banking to start my first little startup, Octavia. One of the things that we pursued at Octavia was to automate the analysis of job specs and CVs to assist recruiters in hiring and screening candidates. This was before the days of LLMs, so instead we pioneered a new approach to Latent Dirichlet Allocation (LDA) to extract the key topics from job specs and CVs - here is a talk I gave on it. It was quite cool, I think one of the better implementations of LDA, but it was still to fickly and it never really worked well enough to make a real impact for recruiters - but it did bring me into the world of NLP and soon after LLMs.
Closing down Octavia in 2018 I joined a scaleup called Streetbees to build their AI/ML team. In November that year I took my fledgling team of 3 researchers to EMNLP in Brussels, which in retrospect feels like ground zero for a lot of what happened next in NLP, LLMs and AI.
At the time we were very excited about RNN-based LLMs, like Elmo and UmlFiT, that were beating the previous state-of-the-art bag-of-words models, like word2vec and Glove. We had read the now classic 2017 paper "Attention is all you need", and thought it was cool, but were still all in on stacking up bi-directional RNNs and didn't think too much of transformers. That really changed at EMNLP - Google had just released their BERT paper and during EMNLP Huggingface implemented the first open source implementation of BERT, which later turned into their now famous transformers library.
Coming back from EMNLP we went all in on transformers - we figured out a way to use a BERT-like architecture to learn the structure of sparse knowledge graphs and predict out-of-sample nodes and relations in such graphs. The idea was to view the graph structure as the definition of a language syntax. We could then sample this language by performing random walk through the graph. These random walks could then be viewed as sample sentences in a graph-specific language, which we could then train a BERT-like model on. Token prediction in this context then became a way to predict the missing nodes and relations in a graph.
Besides a paper at EurNLP, the idea didn't really work that well, and we moved on to other things, but it was a great illustration of the power of reformulating a problem into a language modelling task, perfect for a transformer-based approach. Especially when you have a well-defined grammar and a generating function, which then allows you to generate synthetic data at scale for training.
Enter Agents
After another scaleup data science job, I decided in 2022 to join forces with my friend Ryan to start a new company called Infer. Infer was a more traditional machine learning startup, building models and tools for analysts to use in their day-to-day work.
We eventually got acquired by Frisbii/PSG but during the last months before the acquistion we started working on a number of quite exciting agent projects, which pushed us to build a new style of agentic orchestration framework, which I wrote a series of articles on.
Although not much came out of it, in terms of commercial use, we learned an immense amount about the capabilities and limitations of LLM-based agents for longer, more creative reasoning tasks. We also built a number of novel techniques and tools for defining and orchestrating agents. In particular, we can up with, what I think is a novel way, to model agentic flows via a type state machines, which allowed us to easily enable branching, roll-outs, dynamic context rendering and tool selections and asynchronous (and synchronous) multi-agent reasoning.
After Infer was rolled into our acquirer, I took these ideas, and a bunch of new ones, and started working on them in my spare-time. It was during this that it hit me that what I was building might just be the missing piece when it came to reasoning about dynamical systems. That this framework would allow us to autonomously use and reason about the range of tools that I had previously created for simulating, modelling and reasoning about physical systems.
In this setting we can view proofs as dynamial systems, simulations as agentic tools and agents as the reasoning layer gluing it all together.
Which brings us all the way back to Gimle 😃
To learn more about Gimle itself head over to What is Gimle?.