黑料福利网

Department of Electrical Engineering organizes a lecture by visiting professor Alessandro Abate from University of Oxford, UK. 

Anyone interested is welcome to register and join.

Logic meets Learning - Formal Synthesis with Neural Templates

I shall present recent work on CEGIS, a ``counterexample-guided inductive synthesis'' framework for sound synthesis tasks that are relevant for dynamical models, control problems, and software programs. The inductive synthesis framework comprises the interaction of two components, a learner and a verifier. The learner trains a neural template on finite samples. The verifier soundly validates the candidates trained by the learner, by means of calls to a SAT-modulo-theory solver. Whenever the candidate is not valid, SMT-generated counter-examples are passed to the learner for further training. 
I shall elucidate the ins&outs of the CEGIS framework, and display its workings on a few problems: synthesis of Lyapunov functions and of barrier certificates; hybridisation of nonlinear dynamics for safety verification; synthesis of digital controllers for continuous plants; and an application in real-time autonomy. 

BIOGRAPHY

Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford, where he is also Deputy Head of Department. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received an MS/PhD from the University of Padova and UC Berkeley.  His research interests lie on the formal verification and control of stochastic hybrid systems, and in their applications in cyber-physical systems, particularly involving safety criticality and energy. He blends in techniques from machine learning and AI, such as Bayesian inference, reinforcement learning, and game theory.