aprender-train 0.41.0

Training & Optimization library with autograd, LoRA, quantization, and model merging
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

metadata:
  version: "1.0.0"
  created: "2026-03-19"
  author: "PAIML Engineering"
  description: "LoRA/QLoRA weight decomposition contracts"
  references:
    - "Hu et al. (2021) LoRA: Low-Rank Adaptation of Large Language Models"

equations:
  lora_decomposition:
    formula: "W_adapted = W_frozen + (α/r) * B @ A"
    domain: "W ∈ ℝ^(d×k), A ∈ ℝ^(r×k), B ∈ ℝ^(d×r), r << min(d,k)"
    preconditions:
      - "r > 0"
      - "r <= d.min(k)"
      - "alpha > 0.0"
      - "a.len() == r * k"
      - "b.len() == d * r"
      - "w_frozen.len() == d * k"
    postconditions:
      - "ret.len() == d * k"
      - "ret.iter().all(|v| v.is_finite())"
      - "w_frozen_after == w_frozen_before"
    invariants:
      - "W_frozen unchanged during training"
      - "rank(B @ A) ≤ r"

proof_obligations:
  - type: invariant
    property: "Frozen weights unchanged"
    formal: "W_frozen at step t == W_frozen at step 0"
    applies_to: all
  - type: bound
    property: "LoRA rank preserved"
    formal: "rank(B @ A) ≤ r"
    applies_to: all

falsification_tests:
  - id: FALSIFY-LORA-001
    rule: "Frozen weights"
    prediction: "Base model weights identical before and after training"
    test: "Compare W_frozen checksum at step 0 and step N"
    if_fails: "Gradient leaking into frozen weights"
  - id: FALSIFY-LORA-002
    rule: "Rank bound"
    prediction: "Adapted weight change has rank ≤ r"
    test: "SVD of (W_adapted - W_frozen), check singular values"
    if_fails: "Alpha scaling or merge error"

kani_harnesses:
  - id: lora-kani-001
    obligation: "Frozen weights unchanged"
    bound: 4
    strategy: bounded_int