A learning schema in which training is constituted by the elimination of explicit refutation witnesses against a finitely declared semantic object. Each update is triggered by an exhibited margin failure; the process terminates when no such witness remains in the declared obligation set. Convergence is therefore not asymptotic but certificated: closure holds when a decidable predicate over the finite table returns no counterexample.
Key materials:
Background and prerequisites:
Semantics lock
The declared interpretation under which the run is executed and checked: preprocessing, feature extraction, scoring rule, readout, tie-breaking, margin rule, and scan policy. The lock fixes what counts as the same learning problem. Changing the lock changes the certificate.
Witness table
The finite, enumerated table of labelled examples over which obligations are generated and checked. For purposes of the certificate, this table is not treated as a sample from an implicit completed domain. It is the declared finite domain on which closure is claimed.
Obligation
A finite condition imposed on a table entry under the semantics lock. In the current classification setting, the obligation is a margin condition: the true class must score at least the declared margin above every competing class.
Refutation witness
A concrete failure of an obligation. In the current setting, this is an example index together with a competing class showing that the true class does not exceed that competitor by the required margin. Its existence refutes the claim that the current state is closed.
State
The finite object being checked and subjected to refutation-repair. In the current prototype, the state consists of sparse integer weights together with cached scores. The general role of the state is to carry the learned interpretation under the lock.
Refutation-repair
The local update triggered by a refutation witness. A refutation-repair is indexed by a specific failed obligation: it modifies the state in order to remove that failure at the current point in the run. It is not a gradient step and not an unconstrained optimization move.
Trace
The replayable sequence of states, witnesses, and refutation-repairs produced by the run. A trace matters because it records why each transition occurred: each refutation-repair is justified by a named failed obligation.
State predicate
A decidable check over the finite state. In the current implementation, the main predicates are WF, CACHE.ok, and FULL.ok. These are not performance metrics; they are checks on representation, cache correctness, and finite closure.
Closure
The state in which FULL.ok holds: no refutation witness remains in the declared finite table under the declared semantics lock. Closure is exact but bounded. It is not a claim about examples outside the table.
Certificate
The finite evidence that the terminal state satisfies the declared checks under the lock. A certificate may include the lock, table, terminal state, trace information, hashes, and predicate results. It certifies finite closure, not generalisation.
Refutational Learning gives a finite, constructive account of supervised training under a declared semantics lock. A run is not characterized primarily as descent along a scalar objective, but as the successive elimination of explicit counterexamples to a finite set of declared obligations. The terminal claim is correspondingly bounded: closure holds only relative to the fixed interpretation and the finite witness table on which the obligations are defined.
The semantics lock fixes the objects with respect to which the run is meaningful: preprocessing, feature extraction, class set, scoring rule, readout, margin, tie-breaking convention, and scan order. Together with the finite witness table, these data determine the obligation set and the conditions under which a state may be accepted. A change in the lock changes the claim being certified.
In the present instance, a state has the form $\Sigma=(W,S)$, where $W$ is a sparse integer weight table and $S$ is a cached score matrix. The cache is not part of the semantic commitment; it is an implementation structure whose correctness is itself checked against definitional recomputation. The semantic object remains the locked feature map, scoring rule, and finite table.
For each example $i<N$ with true class $y_i$, and for each competing class $c\neq y_i$, the margin obligation is
A refutation witness is a concrete violation of this condition. It consists of an example and a competing class for which the current state fails to separate the true class by the declared margin. Thus failure is not represented only by an aggregate error, loss, or accuracy value; it is represented by a particular unmet obligation.
The next refutation-repair is selected by the locked scan order. The least index at which some margin obligation fails is
At this index, the competing class is chosen by the locked tie-broken readout,
The pair $(i^*,c^*)$ is the active refutation witness. It supplies the reason that the current state cannot yet be accepted.
The refutation-repair associated with this witness is local. Its magnitude is determined by the current slack,
together with the declared refutation-repair convention. In the sparse integer perceptron instance, the refutation-repair increases the active true-class weights and decreases the active competitor-class weights. The resulting score changes are propagated through the cache by postings. No differentiable loss surface is required for this operation.
Acceptance of a terminal state is expressed by finite predicates. WF asserts well-formedness of the finite representation. CACHE.ok asserts agreement between cached scores and definitional recomputation from $W$ and the locked feature sets. FULL.ok asserts the absence of any remaining refutation witness in the declared table.
Closure is the condition FULL.ok. It is exact, but only over the domain that has been declared. It certifies that every finite margin obligation induced by the lock and witness table has been discharged. It does not certify behavior outside the table, nor does it identify the learned evaluator with an intensionally richer rule beyond the declared semantics.
The trace records the successive states, witnesses, and refutation-repairs,
Its significance is proof-theoretic: each transition is licensed by a named failure of the current state, and the terminal state is accepted only after the finite predicates can be independently checked. The artifact is therefore not merely a trained classifier, but a bounded certificate of closure under the declared interpretation.
This also fixes the permitted substitution. Once closure and cache correctness hold, the learned evaluator may replace the reference evaluator on the locked finite table. The substitution is extensional and bounded. It establishes agreement on the declared table; it does not license claims about examples outside the table or about the identity of underlying programs.
The contrast with gradient descent is consequently evidential rather than competitive. Gradient descent records movement under an aggregate objective. Refutational Learning records the obligation whose failure induced each update. The distinction concerns the structure of the training record: scalar trajectory on one side, witness-indexed refutation-repair trace on the other.
The Boolean demonstrations exhibit this structure on small finite tables. The EMNIST baseline instantiates the same schema on a larger image-derived table. In both cases, the formal claim is not benchmark superiority, but the production of a finite, replayable, and checkable account of closure under a declared semantics lock.
The demo instantiates the refutation-repair loop on small Boolean datasets and runs it in parallel with an SGD trace under the same locked readout rule. All parameters are declared before either trace is generated.
Stepping through the traces reveals what each method makes available for inspection: Refutational Learning exposes the current margin violation, its named refutation witness, and the resulting integer refutation-repair; Gradient Descent exposes the aggregate loss and classification accuracy at each update.
Step 1. We define a target.
Select a Boolean function as a problem:
Witness table (editable):
Format. Input values are space-separated, followed by the delimiter | and an integer class label. Example: 0 1 | 1.
Step 2. Declare the run budget and update-rule parameters.
Shared cycle budget C: .
One cycle constitutes one attempted update: a single refutation-repair step for Refutational Learning, or a single SGD step for Gradient Descent. The two traces share the same cycle budget to make their execution lengths comparable; no claim about equal computational cost is implied.
Seed:
Scan order:
On the GD side, deterministic scan order renders replay unconditional; seeded shuffle introduces stochasticity while preserving full reproducibility. Refutational Learning always selects the earliest refutation witness, independent of scan-order setting.
For Refutational Learning,
margin $\gamma$: , overshoot $\Delta$: .
For the loss-landscape comparison,
learning rate $\eta$: .
Step 3. Generate and inspect the two traces.
The semantics lock declares what is held invariant across the comparison. Without such a declaration, differences in preprocessing, readout, tie-breaking, or evaluation criteria confound any attribution of trace-level differences to the training methods themselves.
Symbolically, $\mathcal{L}$ records $K$ classes, $N$ examples, $F$ features, prediction by $\arg\max\nolimits^{*}$, and the scan schedule.
Semantics Lock:
Step 4. Analyse the traces. Both methods execute over the same finite witness table for the declared cycle budget.
State:
Snapshot:
Refutational Learning log: each entry records the active refutation witness, the competing class, the integer refutation-repair magnitude, and the resulting predicate state.
Interpretation:
Snapshot:
Gradient Descent log: each entry records the per-cycle loss, current prediction, and aggregate accuracy.
Interpretation:
The display below abstracts away from any particular dataset or model class. It presents Refutational Learning as a finite arithmetic procedure: obligations are evaluated under a declared lock, failures are returned as refutation witnesses, and each refutation-repair is justified by a contract on the failed margin. Closure is reached only when the bounded search for such witnesses returns none.