Gradient descent on (x − 1)² is run not on one number but on an interval of
possible starting points. Every bound is a ground fact with a proof, so the run
is certified, and the certificate shows the guaranteed interval shrinking
toward the minimum.
Run it in the playground · Source
Minimize f(x) = (x − 1)² with step size η = 0.2, starting from anywhere in
the interval [0, 2]. After each step, which interval is the current point
guaranteed to lie in, and does that interval shrink?
Instead of trusting floating-point output, each step is derived from the previous one by explicit rules, so a proof can show why each bound holds.
max_k(10).
target(1.0).
eta(Eta) :- (Eta is 1.0 / 5).
x_bounds(0, 0.0, 2.0).
The gradient of (x − 1)² is 2(x − 1). Its bounds at step K follow from
the bounds on x:
g_bounds(K, Gl, Gu) :-
target(A),
x_bounds(K, L, U),
(Dl is L - A),
(Du is U - A),
(Gl is 2 * Dl),
(Gu is 2 * Du).
x_bounds(K1, L1, U1) :-
previous(K1, K),
x_bounds(K, L, U),
eta_le_half(true),
target(A),
eta(Eta),
(Dl is L - A),
(Du is U - A),
(L1 is L - Eta * 2 * Dl),
(U1 is U - Eta * 2 * Du).
The update x' = x − 2η(x − 1) is applied to each endpoint on its own. That is
sound only because, for η ≤ 1/2, the update is increasing in x: a larger
starting point always lands at a larger next point, so the image of [L, U]
is exactly [L1, U1]. The rule checks eta_le_half(true) before using it.
eyeprolog examples/gd-step-certified.pl
xBounds(result, bounds(0, 0.0, 2.0)).
xBounds(result, bounds(1, 0.4, 1.6)).
xBounds(result, bounds(2, 0.64, 1.36)).
xBounds(result, bounds(3, 0.784, 1.216)).
width(0, 2.0).
width(1, 1.2000000000000002).
width(2, 0.7200000000000001).
...
width(10, 0.012093235200000052).
The midpoint stays at 1.0, the true minimum, and the certified interval
shrinks by the factor 1 − 2η = 0.6 per step, from width 2 to about 0.012
after ten steps. widthContractsAt/2 holds at every step from 1 to 10, and the
run prints 89 facts in all.
A naive interval update computes the interval of possible steps, η·f'(x) over
[L, U], and subtracts it from [L, U]. That treats the x in the update and
the x inside the gradient as two independent unknowns, so the worst cases add
up and the width grows by 1 + 2η per step: from 2 to about 58 after ten
steps. This is the classic dependency problem of interval arithmetic.
Updating each endpoint with itself avoids it, and the monotonicity condition
η ≤ 1/2 is what makes that sound. The step bounds are still reported, as
stepBounds/2, but only as information.
eyeprolog --proof examples/gd-step-certified.pl
step(stepBounds(result, step(0, -0.4, 0.4)),
rule(50),
['K' = 0, 'Pl' = -0.4, 'Pu' = 0.4],
[index(0), p_bounds(0, -0.4, 0.4)]).
step(width_contracts_at(1, true),
rule(34),
['K1' = 1, 'K' = 0, 'W' = 2.0, 'W1' = 1.2000000000000002],
[eta_le_half(true),
The first step’s bounds [-0.4, 0.4] come from rule 50 applied to
p_bounds/3. The contraction at step 1 rests on eta_le_half(true) and the
two widths, 2.0 and about 1.2. The step for x_bounds(1, 0.4, 1.6) uses the
update rule with 'Eta' = 0.2, resting on x_bounds(0, 0.0, 2.0), so every
bound traces back to the starting interval.
condition('C1', resolution, ok, 211).
condition('C5', re_decision, ok, 187).
steps(398).
verified(211).
recomputed(187).
trusted(0).
claims(89).
verdict(checked).
211 steps were replayed against program clauses, and 187 arithmetic steps were recomputed independently by the checker. Nothing is trusted: every number in the certificate is re-derived.
eta to 1.0 / 2. The width drops to 0.0 after one step: for a
quadratic, that step size jumps straight to the minimum.eta to 3.0 / 5. Only x_bounds(0, …) remains, because
eta_le_half fails and the update rule refuses to run. Why would updating
the endpoints separately be wrong once the update is decreasing in x?L1 is L - Pu and
U1 is U - Pl from p_bounds/3, and watch the width grow instead.:- table x_bounds/3. and compare --stats before and after.Learn more in The Art of EyeProlog, Chapter 29.