Meetings

Functional Synthesis: Formal Methods meets Machine Learning

When: Thursday, September 29, 2022, 11am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Functional Synthesis: Formal Methods meets Machine Learning.

Speaker: Priyanka Golia, Ph.D. candidate at IITK, India and NUS, Singapore.

Abstract

Given a specification F(X,Y) over the set of input variables X and output variables Y, we want the assistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850’s and yet scalability remains a core challenge. Motivated by progress in machine learning, we design a new algorithmic framework Manthan, which views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 509 benchmarks in comparison to 280, which is the most solved by a state of the art technique. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.

The talk is based on following two papers:

1. [CAV-2020] Manthan: A Data-Driven Approach for Boolean Function Synthesis
2. [ICCAD 2021] Engineering an Efficient Boolean Functional Synthesis Engine.

Short Bio

Priyanka Golia is Ph.D. candidate at IITK, India and NUS, Singapore. Her research interest lies in the area of functional synthesis, constrained sampling, and knowledge compilation. She is the lead designer of the state-of-the-art functional synthesis engine Manthan, which takes advantage of advances in machine learning, constrained sampling, and automated reasoning to synthesize Boolean functions efficiently.

Material

• Video (restricted access)

Symbolic tableaux for LTL/LTLf satisfiability

When: Thursday, September 22, 2022, 11am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Symbolic tableaux for LTL/LTLf satisfiability

Speaker: Dr. Nicola Gigante, Researcher (RTD/a) at Free University of Bozen-Bolzano, Italy.

Abstract

Tableau methods are among the first techniques studied to solve the satisfiability problem for a variety of logics, including linear temporal logic (LTL). Recent developments in the field of tableau methods for LTL include a tree-shaped tableau by Reynolds which improved the state of the art in various directions. However, in the practical usage, tableau methods for LTL usually still suffer on formulas that require complex propositional reasoning, because of the huge size of the tableau tree which, especially in unsatisfiable instances, has to be explicitly explored entirely. In this talk, we introduce the “symbolic tableau” approach, where a propositional encoding of the Reynolds tableau, solved by efficient state-of-the-art SAT solvers, is used to symbolically traverse the tableau tree. The approach combines the advantages of tableau methods (in particular the termination guarantees) with the efficiency of bounded model checking-like approaches. The approach has been implemented in BLACK (Bounded Ltl sAtisfiability ChecKer), a robust and featureful tool that supports LTL, LTLf, and other linear-time logics.

Short Bio

Nicola Gigante got his PhD at the University of Udine in 2019, and after a couple of years there as a postdoc, he is now a researcher at the Free University of Bozen-Bolzano. His main research interests lie at the intersection between AI and formal methods, with a focus on temporal reasoning, including temporal logics, planning, and reactive synthesis.

Material

• Video (restricted access)

Feature-based Generalized Policies and Guarantees

When: Wednesday, September 7, 2022, 12pm (CEST).

Where: Room B203, DIAG & Zoom online, check the address in the Google Calendar Event.

Topic: Feature-based Generalized Policies and Guarantees

Speaker: Prof. Blai Bonet, retired Professor of Computer Science from Universidad Simón Bolívar, and currently research associate at the Universitat Pompeu Fabra, Barcelona, Spain.

Abstract

In recent years, generalized planning has become an important thread in planning and deep reinforcement learning (DRL). In the logical setting, a successful approach for generalized planning is to express general policies or strategies with rules over state features as the latter provide the necessary abstraction over classes of planning instances with different sets of grounded actions, and the rules tell which transition to take at non-goal states. Furthermore, the same type of rules can also be used to express general strategies based on subgoal-based decompositions that are guarantee to be executable in polynomial time. In this talk, we revise the main ideas underlying these approaches and address the task of establishing formal guarantees for general policies.

Short Bio

Prof. Blai Bonet is retired professor from the Computer Science Department at Universidad Simon Bolivar, Venezuela, and currently a research associate at the Universitat Pompeu Fabra, Barcelona, Spain. He received his Ph.D. degree in computer science from the University of California, Los Angeles. His research interests are in the areas of automated planning, search and knowledge representation, deep learning, and theory of computation. Blai has received several best paper awards or honorable mentions, including the 2009 and 2014 ICAPS Influential Paper Awards, and he is a co-author of the book “A Concise Introduction to Models and Methods for Automated Planning”. He has served as associate editor of Artificial Intelligence and the Journal of Artificial Intelligence Research (JAIR), conference co-chair of ICAPS-12, program co-chair of AAAI-15, and has been a member of the Executive Council for ICAPS and AAAI.

Material

• Video (restricted access)

Factored Planning: From Classical Planning to Dec-POMDPs

When: Thursday, July 7, 2022, 12pm (CEST).

Where: Room A2, DIAG & Zoom online, check the address in the Google Calendar Event.

Topic: Factored Planning: From Classical Planning to Dec-POMDPs

Speaker: Prof. Ronen Brafman, Scharf-Ullman Chair in Computer Science at Ben-Gurion University in Israel.

Abstract

