Analyzing Disease Spread Models using a Theorem Prover

During panedmics, public health professionals often suggest “social distancing”. The goal of social distancing is to slow down the spread of the disease so that public health infrastructure is not overloaded. Unfortunately, social distancing often incures a significant social and economic cost. Businesses must close, and people are isolated from their friends and family. This leads us to an interesting question: how much social distancing is enough?

Answering that question in the context of a real pandemic requires an enormous amoung of effort. In this note, we’ll consider a very simple toy model of a pandemic and use a theorem prover to derive the minimum amount of social distancing necessary to avoid hospital overload.

SIR Models

A Susceptible-Infected-Recovered model is a simplified dynamical system model of disease spread. The basic model is a set of three ordinary differential equations:

s' = -b*s*i,
r' = -k*i,
i' = b*s*i - k*i

where:

• s is the number of individuals in the population who are susceptible to the infection,
• r is the number of individuals in the population who are recovered (we make the assumpption that once an individual is recovered they will not get the disease again; this assumption obviously doesn’t always hold), and
• i is the number of currently infected individuals.

In addition to these variables, the system also has two parameters:

• b is the number of contacts individuals make each day, and
• k is the recover rate (the number of individuals who change from infected (i) to recovered (r) each day.

Our goal is to allow as much contact between inviduals as possible while keeping the infected rate (i) below hospital’s capacity (capacity). In terms of the model, we would like to know: how large we can let b get before i goes above capcity?

This is a reachability property of the SIR model: we would like to know, given some initial conditions on s, i, and r, whether the flow of the SIR differential equations will reach point where i < hospitalCapcity. The KeYmaera X theorem prover was designed to explore exactly these types of reachability properties.

A Quick Introduction to Differential Dynamic Logic and KeYmaera X

In this note, we will use KeYmaera X to discover values of b that keep the value of i below hospitalCapcity. KeYmaera X is a theorem prover for differential dynamic logic. This logic allows you to state and prove reachability properties of differential equations by writing formulas such as:

init -> [{ODEs}]property

where,

• init is a formula of first order logic over real-valued variables (e.g., x>0 & y>0),
• ODEs is a system of differential equations,
• property is also a formula of first order logic over real-valued variables (e.g., i < capacity),

and the meaning of the formula init -> [{ODEs}]property is: starting from a set described by the formula init, any flow of the different equaltions ODEs will stay within the set described by property.

For example, we can state properties such as: x>0 & y>0 -> [{x'=y}]x>0; i.e., if x starts positive and has a positive derivative then the value of x will remain positive throughout the flow of the equation x'=y.

Finding a Safe Contact Rate using KeYmaera X

Here’s a simple SIR model written in KeYmaera X’s input language:

ProgramVariables
R s, r, i, s_0, r_0, i_0, b, k, capacity;
End.
Problem
  (
    i < capacity &
    s=s_0 & 
    r=r_0 & 
    i=i_0 & 
    0 < k & k < 1
  )
  ->
  [
    {
      s' = -b*s*i, 
      r' = k*i, 
      i' = b*s*i-k*i
    }
  ](i<capacity)
End.

Notice that this formula is not true! For example, if:

s_0      = 1,000,000
r_0      = 0
i_0      = 999
capacity = 1000

then obviously i will quickly exceed capcity. However, we can use KeYmaera X to derive necessary and sufficient conditions on the choice of b in terms of any concrete choice of s_0, r_0, and i_0.

Conclusion

Theorem provers are useful for more than just checking the truth of things we already know. They can also help us understand the world.