A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs

TL;DR

This work develops a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine learning (sparse-linear and symbolic) regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check whether such function is actually a solution of the recurrence.

Abstract

Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and many for other languages), as CiaoPP, are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with state-of-the-art solvers, including Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning (sparse-linear and symbolic) regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check if it is actually a solution of the recurrence. Our prototype implementation and its experimental evaluation within the context of the CiaoPP system show quite promising results. Overall, for the considered benchmarks, our approach outperforms state-of-the-art cost analyzers and recurrence solvers, and solves recurrences that cannot be solved by them. Under consideration in Theory and Practice of Logic Programming (TPLP).

Figures (7)

• Figure 1: Architecture of our novel machine learning-based recurrence solver.
• Figure 2: A program with a nested recursion.
• Figure 3: Comparison of solver tools by accuracy of the result.
• Figure 6: Candidate functions for linear regression in dimension $\leq 2$. ${\mathcal{F}_{\mathrm{small}}=S_{\mathrm{small}}}$, ${\mathcal{F}_{\mathrm{medium}}=\mathcal{F}_{\mathrm{small}}\cup S_{\mathrm{medium}}}$, ${\mathcal{F}_{\mathrm{large}}=\mathcal{F}_{\mathrm{medium}}\cup S_{\mathrm{large}}}$. Lambdas omitted for conciseness.
• Figure 8: Prolog encoding of the enqdeq benchmarks, inspired from Section 2.1 of jan-hoffman-phd introducing amortized analysis, where a queue datastructure is implemented as two lists that act as stacks. We encode the enqdeq problems for each tool following a best-effort approach. Recurrence equations are set up in terms of compositions of cost and size functions.

Theorems & Definitions (1)

• Example 1