← /projects
$cat ~/projects/bend-ml/README.md

bend-ml

Machine learning in Bend. Tensor shapes live in the types; structural guarantees are checked by the kernel.

packages
5 on BendHub
demos
MNIST · GPT-2
checks
kernel · PyTorch
bend-ml42c8aea

what I built

I built bend-ml to take machine learning in Bend beyond a small example: tensors, a tokenizer, automatic differentiation, and models that actually run. The five packages are published on BendHub.

A matrix carries its dimensions in its type. If two matrices cannot be multiplied, the program is rejected before that multiplication runs. The same idea extends to dimensions that are only known at run time.

a concrete example

Multiplying a 2 × 3 matrix by a 4 × 5 matrix would require the inner dimensions to agree. Here they do not: Bend expects three rows in the second matrix and finds four.

an error caught by the types

A2 × 3
B4 × 5

SOME PROOFS FAIL

expected  Mat<3n, 5n>
observed  Mat<4n, 5n>

The incompatible dimensions from the public example, drawn here. The original checker output is linked below.

public source ↗open full image ↗

the decisions

  • Keep the shape in the type, including symbolic sizes. A reshape requires a proof that it preserves the number of elements.
  • Publish separate packages for arithmetic lemmas, BPE tokenization, list-backed tensors, array-backed tensors, and automatic differentiation.
  • Store matrix rows in bands for parallel work. Each task receives its own part of the weights instead of a copy of the whole matrix.

the results

  • The MNIST demo trains a digit classifier. With the same initial weights and batches, its loss and correct predictions match the PyTorch reference.
  • GPT-2 small generates the same greedy tokens as PyTorch on 11 tested prompts; the reported logit error is within 3.2e-4. The tokenizer matches tiktoken on 79 texts.
  • Package laws are checked again with Bend’s Lean-proved kernel. They cover structural properties such as tokenizer roundtrips and agreement between reverse and forward differentiation.

the limits

  • The numerical results are tested against PyTorch, NumPy and tiktoken. Floating-point arithmetic is not proved equivalent to real arithmetic.
  • The published comparisons include losses: GPT-2 is slower than PyTorch and llama.cpp in the reported CPU runs, and MNIST is slower despite its smaller memory footprint. The README links the figures and release context.
  • The demos show what the packages can do; they do not establish production readiness or performance on other machines.

reference README ↗ · published comparisons ↗