PyCon Israel 2022

Formal verification is a subfield in mathematics/computing that provides methods to specify [1] and formally prove the correctness [2] of algorithms and systems given an environment and described using variables, transition functions, etc.

The ability to check a code, whether it enters a state that is not safe using the information in the system is a great advantage. But unfortunately, the main model checkers (which are automatic tools implementing formal verification algorithms) are not very user-friendly. They require writing a text file, which can be very long for large-scale problems, and multiple steps to compile and run, also their UI isn’t always very accessible.

Utilizing model checkers such as NuSMV [3] can become easier by using python. By writing a code that generates the text file for us and activating the NuSMV as a subprocess, we can get the NuSMV results and by using python disassemble the answer and use it in our code accordingly.

Moreover, if we change the problem parameters or the scale of the problem changes between runs, we need to change the file for the NuSMV accordingly, which makes the transition between runs much more complicated. By using python we can make this process much easier and more modular, we can use the information on our code to write the file and also run it.

To demonstrate the idea, we will focus on reinforcement learning (which is a subfield of machine learning). We trained an agent to play frozen lake - a game in which the player needs to reach from one point to another on a board without falling into certain squares which are water holes. We use Q-learning [4] (which is a reinforcement learning algorithm) for the agent which is trained until the decisions table converged by a change of a bound - epsilon or less. We aim to find a way to improve the learning process using Formal verification and specifically NuSMV.

We used NuSMV as an expert of reinforcement learning, the NuSMV checks if the problem we created is solvable before we run the agent, and also during the training process, we used it as an expert that helps the agent learn and make sure it can find an optimal route to the goal.

Before using it as an expert that gives the agent the solution, we used formal verification and python together. For example, some problems require parameters tunings and so we used the NuSMV to check if the epsilon to convergence is good enough to reach the optimal solution, which has the potential to save time because we might be able to take a much larger epsilon.

Furthermore, NuSMV can tell us if the agent during the training process has enough information to reach the solution or if it needs more training. These principles are beneficial to other RL problems.

To conclude, formal verification can be helpful in many problems but using it may be hard for large-scale or complicated problems, so python is a powerful tool that can help us make the process easier and manageable and allow future integration with new problems and tools.

[1] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992).
[2] Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (Eds.): Handbook of model checking (Vol. 10). Cham: Springer (2018).
[3] Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: a new symbolic model checker. Int. J. Softw. Tools Technol. Transfer 2(4), 410–425 (2000).
[4] Watkins, C. J., & Dayan, P.: Q-learning. Machine learning, 8(3), 279-292 (1992).