I wrote a program called scikit-verify. You give it a numerical function and it gives you back the equation that function computes.
Here is why I wrote it. Take this code:
def variance(x):
n = len(x)
return sum((x - x.mean())**2) / n
It runs fine and returns a reasonable number. It is also wrong, because it divides by n instead of n-1. No test that checks the output will find this, because the mistake is not in any input, it is in the equation, and the equation is not written down anywhere. It was in your head when you wrote the code and then it was gone.
The usual tools do not help here. Concolic testing, fuzzing, and property-based testing all work by choosing which inputs to run, but numerical code has almost no branches and the meaning is in the arithmetic between them. You can run every path through variance and still never see the n against n-1 mistake, because it happens the same way on every path.
scikit-verify recovers the equation instead. You run your function once and it returns the formula:
from skverify import to_sympy
import numpy as np
def weighted_rms(x, w):
return np.sqrt(np.sum(w * x**2) / np.sum(w))
out = to_sympy(weighted_rms, np.array([1.,2.,3.]), np.array([.5,.3,.2]))
print(out.formula)
# sqrt(Sum(w[j]*x[j]**2, (j, 0, 2)) / Sum(w[j], (j, 0, 2)))
Your function is not modified and not annotated. It runs once on values that carry both a number and a record of what was done to them. When NumPy does arithmetic, the program writes down the arithmetic. King described this pairing of a concrete run with a symbolic one in 1976, and the concolic testing people have used it for years to pick inputs. I use it to keep the expression rather than throw it away.
Once you have the equation you can check it against one you believe. This is a pytest test:
y = sympy.IndexedBase("y")
@specifies((y[0] + 4*y[1] + 2*y[2] + 4*y[3] + y[4]) / 3)
def test_simpson():
return (lambda y: simpson(y)), (samples,)
It passes if scipy's simpson computes the Simpson formula for every input of that shape, proved by symbolic equality rather than by comparing sampled outputs. If it fails you get both formulas and an input that separates them.
A single run only follows one path. When the code branches on the data, explore() takes over. It negates each recorded branch condition and asks Z3 for an input that satisfies the negation, then reruns the function on that input, and it keeps going until every branch has been reached or Z3 has proved that no input reaches it. It reports full coverage only when Z3 proves the branch conditions cover the whole domain. By default the check runs on every branch, so a passing test cannot hide a branch your test data never took.
When there is no closed form to compare against, you can state a property instead of a formula, and check_property decides it the same way. This checks that softmax sums to one on every reachable branch:
@specifies.property(lambda F: sympy.Eq(sum(F[k] for k in range(3)), 1))
def test_softmax():
return (lambda v: softmax(v)), (np.array([0.7, -1.2, 2.5]),)
If the program hits something it cannot turn into exact math, like a compiled LAPACK call, it does not guess. It stops:
to_sympy(lambda a: a.astype(int).mean(), np.array([1.4, 2.6])) # NotImplementedError: astype to non-float would change the math
A checker is only worth something if its yes means yes, so it returns an exact answer or it refuses out loud. A compiled call it cannot read gets sealed as a named symbol and checked against its defining equation, a solve against A x = b, a decomposition against U Σ Vᵀ = A. Z3 does that work too, generating a witness and verifying it by substitution, or returning unsat as a proof that no counterexample exists.
I ran it on a Markov chain library. Its stationary distribution routine goes through a compiled LAPACK eigendecomposition, which the program cannot read, so it sealed that call as a symbol and checked it against the equation the stationary distribution has to satisfy. The equation did not hold. The backend had passed a C-ordered array to a Fortran routine that wanted column-major order. The tests had missed it because they used symmetric matrices, where the wrong answer equals the right one, so no comparison of outputs could have caught what the defining equation did.
Here is what it does not do. The proof holds only at the shape you traced, so a property proved at length five says nothing about length six. It checks the mathematics and not the floating point, so a correct formula can still lose precision to cancellation. A branch guard that falls outside the theories Z3 decides, such as one built from transcendental functions, comes back marked undecided. And it checks your code against the formula you typed, not against the formula you should have typed, so if your formula is wrong it will prove your code matches it.
pip install scikit-verify. BSD licensed. It needs NumPy, SymPy, and z3-solver. The source is open. Tell me where it is wrong.
Aadya