Automated programming using constrained inductive logic programming

Abstract

This doctoral thesis presents a novel and general framework for using constraints expressed in propositional logic when performing program synthesis in inductive logic programming. The constraints are used to restrict the search space and can be inserted both statically before search begins and dynamically during search. We present practical instances of constraints, derived from pruning the search space, input-output specifications of predicates, functional predicates, variable splitting, and constraint relations. The main motivations for using these constraints are performance and accuracy gains, as smaller search space regions have to be explored. Undesirable or practically unrealizable solution forms are never generated. Moreover, by solving the constraints using a complete boolean satisfiability solver (SAT solver), search space exhaustion can be detected, leading to guaranteed optimal results. Constraints can be used to dynamically direct the search towards arbitrary regions of the search space, providing a more flexible alternative to top-down and bottom-up refinement operators. Various aspects of choosing an efficient SAT solver are discussed. We pay special attention to DPLL-based solvers, with the use of non-trivial optimizations— such as clause learning and non-chronological backtracking—when embedding the solver into an inductive logic programming system. Some minor internal adjustments to the SAT solver are needed, which we discuss. Benchmarks are performed to measure the benefits of using constraints, both in the classical and noisy settings. In both settings, the results show that the presented constraint framework provides a significant performance boost without loss of accuracy, thus being well suited for program synthesis problems. Lazy evaluation strategies for both positive and negative coverage are discussed in conjunction with pruning constraints. All research in this thesis is implemented in Atom, our inductive logic programming system. For users, we describe Atom’s syntax; give guidelines on how to specify efficient mode declarations, constraints, and examples; discuss adjustable parameters; and how to produce search space graphs for visualization. For researchers, we also give implementation details and correctness proofs: data structures used (representation), bottom clause construction and related optimizations, induction algorithms, and evaluation functions. We conclude the thesis with a discussion of our contribution and possible extensions

Date of Award	16 Feb 2015
Original language	English
Awarding Institution	City University of Hong Kong
Supervisor	Shiu Yin Kelvin YUEN (Supervisor)