---

Symbolic AI and SMT solving
Dott. Enrico Lipparini
University of Cagliari

Schedule:  February 5th, 9:00-14:00, Lab Pes

Abstract

Symbolic AI is an approach to Artificial Intelligence that relies on deductive reasoning to produce exact, explainable solutions to well-defined problems. This contrasts with sub-symbolic methods (e.g., machine learning, NNs, and LLMs), which use statistical learning to address a wide range of (possibly vaguely defined) tasks, producing plausible but not always correct results that are typically hard to explain. Integrating symbolic and sub-symbolic techniques is a hot topic in AI (neuro-symbolic AI).

SMT (Satisfiability Modulo Theories) solvers are automated tools for reasoning about and rigorously solving problems involving arithmetic, arrays, bit vectors, and more. They are widely used in industrial settings for tasks such as program verification, planning, and testing.

In this seminar, we introduce Z3, an efficient and user-friendly SMT solver developed by Microsoft. We will compare it to both hand-written algorithms and LLM-based approaches on a simple illustrative problem, such as solving a Sudoku. Then, we will show how SMT solving can be used for program verification (i.e., checking whether a program satisfies a given specification), discussing some applications in smart contract security.

Throughout the seminar, students will actively engage with the material by working on a series of simple, guided exercises that will be assigned during the session, allowing them to experiment directly with the tool and reinforce the concepts discussed.

Exam
The final assessment consists of a small project developed using the Z3 Python APIs.

For further information on this activity, contact Prof. Bartoletti at bart@unica.it