Formal Verification of Discrete Active Inference Systems in PRISM

Hello and welcome everyone. It's July 15th, 2023. We're here in Active Inference Model Stream number 9.1 with Aspen Paul. Today we're going to have a presentation and a discussion on efficient computation in Active Inference. So if you're watching along live, please feel free to add comments or questions in the chat. Otherwise, Aspen, thanks so much for joining today. Really looking forward to your talk. Thank you, Daniel. Thank you so much. So as mentioned, today I'm here to talk about efficient computation in Active Inference and yeah, let's get started. So we're all familiar with this idea of the free energy principle, which is also known as active inference, right? So the central concept is that an agent minimizes entropy of its observation. To maintain homeostasis or survive in its environment. And here the entropy is defined in the information theoretic sense, right? So if an observation is highly probabilistic, that is less entropic or less surprising because it was high probability and we were expecting it. And that's the idea. Then that's the base that we build this framework of active inference on. And this idea of Markov blanket, it gives us a systematic way of surprising or systematic way of separating an agent from its environment and model purposeful behavior, right? So let's focus on this idea of minimizing entropy. So how does an agent minimize entropy or know which observation is highly probabilistic and vice versa? So that is by maintaining a generative model. And the generative model is basically a toy model of the environment, which the agent builds in its brain. And that is built using only the observation that it get from the environment. So it has no access to the real states or the hidden states of the environment. It's building the toy model. And given this toy model, it has scope or ability to compute the probability of an observation and hence try to minimize the entropy, right? So that's the idea, but it has a problem of, um, cause of dimension dimensionality, like given a generative model, it may not be possible always, uh, to calculate or marginalize the probability of observations out of it, because the state space can quickly become intractable. But the idea is that you define an upper bound on the surprise using Jensen's inequality. And you may also define a new term called Q, which is the hidden, um, belief or the belief about the hidden states. And this Q is going to be the focus of decision-making, right? So if you have a noisy Q and you have no idea what's in the environment, then you can't make or hope to make decisions to control that environment. And it is this belief about the hidden states that you use and that becomes useful to take decisions. And this whole quantity is of course called the free energy and the variation free energy, uh, F can be interpreted in multiple ways. So the first or the most common is the machine learning way of how it is, um, trying to minimize the complexity of the model, uh, at the same time trying to maximize the accuracy of it. So that's the machine learning interpretation of minimizing various free energy. You may also try to, um, interpret free energy in the physics term where you at the same time, try to minimize the energy of your model, um, but at the same time trying to maximize the entropy, but the focus of today, uh, or decision-making is always on this belief that you have, uh, after you do the perception in active inference. So how do you do vanilla decision-making or what is the most discussed idea of decision-making and classical active inference? Uh, so if you, uh, are in an environment, uh, and if you're an agent who's trying to make decisions, then you have a, uh, space of available actions, right? So in this toy model, you have three available actions, uh, run, jump, or stay, uh, and given these actions, you can hope to define a policy by small pie, which is a sequence of actions in time, uh, and capital T is the time horizon of planning…