Automated Reasoning and Learning for Automated Payroll Management

While payroll management is a crucial aspect of any business venture, anticipating the future financial impact of changes to the payroll policy is a challenging task due to the complexity of tax legislation. The goal of this work is to automatically explore potential payroll policies and find the optimal set of policies that satisfies the user’s needs. To achieve this goal, we overcome two major challenges. First, we translate the tax legislative knowledge into a formal representation flexible enough to support a variety of scenarios in payroll calculations. Second, the legal knowledge is further compiled into a set of constraints from which a constraint solver can find the optimal policy. Furthermore, payroll computation is performed on an individual basis which might be expensive for companies with a large number of employees. To make the optimisation more efficient, we integrate it with a machine learning model that learns from the previous optimisation runs and speeds up the optimisation engine. The results of this work have been deployed by a social insurance fund.

This project was executed in collaboration with Teal Partners.

Approach

Financial Modelling Language (FML)

The first step is translating the legal knowledge into a formal representation flexible enough to support and simulate a variety of scenarios.

Problem

• Given: Computational rules
• What: Optimise a target quantity while respecting the rules and given a number of open variables
• Why: Reuse existing knowledge base to offer new services
• How: Decoupling procedural knowledge and the knowledge in the rules

Technique: SMT

We will use techniques from constraint satisfaction, a declarative framework for modelling problems without the need to provide the steps towards the solution. Different paradigms exist: (1) Boolean satisfiability, (2) Constraint programming (CP), and (3) Satisfiability modulo theory (SMT).

To solve financial models, we use SMT. However, a problem is that typically there are no multiple multiplications between variables. Most common solvers are designed for Linear programming, Integer Linear Programming, or mixed-integer programming. All of these assume linear constraints.

The computation rules generated for our financial models contain structures like:

constraint Var1 = (Var2 * 23) div 100;
constraint Var3 = Var1 * Var4;

This is a non-linear computation that is diffcult to optimise in theory. However, there are lots of solvable problems in practice. One reason to choose SMT over CP is that CP-tools like MiniZinc need to linearize approximately and derive new bounds. We found only the solver SCIP with support for nonlinear constraints but it fails to propagate the boundaries because our financial models have too many nonlinear interactions.

A SMT-solver like Z3 has a dedicated solver for non-linear constraints and can deal with our models. Additionally, Z3 has native support for real numbers and has support for many programming structures because of its applications in program verification.

Optimisation

One of the goals of financial modeling is to optimize a number of parameters to minimize or maximize a certain value (e.g. reduce taxes). We support:

• Maximization, for example: $maximize\ income$
• Minimization, for example: $minimize\ cost$
• Reach target, for example: $minimize |value_{desired} - value_{possible}|$

Unfortunately, there is no support for optimising a target value. But for the financial models use here, we foresee a custom method that is based on binary search and takes into account the difference between SAT and UNSAT.

Often, there is no one best solution to minimize a target value. In such cases we are interested in finding a pareto front that expresses the trade-off between various parameters.

Machine Learning

The payroll optimisation task is performed on an individual employee basis. This can be an expensive task for a company of many thousands of employees. To overcome this issue, we can improve the efficiency of the optimisation step by using the solutions from previous calculations to provide a better initial point for the optimisation procedure. Though very few employees would share the identical characteristics, many employees would be similar which could give us a good estimate of the range for the optimal target value.

Remembering the optimal solutions for all previously solved cases is not a feasible strategy. Therefore, we will use machine learning to discover the relationship between the subset of input values of the individuals and the optimal payroll target and use the predicted value as an initial value during optimisation.