Support Vector Machines (spec models)

This file provides a small linear SVM baseline with explicit gradients.

PyTorch analogue:

• scoring function: score = X @ w + b (like nn.Linear(p, 1) without an activation),
• loss: hinge loss on signed labels y ∈ {−1, +1}: loss_i = max(0, 1 - y_i * score_i),
• optimization: a small deterministic gradient descent loop (not an optimized solver).

There are two "layers" in this file:

• LinearSVM: the clean mathematical model + objective + backward pass (VJP-style gradients);
• fitLinearSVM/SVM.predict: a small training + prediction wrapper used by runtime checks and examples.

Classic SVM literature often uses C for the weight on the hinge term. This implementation instead uses the equivalent primal form with an explicit L2 coefficient named lambda.

References:

• Cortes and Vapnik, "Support-Vector Networks", 1995.
• Vapnik, "The Nature of Statistical Learning Theory", 1995/1998.

Implementation status

No API builder implements this model, and no theorem is proved about it. It is a reference definition only.

Linear SVM (primal)

structure LinearSVM (p : ℕ) (α : Type) [TorchLean.Storage α] : Type

Linear SVM parameters: a weight vector w and bias b.

We intentionally keep "training hyperparameters" (regularization strength, learning rate, etc.) out of the parameter record; those are choices about an optimizer, not part of the model itself.

• w : TorchLean.Tensor α [p]

  Normal vector of the separating hyperplane.

• b : α

  Bias, or intercept, of the separating hyperplane.

def LinearSVM.decision {α : Type} [TorchLean.Storage α] [Context α] {p : ℕ} (m : LinearSVM p α) (x : TorchLean.Tensor α [p]) : α

Decision function f(x) = w·x + b.

def LinearSVM.decisionBatch {α : Type} [TorchLean.Storage α] [Context α] {n p : ℕ} (m : LinearSVM p α) (X : TorchLean.Tensor α [n, p]) : TorchLean.Tensor α [n]

Batch decision values for X : (n×p).

def hingeLossPerExample {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] (score y : α) : α

Hinge loss per example: ℓ_i = max(0, 1 - y_i * f(x_i)).

We write it using if rather than max to make the "active-set" logic explicit.

def hingeLossMean {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n : ℕ} (scores y : TorchLean.Tensor α [n]) : α

Mean hinge loss over a dataset.

def LinearSVM.objective {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n p : ℕ} (lambda : α) (m : LinearSVM p α) (X : TorchLean.Tensor α [n, p]) (y : TorchLean.Tensor α [n]) : α

L2-regularized SVM objective (primal, soft-margin style).

We use the common objective $\frac12\lambda\lVert w\rVert^2+\operatorname{mean}(\text{hinge loss})$.

Backward pass

For the objective

L(w,b) = ½λ‖w‖² + (1/n) Σ max(0, 1 - y_i (w·x_i + b))

the gradients are:

• ∂L/∂w = λ w + (1/n) Σ [margin_i < 1] * (-y_i x_i)
• ∂L/∂b = (1/n) Σ [margin_i < 1] * (-y_i)

We also return ∂L/∂X because it is sometimes useful for sensitivity analysis.

PyTorch analogy: this is what autograd would compute for 0.5*λ*||w||^2 + mean(relu(1 - y*(X@w+b))), except we write it out explicitly.

def LinearSVM.backward {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n p : ℕ} (lambda : α) (m : LinearSVM p α) (X : TorchLean.Tensor α [n, p]) (y : TorchLean.Tensor α [n]) : TorchLean.Tensor α [p] × α × TorchLean.Tensor α [n, p]

Backward/VJP for the linear SVM objective.

Returns (dw, db, dX) where:

• dw : ∂L/∂w
• db : ∂L/∂b
• dX : ∂L/∂X (sometimes useful for sensitivity analysis)

A Small Training Wrapper (Gradient Descent)

The LinearSVM definitions above are enough for "spec math". For examples/tests, it is convenient to package a trained parameter pair together with a simple predictor, so we provide:

• SVM: a small record holding (weights, bias) and a heuristic support-vector index tensor,
• fitLinearSVM: deterministic gradient descent using LinearSVM.backward,
• SVM.predict: sign prediction as ±1.

