Synthesis for Education

Speaker  Sumit Gulwani

Host  Anoop Gupta

Affiliation  MSR

Duration  01:06:31

Date recorded  14 January 2013

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).

©2013 Microsoft Corporation. All rights reserved.
> Synthesis for Education