Solving Recurrence Relations using Machine Learning, with Application to Cost Analysis

TL;DR

This paper introduces a machine learning-based method to solve complex recurrence relations in static cost analysis, overcoming limitations of existing solvers and enabling more effective resource usage predictions.

Contribution

It presents a novel, general approach combining machine learning, SMT-solving, and CAS to solve arbitrary constrained recurrence relations in cost analysis.

Findings

Successfully solves classes of recurrences unsolvable by existing tools.

Achieves reasonable computation times for complex recurrence relations.

Demonstrates effectiveness on recurrences generated by a cost analysis system.

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 other languages) are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions that are equivalent to (or a bound on) them. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with current solvers, such as 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 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. We have implemented a prototype and evaluated it with recurrences generated by a cost analysis system (the one in CiaoPP). The experimental results are quite promising, showing that our approach can find closed-form solutions, in a reasonable time, for classes of recurrences that cannot be solved by such a system, nor by current CASs.