Learning frameworks for program synthesis

Saha, Shambwaditya

Permalink

https://hdl.handle.net/2142/106251 Copy

Description

Title

Learning frameworks for program synthesis

Author(s)

Saha, Shambwaditya

Issue Date

2019-12-05

Director of Research (if dissertation) or Advisor (if thesis)

Parthasarathy, Madhusudan

Doctoral Committee Chair(s)

Parthasarathy, Madhusudan

Committee Member(s)

• Viswanathan, Mahesh
• Xie, Tao
• Singh, Rishabh

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• program synthesis
• machine learning
• program verification

Abstract

The field of synthesis is seeing a renaissance in recent years, where the task is to automatically synthesize small expressions or programs. One of the most prominent techniques counterexample guided inductive synthesis (CEGIS), uses a teacher(verification oracle) and a learner(learning algorithm) to learn such expressions across multiple rounds. A learning framework is a sub-framework of CEGIS where the learner is entirely agnostic of the specification and learns only from input-output examples provided by the teacher as natural notions of counterexamples. Thus, learning frameworks for synthesis have three components: the verification oracle, the notion of a natural counterexample, and the learning algorithm. The goals of this thesis are to study learning frameworks for synthesis, developing new and more efficient algorithms for learning, exploring new classes of counterexamples, and finding applications of synthesis to new domains. Specifically, by co-designing the notion of counterexamples, the learning algorithms, the verification oracle, and taking into account the aspects of the application domain, we achieved more effective program synthesis. We discuss learning frameworks for four different applications, illustrating the co-design of oracle-counterexample-learner for each of them. For the first application, we developed a general purpose SyGuS solver for piece-wise functions, using multiple learners to learn parts of the expression modularly and then compose them together to get the final expression. Second, we considered the application of automatic verification, where we synthesized inductive invariants using incomplete verification oracles. We also propose a novel property driven ICE learning algorithm to learn conjunctive inductive invariants. We considered specification mining for the next two applications, where we learned preconditions and postconditions of a method. Instead of using a verification engine as the oracle, which is not efficient, does not scale, and needs loop invariants, we bypassed all these limitations by using a test generator as the oracle.

Graduation Semester

2019-12

Type of Resource

text

Permalink

http://hdl.handle.net/2142/106251

Copyright and License Information

Copyright 2019 Shambwaditya Saha

Owning Collections