Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs
This work addresses efficiency challenges in logic program synthesis for the ILP community, though it appears incremental by building on existing MIL methods.
The authors tackled the program synthesis problem in Inductive Logic Programming by incorporating user-provided types into the Meta-Interpretive Learning framework, resulting in a cubic reduction in search space size and synthesis time based on the number of typed background predicates.
The program synthesis problem within the Inductive Logic Programming (ILP) community has typically been seen as untyped. We consider the benefits of user provided types on background knowledge. Building on the Meta-Interpretive Learning (MIL) framework, we show that type checking is able to prune large parts of the hypothesis space of programs. The introduction of polymorphic type checking to the MIL approach to logic program synthesis is validated by strong theoretical and experimental results, showing a cubic reduction in the size of the search space and synthesis time, in terms of the number of typed background predicates. Additionally we are able to infer polymorphic types of synthesized clauses and of entire programs. The other advancement is in developing an approach to leveraging refinement types in ILP. Here we show that further pruning of the search space can be achieved, though the SMT solving used for refinement type checking comes