Algebro-geometric Approaches to Automated Program Synthesis

PhD Qualifying Examination


Title: "Algebro-geometric Approaches to Automated Program Synthesis"

by

Mr. Hitarth SINGH


Abstract:

Automated program synthesis is the problem of generating a program from 
high-level specifications in a given domain-specific programming language 
(DSL). The construction ensures that the program is correct and meets the 
high-level specifications used to generate the program. Synthesis has 
applications from allowing people without programming experience to automate 
routine tasks to creating safety-critical programs.

Many techniques have been developed and studied for program syntheses such as 
enumerative techniques, deductive techniques, machine learning-based 
techniques, genetic programming, and constraint-based techniques. Programming 
By Example (PBE), for instance, is the technique in which the user expresses 
their intent by providing input-output examples as the specifications. We will 
survey various techniques for program synthesis.

Program synthesis has practical applications in diverse fields. Various 
synthesis tools have been developed that help the user to synthesize programs 
to perform routine tasks like data cleaning, data transformation, and 
converting raw semi-structured data into more structured data that is easier to 
analyze. Synthesis has also been applied to graphics; given a drawing with a 
repeated pattern, one can generate a program that, when executed, draws the 
same pattern but for an arbitrary size. We survey various exciting applications 
of synthesis.

Template-based synthesis problem is one where the programmer provides the 
high-level structure of the program while leaving the low-level details as 
holes for the synthesis engine to fill. Polynomial program is the class of 
imperative programs where each expression is restricted to be a polynomial over 
the program variables. It forms a highly expressive class of programs used in 
cyber-physical systems, and as subroutines in complex programs. Polynomial 
programs can also represent many real-world programs through over-approximation 
of program behavior through abstract interpretation.

We present our synthesis algorithm for polynomial programs based on tools from 
algebraic geometry such as Handelman’s Theorem and Putinar's 
Positivstellensatz. Broadly, our algorithm eliminates the quantifier 
alternation and reduces the synthesis problem to quadratic-constrained 
quadratic programming (QCQP). This reduction makes the otherwise intractable 
problem solvable using the SMT solvers like Z3 and MathSAT. The field of 
synthesis is quite broad and has exciting research opportunities. We conclude 
with future research directions in polynomial program synthesis.


Date:			Monday, 6 February 2023

Time:                  	11:00am - 1:00pm

Venue:                  Room 5501
                         Lifts 25/26

Committee Members:	Dr. Amir Goharshady (Supervisor)
  			Prof. Pedro Sander (Chairperson)
 			Dr. Sunil Arya
 			Dr. Dimitris Papadopoulos


**** ALL are Welcome ****