structure SVM (p n : ℕ) (α : Type) [TorchLean.Storage α] : Type

Small trained SVM bundle for examples/tests.

This is not a full SMO-style solver; it is a deterministic gradient-descent baseline that is useful as a reference model in the TorchLean spec layer.

• weights : TorchLean.Tensor α [p]

  Normal vector w of the separating hyperplane.

• bias : α

  Bias/intercept term b.

• supportVectorIndices : TorchLean.Tensor ℕ [n]

  One entry per training row: its index when the margin is near 1, or the sentinel n otherwise. Filter out n before using entries to index the training data.

def findSupportVectorIndices {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n p : ℕ} (X : TorchLean.Tensor α [n, p]) (y : TorchLean.Tensor α [n]) (finalWeights : TorchLean.Tensor α [p]) (finalBias : α) : TorchLean.Tensor ℕ [n]

Heuristic support-vector index extractor.

We mark an example as a "support vector" if its margin is close to 1. The output has one entry per training row, containing that row's index or the sentinel n for a non-support row. It is not a compact list of valid indices. This is only meant for introspection and examples (it is not used by the optimizer).

inductive SVM.FitError : Type

A training label outside the signed encoding used by the hinge objective.

• invalidLabel (row : ℕ) : FitError

  The zero-based row whose label is neither -1 nor 1.

@[instance_reducible]

instance SVM.instReprFitError : Repr FitError

def SVM.instReprFitError.repr : FitError → ℕ → Std.Format

@[instance_reducible]

instance SVM.instBEqFitError : BEq FitError

def SVM.instBEqFitError.beq : FitError → FitError → Bool

def fitLinearSVM {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n p : ℕ} (X : TorchLean.Tensor α [n, p]) (y : TorchLean.Tensor α [n]) (learningRate lambda : α) (iterations : ℕ) : Except SVM.FitError (SVM p n α)

Fit a linear SVM after checking that every label is -1 or 1.

The check uses the scalar context's equality operation and precedes every optimization step, including a request for zero steps. Binary 0/1 labels therefore cannot silently change the hinge objective. LinearSVM.objective and LinearSVM.backward remain explicit formulas for mathematical work with a supplied parameter record.

def fitLinearSVM.gradientDescent {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n p : ℕ} (X : TorchLean.Tensor α [n, p]) (y : TorchLean.Tensor α [n]) (learningRate lambda : α) (iter : ℕ) (weights : TorchLean.Tensor α [p]) (bias : α) : TorchLean.Tensor α [p] × α

def SVM.predict {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n batch p : ℕ} (model : SVM p n α) (X : TorchLean.Tensor α [batch, p]) : TorchLean.Tensor α [batch]

Predict signed labels ±1 using the learned hyperplane.

The training size n indexes the stored support-vector information. Prediction only needs the weights and bias, so the inference batch has an independent size. A zero decision value gives label -1; an empty batch returns an empty label tensor.

def SVM.predictOne {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {n p : ℕ} (model : SVM p n α) (x : TorchLean.Tensor α [p]) : α

Predict a signed label for one feature vector using the batch predictor's arithmetic.

def Kernel.linear {α : Type} [TorchLean.Storage α] [Context α] {p : ℕ} (x y : TorchLean.Tensor α [p]) : α

Linear kernel: k(x, y) = x·y.

def Kernel.polynomial {α : Type} [TorchLean.Storage α] [Context α] {p : ℕ} (degree : ℕ) (c : α) (x y : TorchLean.Tensor α [p]) : α

Polynomial kernel: k(x, y) = (x·y + c)^degree (naive power for generic α).

def Kernel.polynomial.powRec {α : Type} [Context α] (base : α) (exp : ℕ) : α

def Kernel.rbf {α : Type} [TorchLean.Storage α] [Context α] {p : ℕ} (gamma : α) (x y : TorchLean.Tensor α [p]) {h : p ≠ 0} : α

RBF kernel: k(x, y) = exp(-gamma * ||x - y||^2).

When the squared distance is finite, evaluate the usual distance-then-exponential expression. Finite feature differences can overflow that distance even when multiplication by a small gamma gives a representable exponent. In that case, multiply each difference by gamma before its second factor, then sum the weighted squares.