Symbolic AI and SMT solving

Dott. Enrico Lipparini
University of Cagliari

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 short course, 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 course, 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.

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

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