The idea of taking a problem and solving it by decomposing it to multiple smaller problems and then somehow combining them together has motivated algorithm design in many different area. I this talk I will review an evolving journey motivated by this idea that I’ve been taking with the help of many colleagues. Starting from an attempt to make classical planning more efficient, it evolves into distributed classical planning, privacy preserving multi-agent planning, multi-agent forward search, and eventually (for now?) planning in decentralized POMDPs. Common to most of these techniques is the idea of identifying the parts of the problem (variables/actions) involving multiple components/agents and those relevant to one component only. This then allows us to formulate an abstract problem whose solution forms a skeleton to the solution of the real problem. This skeleton then serves to partition the problem into multiple independent problems involving one component/agent only, that can be solved in parallel.

Short Bio

Prof. Ronen Brafman is the Scharf-Ullman Chair in Computer Science at Ben-Gurion University in Israel. He obtained his Ph.D. from Stanford University in 1996, was a Post-Doctoral Fellow at UBC, and was a research scientist at NASA AMES Research Center between 2004-2006. His work spans diverse aspects of decision making, including preference modeling and reinforcement learning, where he co-developed the CP-nets model and the R-max algorithm, but he is mostly interested in decision making under uncertainty, and more recently, planning for multi-agent systems where he co-introduced the MA-STRIPS model and privacy preserving planning. Ronen is also interested in applying planning to robotics, and improving the practice of software engineering for autonomous robots. He served as Program and Conference Chair for ICAPS, an Associate Editor for JAIR, AIJ, and JAAMAS, and is a AAAI and EurAI fellow.

Material

• Video (restricted access)

Iterative Depth-First Search for Fully Observable Non-Deterministic Planning

When: Friday, June 10, 2022, 10am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Iterative Depth-First Search for Fully Observable Non-Deterministic Planning

Speaker: Dr. Ramon Fraga Pereira, Research Associate at the Dipartimento di Ingegneria Informatica, Automatica e Gestionale (DIAG) at Sapienza Università di Roma, working with Prof. Dr. Giuseppe De Giacomo on his Advanced ERC project WhiteMech.

Abstract

Fully Observable Non-Deterministic (FOND) planning models uncertainty through actions with non-deterministic effects. Existing FOND planning algorithms are effective and employ a wide range of techniques. However, most of the existing algorithms are not robust for dealing with both non-determinism and task size. In this paper, we develop a novel iterative depthfirst search algorithm that solves FOND planning tasks and produces strong cyclic policies. Our algorithm is explicitly designed for FOND planning, addressing more directly the non-deterministic aspect of FOND planning, and it also exploits the benefits of heuristic functions to make the algorithm more effective during the iterative searching process. We compare our proposed algorithm to well-known FOND planners, and show that it has robust performance over several distinct types of FOND domains considering different metrics.

Short Bio

Dr. Ramon Fraga Pereira is a Research Associate at the Dipartimento di Ingegneria Informatica, Automatica e Gestionale (DIAG) at Sapienza Università di Roma, working with Prof. Dr. Giuseppe De Giacomo on his Advanced ERC project WhiteMech. He obtained his Ph.D. degree in 2020, at Pontifical Catholic University of Rio Grande do Sul (PUCRS), Porto Alegre, Brazil, under the supervision of Prof. Dr. Felipe Meneguzzi (PUCRS) and Dr. Miquel Ramírez (University of Melbourne). During his Ph.D. (from June 2018 to April 2019) he was a Ph.D. Intern in the School of Computing and Information at the University of Melbourne, under the supervision of Dr. Miquel Ramírez.

In 2020, he was recognized as having the best Ph.D. thesis in Artificial Intelligence in Brazil, CTDIAC at 9th the Brazilian Conference on Intelligent Systems (BRACIS).

His research is in the field of Artificial Intelligence, particularly in the area of Automated Planning. Over the past years, he has been working on Goal and Plan Recognition techniques over several types of domain models.

Material

• Video (restricted access)

Best-effort synthesis

When: Thursday, May 12, 2022, 9am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Best-effort synthesis

Speaker: Prof. Sasha Rubin, Senior Lecturer, Leader of the Computational Logic for Artificial Intelligence (LOGIC-AI) group in the School of Computer Science, The University of Sydney.

Abstract

In the classic formulation (Pnueli and Rosner 1989), the synthesis problem concerns finding an agent strategy that guarantees that a specification formula expressed in linear-time temporal logic (LTL) is satisfied irrespective of the actions of the environment (this can be seen as an analogue of Planning with temporally extended goals in AI).

What should an agent do when it can’t achieve its task in all circumstances? In the classic formulation the agent ‘gives up’ (i.e., the synthesis procedure returns ‘unsynthesisable’). However, what if giving up is not acceptable? One idea might be to do as well as possible, i.e., do a ‘best effort’. In this talk I will offer a formalisation of what it means that an agent strategy does a best effort, and discuss how to algorithmically solve such synthesis problems using automata-theory.

This talk is based on joint works with Benjamin Aminof, Giuseppe De Giacomo, Alessio Lomuscio, and Aniello Murano.

Short Bio

Sasha Rubin is a Senior Lecturer and the Leader of the Computational Logic for Artificial Intelligence (LOGIC-AI) group in the School of Computer Science, The University of Sydney. His main interest is in Logic and Formal Methods for AI. In particular: Foundations of synthesis and planning for temporally extended goals, Logics for games and strategic reasoning, multiplayer games, imperfect information, incomplete information, Formal methods for multi-agent systems Automata theory, Finite and algorithmic model theory.