Error Recognition and Formal Verification of Reinforcement-Based Learning

Congratulations, Or Reginiano and Eliya Bronshtein, fourth-year students at the computer engineering track, whose final project — Error Recognition and Formal Verification of Reinforcement-Based Learning — was accepted as a lecture at this year’s PyCon. The conference will be held at the Wohl Center at Bar Ilan University on June 28–29, 2022, and will cover innovations in Python programming language.

“Formal verification is about proving the correctness of algorithms and testing to see whether certain properties occur in the system or not. Reinforcement-based learning is a sub-field of Machine Learning, and in this case, learning does not rely on existing data but on studying the environment and identifying the best policy or strategy of action,” explains Or and Eliya. “With this project, we wanted to combine the two: Improve the capabilities of reinforcement-based algorithms by using tools of formal verification. We used a tool called NuSMV which, given a certain environment and query, checks whether or not that query is valid for that system.”

Or and Eliya’s project was supervised by Avraham Raviv and prof. Hillel Kugler. “Our lecture at the conference will revolve around formal verification, why it’s important, and how it can be used with Python,” they share. “Formal verification tools are not always user-friendly. Checking properties and states on certain systems requires code files that can be incomprehensible or simply too long. In addition, more often than not, the user interface is inconvenient or unclear. Python helps simplify the process and allows us to achieve a much more convenient user interface.