Guide

numpy explore runs your NumPy function once and reports the mathematical expression it computed, together with the conditions under which that expression holds. This page explains the mechanism, how to read each output view, and exactly what is and is not being claimed.

How the trace works

Your function is executed once on traced arrays. Each traced value carries two things in lockstep. One is a concrete NumPy array, so your code runs on real numbers and takes real branches. The other is a SymPy expression recording what has been computed so far. NumPy operations are intercepted through the standard dispatch protocols, __array_ufunc__ for elementwise operations and __array_function__ for the rest, so the function itself is not modified, rewritten or annotated.

When your code branches on data, the truth test returns the concrete answer and the symbolic comparison is appended to the current path. The branch taken is therefore part of the result, not something that silently disappeared. This is the concolic style of execution, a concrete run and a symbolic run sharing one control flow.

The rule throughout is to return an exact expression or to refuse. There is no approximation step and no best-effort fallback, because a plausible but wrong formula is precisely the failure the tool exists to catch.

Writing a program

Type a function in the editor. The last function you define is the one traced, so helper functions above it are fine. np, numpy and sympy are in scope already.

def weighted_rms(x, w):
    return np.sqrt(np.sum(w * x**2) / np.sum(w))

By default you do not supply inputs. Each parameter is filled with a float array of length 5, and the symbols in the output are named after your parameters, so x above becomes the indexed symbol x[j]. Loops, helper variables, in-place updates and method-call style (x.mean()) all trace the same as their functional equivalents.

Choosing your own inputs

When the function needs something other than 1-D arrays, a matrix, a particular shape, or a scalar parameter, define ARGS at the top of the buffer and it is passed to the function verbatim:

ARGS = (np.array([[2.0, 1.0],
                  [1.0, 3.0]]),
        np.array([1.0, 2.0]))

def solve_sum(A, b):
    return np.linalg.solve(A, b).sum()

Arrays in ARGS are traced at exactly the shape you give them, and plain scalars stay symbolic, so ARGS = (x_sample, 2.0) for f(x, p) produces a formula with p as a free symbol. The solve example tab shows this in use.

The four views

For the weighted rms above, steps reads:

step 0: w[i]
step 1: x[i]
step 2: x[i]**2
step 3: step[2]*w[i]
step 5: Sum(w[j]*x[j]**2, (j, 0, 4))
step 6: w[i]
step 7: Sum(w[j], (j, 0, 4))
step 8: step[5]/step[7]
step 9: sqrt(step[8])
result: sqrt(step[8])

Each line is one operation the dispatch layer saw, in execution order. Step numbers can be skipped where an intermediate was folded into a later step.

Path conditions

Run the median example. The result is a single entry of the array, and beneath it are the comparisons that had to hold for that entry to be the median of the sample that was traced. The expression and its conditions are one object. Reporting the formula without the hypotheses it was derived under would overstate what the trace established, so the two are never separated.

Refusals

Some operations have no exact symbolic form. The refusal example casts to int midway, and integer truncation of a symbolic real has no faithful expression, so the trace stops with one sentence:

astype to non-float would change the math

A refusal is a designed outcome with a stated reason, not an error state. If you hit one on code you believe should trace, the reason names the missing mechanism.

Sealed compiled calls

Routines that bottom out in compiled code, LAPACK factorizations being the usual case, cannot be traced through. They become named symbols, and the concrete result is checked against the routine's defining equation on the actual arguments, in the result-checking tradition of Blum and Kannan. A solve is checked against Ax = b, an eigendecomposition against A v = w v. Try returning np.linalg.eig(a). The output comes back as eig_w[i] and eig_v[i, j], and the math tab lists eig under sealed calls, so the boundary of the symbolic reasoning is explicit rather than hidden.

Scope

Be precise about what a result here means.

• Claims are shape-specific. Arrays are traced at length 5, and an expression established at one shape is not thereby established at another.
• The trace follows one path, the one the concrete sample took. The conditions tell you which path that was. Covering the remaining branches is explore() in the library, which drives the Z3 solver and is not loaded in this page.
• Reasoning is over exact arithmetic. A confirmed expression says what the code computes mathematically, not that it is numerically stable in floating point.
• Checking an expression you supply, with check_formula and the @specifies decorator, is part of the library rather than this page.

pip install scikit-verify

Sharing

The copy link button encodes your program into the URL fragment. Fragments are not sent to any server, so the code travels inside the link and nowhere else. Opening a shared link adds a tab named shared.

Lineage

The ideas are old and good. Pairing a concrete execution with a symbolic one is King's symbolic execution (1976), run in the concolic style of Cadar and Sen. Checking a compiled routine's answer against its defining equation rather than trusting its name is Blum and Kannan's result checking (1989). The details, with the design document and measured coverage boards over NumPy, SciPy, scikit-learn and statsmodels, are in the repository.