Relational program synthesis with numerical reasoning
This addresses a specific bottleneck in program synthesis for tasks requiring numerical reasoning, such as game playing and program synthesis, but appears incremental as it builds on existing relational and SMT-based methods.
The paper tackles the problem of learning programs with numerical values, especially continuous values like intervals, by introducing NUMSYNTH, an inductive logic programming approach that combines relational learning with numerical reasoning using satisfiability modulo theories solvers. The results show it can learn such programs and outperform existing approaches in predictive accuracies and learning times across four domains.
Program synthesis approaches struggle to learn programs with numerical values. An especially difficult problem is learning continuous values over multiple examples, such as intervals. To overcome this limitation, we introduce an inductive logic programming approach which combines relational learning with numerical reasoning. Our approach, which we call NUMSYNTH, uses satisfiability modulo theories solvers to efficiently learn programs with numerical values. Our approach can identify numerical values in linear arithmetic fragments, such as real difference logic, and from infinite domains, such as real numbers or integers. Our experiments on four diverse domains, including game playing and program synthesis, show that our approach can (i) learn programs with numerical values from linear arithmetical reasoning, and (ii) outperform existing approaches in terms of predictive accuracies and learning times.