The Power of Perseverance

In recent years, students in Prof. Hillel Kugler's laboratory have been working on using formal verification tools for artificial intelligence problems, particularly for agents that learn through deep reinforcement learning. "Previous projects studied relatively simple agents, but last year we expanded the connection between these fields to more advanced agents that learn through deep neural networks. The purpose of each project was to implement a solution we developed in the lab to improve a specific algorithm, with each project implementing the solution for a different problem," explains PhD student Avraham Raviv

Two of the projects, supervised by Raviv, were carried out by Shaiel Vistuch, Erel Dekel, and Boaz Gurevich, students in the computer engineering track. “Both projects were tasked with using verification tools to improve the robustness and efficiency of deep reinforcement learning by integrating formal verification techniques. This required of them to adopt innovative verification tools suitable for neural networks,” Raviv elaborates. "One project successfully demonstrated this on a problem called 'frozen lake,' and beyond just illustrating the concept, Shaiel managed to show that it works on medium-scale problems, not just small ones. In the second project, students Erel and Boaz implemented the same idea on another, inherently more complex problem, within a Japanese puzzle game called Sokoban."

"Our goal was to see if reinforcement-learning-based algorithms and formal verification could bolster each other and create a smarter agent. Since we didn't have much knowledge, we began researching both fields, and Avraham, our supervisor, provided us with papers and explained how the project would be structured," says student Erel Dekel, now a soldier. "Gradually, we started building a simple reinforcement learning agent and added formal verification tools designed to ensure that the agent has a goal and isn't just moving around randomly. Boaz and I developed the software ourselves, but Avraham was there for us with every problem we encountered, answering questions and meeting with us in person at the Faculty."

Raviv notes that while each project tackled a different problem, throughout the year the students frequently consulted with each other and worked in collaboration. "In the end, both projects successfully used what we developed in the lab for new problems. Therefore, we decided to write a paper presenting the theoretical idea and its implementation as demonstrated in each project."

From Final Project to Conference Paper - For the Third Consecutive Time

The jointly written paper required a division of labor: mentor Raviv was responsible for the theoretical part. The experimental section included two parts, one for each project, written by the students, with the results from both projects supporting the theory. "Writing the paper was a challenge," admits Erel. "Boaz and I were responsible for writing explanations about our project, providing examples from it that prove the effectiveness of combining reinforcement learning tools and formal verification, and for the related works section. Additionally, we had to read the rest of the paper and provide comments. The mentors handled the more formal parts, with the proofs and theories. We put a lot into this project and paper."

The paper was submitted for publication but was rejected. The academic year ended, and all three students enlisted in the IDF. But Raviv, their supervisor, did not give up. Over the past year he continued working on the paper and improving it. This month he received news that the paper was accepted to the International Symposium on Theoretical Aspects of Software Engineering (TASE) conference, to be held in July in Limassol, Cyprus.

"When Avraham called to tell me that the paper was accepted to the conference, I was in the military base dining hall and could barely hear him. I didn't even know it had been submitted again, and of course I was excited and very happy," says Erel. "Before publication, we needed to change a few things, and despite all three of us being soldiers now - we rallied to help, modify, and fix everything that needed fixing."

"This is the third time that a final project in our lab has turned into a paper published at international conferences. It's always exciting, and each paper takes a different path," says Raviv. "The students worked hard, did not give up even when faced with challenges, proposed innovative and beautiful ideas, and ultimately achieved excellent results. This is also an opportunity to express gratitude to Prof. Hillel Kugler who oversees everything and always pushes us forward."