Synthesis for Education

Recently, program synthesis techniques have been successfully used for synthesizing small scripts from examples and natural language in the area of end-user programming. In this talk, I will describe some surprising applications of these synthesis techniques in the area of intelligent tutoring systems including solution generation, problem generation, automated grading, and even structured content entry. I will demonstrate these applications for various subject domains including ruler/compass based geometric constructions, algebraic proof problems, procedural math problems, automata theory, and introductory programming. The underlying synthesizers leverage search techniques from various communities including use of SAT/SMT solvers (formal methods community), version space algebras (machine learning community), and A*-style goal-directed heuristics (AI community).