Type guided program synthesis: at the intersection of programmer tools, proof assistance and explainable AI
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
EPSRC research areas: Artificial intelligence technologies, Logic and combinatorics, Programming languages and compilers, Theoretical Computer Science, Verification and correctness.
Potential impact: Program synthesis, among the oldest problems in computer science, has great potential for addressing the newly arising problem of explainable AI. Programming often involves small tasks that seem trivial and tedious. Program synthesis will soon become a mainstream tool to either quickly solve such problems (by generating a program) or to let the programmer know that a non-trivial task is at hand. At the same time synthesis can be understood as automated proof search, iteratively applying formal rules until a valid proof has been found. Within AI, program synthesis has great promise as a paradigm for generating programs that are not just understood by machines, but also allow humans to effectively reason about their behaviour.
Context: The starting off point will be research conducted for a master's thesis on the effectiveness of types in reducing the program hypothesis space in the setting of Inductive Logic Programming (ILP), i.e. generating logic programs from examples. Having identified typing of programs as important structure for synthesis, the DPhil will focus on leveraging refinement types (and related concepts) as a tool for the specification of synthesis problems, as well as letting types guide the search.
A type refinement are propositions which restrict the values that belong to that type. Refinements allow us to reason about when composing programs makes sense. As automation of program/proof generation is the goal, deciding on whether combined refinements describe programs that are still compatible with the synthesis specification is important. For synthesis to be useful it needs to be done rapidly. The issue is that for each partial program considered, during synthesis, the satisfiability of the refinements in the program needs to be determinded. Especially promising are Satisfiability Modulo Theories (SMT) solvers, as they have proven to be very efficient on restricted logics.
Major trends that influence the direction of the work are the Meta-Interpretive Learning (MIL) framework originating in ILP and the automation that is available in proof assistants (e.g. Coq.). Both approaches rely on the user to supply programs/proofs and metarules/tactics to inform the synthesizer of the kinds of hypotheses to consider. The correspondence between programs and proofs is well known; the relation between metarules, an encoding of the allowed structure of the program, and that of tactics, aggregations of rules for backward reasoning in proof construction, has yet to be considered in detail.
Aims and objectives:
Vastly improve on the master's thesis approach of utilizing SMT solving to decide on compatibility of type refinements. The prime interest is in identifying encoding to logic fragments that are effective for synthesis. Use the MIL framework as a testbench.
Evaluate whether it is possible to encode the synthesis problem in a logic as a SMT problem
Determine whether the strong structural properties of logic programs, captured by metarules, lead to an description of structural patterns in functional programs/proofs useful in synthesis.
Investigate how metarules and tactics relate, respectively (logic) program synthesis and proof search in proof assistants, and find areas where they can reinforce each other.
Determine how users' intuitions for strong structural properties, such as the need for nested induction/mutually recursion (on particular variables), can be captured as high level rules in these frameworks and how such hints can be used to restrict the search space.
Collaborators:
Prof. Luke Ong (DPhil & MSc thesis supervisor)
Prof. Jeremy Gibbons (DPhil supervisor)
Dr. Andrew Cropper (MSc thesis supervisor)
Potential impact: Program synthesis, among the oldest problems in computer science, has great potential for addressing the newly arising problem of explainable AI. Programming often involves small tasks that seem trivial and tedious. Program synthesis will soon become a mainstream tool to either quickly solve such problems (by generating a program) or to let the programmer know that a non-trivial task is at hand. At the same time synthesis can be understood as automated proof search, iteratively applying formal rules until a valid proof has been found. Within AI, program synthesis has great promise as a paradigm for generating programs that are not just understood by machines, but also allow humans to effectively reason about their behaviour.
Context: The starting off point will be research conducted for a master's thesis on the effectiveness of types in reducing the program hypothesis space in the setting of Inductive Logic Programming (ILP), i.e. generating logic programs from examples. Having identified typing of programs as important structure for synthesis, the DPhil will focus on leveraging refinement types (and related concepts) as a tool for the specification of synthesis problems, as well as letting types guide the search.
A type refinement are propositions which restrict the values that belong to that type. Refinements allow us to reason about when composing programs makes sense. As automation of program/proof generation is the goal, deciding on whether combined refinements describe programs that are still compatible with the synthesis specification is important. For synthesis to be useful it needs to be done rapidly. The issue is that for each partial program considered, during synthesis, the satisfiability of the refinements in the program needs to be determinded. Especially promising are Satisfiability Modulo Theories (SMT) solvers, as they have proven to be very efficient on restricted logics.
Major trends that influence the direction of the work are the Meta-Interpretive Learning (MIL) framework originating in ILP and the automation that is available in proof assistants (e.g. Coq.). Both approaches rely on the user to supply programs/proofs and metarules/tactics to inform the synthesizer of the kinds of hypotheses to consider. The correspondence between programs and proofs is well known; the relation between metarules, an encoding of the allowed structure of the program, and that of tactics, aggregations of rules for backward reasoning in proof construction, has yet to be considered in detail.
Aims and objectives:
Vastly improve on the master's thesis approach of utilizing SMT solving to decide on compatibility of type refinements. The prime interest is in identifying encoding to logic fragments that are effective for synthesis. Use the MIL framework as a testbench.
Evaluate whether it is possible to encode the synthesis problem in a logic as a SMT problem
Determine whether the strong structural properties of logic programs, captured by metarules, lead to an description of structural patterns in functional programs/proofs useful in synthesis.
Investigate how metarules and tactics relate, respectively (logic) program synthesis and proof search in proof assistants, and find areas where they can reinforce each other.
Determine how users' intuitions for strong structural properties, such as the need for nested induction/mutually recursion (on particular variables), can be captured as high level rules in these frameworks and how such hints can be used to restrict the search space.
Collaborators:
Prof. Luke Ong (DPhil & MSc thesis supervisor)
Prof. Jeremy Gibbons (DPhil supervisor)
Dr. Andrew Cropper (MSc thesis supervisor)
Organisations
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509711/1 | 01/10/2016 | 30/09/2021 | |||
| 2054778 | Studentship | EP/N509711/1 | 01/10/2018 | 31/03/2022 | Rolf Morel |