I have recently been thinking about modelling of dynamical systems again - so wanted to revisit some of my old ideas.

A new approach to modelling dynamical systems

A couple of things have changed recently, which is what brings me back to thinking about dynamical systems - particularly the ability to better reason about proofs, and hence the construction of systems and programs - in the style of programs-as-proofs.

I am putting the pieces together, but my general theory is that we can now move to another paradigm for modelling dynamical systems that combines the two previous approaches. So what are these previous approaches and this new paradigm:

Approach 1: Explicitly define system representations

This is way we have been doing it for a long time. We model a dynamical system by writing down the equations that describe it, which we can then simulate. We use our knowledge of the system and general physics to define it. Often this means applying Navier-Stokes equations to fluid systems, or Newton’s laws to mechanical systems. THe downside of this approach is that it is often hard to know what equations to use, and the equations are often complex and difficult to solve.

Approach 2: Implicitly learn system representations

This is the more recent approach, especially accelerated by the availability of large amounts of data and the development of deep learning. In this approach we no longer define the equations that describe the system, but instead train a model to predict the future state of a system based on its current state and the actions taken on it. The idea is that the model will learn the equations that describe the system, but without us having to explicitly define them. This has obvious benefits - in particular, the ability to model complex systems without having to define the equations that describe them.

Approach 3: Learn explicit system representations

With recent developments in large language models, I believe we can now also learn explicit system representations - if we have the right framework for defining and reasoning about dynamical systems.

Why is this an improvement? By implicitly learning the system representations and not having access to the equations, we cannot reason well about the system and it often generalises poorly beyond the data we have. If instead we could learn the equations that describe the system, we could then both reason about the system and predict future states - even in scenarios where we have no data.

An example of the above would be weather forecasting. Traditionally we use explicit models of the atmosphere to model the incredibly complex dynamical system that makes up the atmosphere. We are now more moving towards using transformer based syststems to predict the future state of the atmosphere. But with this third approach we could potentially learn the equations that describe the atmosphere and then use that to apply reasoning about the atmosphere and better predict scenarios that we have no data for.

Abstract Hoare Logic

The origin of my interest in this goes back to my PhD thesis, where I was working on a general approach to modelling and reasoning about systems in a way that would allow for pre- and post-conditions reasoning to be applied to them.

I called it Abstract Hoare Logic - named after the Hoare Logic for proving properties of programs.

The idea generally was that by abstracting away the specifics of a family of systems to the level of categories, we could build theories and practices for reasoning at a higher level of abstraction and then apply that to instantiations of the framework. The reasoning steps was akin to the steps of a proof within traditional Hoare Logic - hence the name - and the canonical instantion of the framework was the category of imperative WHILE programs, as in Hoare Logic.

However, by changing the categorical structure, we could instantiate the framework to other types os systems - in particular, by inverting the categorical structure of WHILE programs to its dual category, we could instantiate the framework to the category of dynamical systems.

I seem to have lost the electronic version of my thesis, but I found some old related articles and slides here and here. Also googling around, I found some recent work on the topic.

LCL - Little Categorical Language

The original work around categorical logic and modelling was still quite abstract and high-level but a few years later, having spent some time working in finance working with large scale dynamical systems, I came up with a more concrete instantiation for dynamical systems that would allow me to both reason and effectively simulate

I named the instantion LCL, Little Categorical Language, and build a number of libraries and tools around it.

LCL could model not just simple dynamical systems, but also complex stochastic systems defined within stochastic calculi, like Ito or Stratonovich. In fact, the underlying calculus of the systems was completely flexible and abstracted awway in the reasoning step.

The interface was a simple but a little clunky and verbose - it was written for Python 2.7 after all! But here is a simple example of how to use it to simulate a simple dynamical system:

# define the governing equations of the system
equation = lng.equation(lng.variable("f"), lng.diff(lng.variable("f"), lng.variable("t")))

# define the dimensions of the system
dimension_t = lcl.dimension("t", 10)

# define the boundary conditions of the system
boundary_t = lcl.boundary("f", dimension_t, 1.0)

# approximate the system - this creates a approximate solution
approximation = lcl.approximate(equation, boundary=boundary_t, dimensions=dimension_t)

# define the initial conditions of the system and the type of the variables
point = lcl.point(dimension=dimension_t, type=lcl.REAL, value=1.0)

# simulate the system
result = lcl.simulate(approximation, point)

You can find more examples and details of the language in a few presentations I did at the time at ERCIM 2012 and EuroScipy 2013. The EuroScipy poster is probably the best I think.

Reasoning about systems

The reasoning part of LCL was particularly interesting to me, since it could in theory allow for constructions of explicit systems based on a data set of observed dynamics. For example, if we could observe a system in action we could reason our way to an explicit representation for the system - which would allow us to then simulate it under other conditions and build new systems from it.

The reasoning part could also be used to rewrite existing explicit representations into simpler forms - including closed form solutions. In fact, there is a specfific way within AHL and LCL to define what closed versus open form means, namely the a system which proof represenation include a loop-construct. Akin to a cut-free proof in the sequent calculus - see Wiki’s article on Cut Elimination for more..

However, as it all came down to proof construction, it was incredibly difficult to automate beyond simple cases. This is the bit that I am hopefull can now be solved with the right reasoning tools, ie large language models.

The beauty of LCL and dynamicals systems is that it presents an oracle of truth - we can test any system construction that the proof agent has come up with and provide feedback on the error rates etc. This fits particular well with the new style of agentic reasoning that we are starting to see.

When I originally built reasoning systems for LCL I used more traditional search methods on the proof space, like differential evolution. But these methods rely on large scale experimentation - trying out large amounts of combinations to evolve to the next state, as opposed to agentic reasoning, which is much more efficient - only trying out the most promising paths at a time. Because of the cost of simulating large scale systems, this made my previous attempts infeasible.

This is just another example of the type of deep and complex reasoning tasks that I know think we can solve with agentic reasoning. Agentic reasoning isn’t in itself the solution but it might be the missing piece for a lot of problems where we have already made significant progress.