Coppelius.Learner

1module Coppelius.Learner
2
3import Model.Architecture
4import Representation.Schema
5import Accelerator.SM86.Instruction
6
7-- Coppelius keeps the objective beside the model geometry, but learning is a
8-- separate semantic choice.  The shared Representation.Schema owner defines
9-- AdamW; this module only binds that reusable learner to Coppelius.
10family CoppeliusLearningSemantics : Type 0
11constructor CoppeliusLearningSemanticsValue
12field unrestricted coppeliusLearningObjective : (family ModelObjective)
13field unrestricted coppeliusLearningLearner : (family LearnerContract)
14
15end-family
16
17def coppeliusObjectiveIdentity : Bytes =
18  b"exact-vocabulary-cross-entropy"
19
20def coppeliusLearnerIdentity : Bytes =
21  b"adamw"
22
23def coppeliusObjective : (family ModelObjective) =
24  (constructor ModelObjective ModelExactVocabulary)
25
26def coppeliusLearner : (family LearnerContract) =
27  (constructor LearnerContract LearnerAdamW)
28
29def coppeliusLearningSemantics : (family CoppeliusLearningSemantics) =
30  (record
31    CoppeliusLearningSemantics
32    (coppeliusLearningObjective = coppeliusObjective)
33    (coppeliusLearningLearner = coppeliusLearner))
34
35-- AdamW's hyperparameters, exact (numerator, denominator): the plan's
36-- per-step scalars (Coppelius.Build.Graph) are computed from them and
37-- rounded to binary32 once
38def coppeliusLearningRateNumerator : Nat = 1
39def coppeliusLearningRateDenominator : Nat = 10000
40def coppeliusBeta1Numerator : Nat = 9
41def coppeliusBeta1Denominator : Nat = 10
42def coppeliusBeta2Numerator : Nat = 999
43def coppeliusBeta2Denominator : Nat = 1000
44def coppeliusWeightDecayNumerator : Nat = 1
45def coppeliusWeightDecayDenominator : Nat = 10
46def coppeliusEpsilonNumerator : Nat = 1
47def coppeliusEpsilonDenominator : Nat = 100000000
48-- The 16-bit format of every half the plan makes -- the matrices' copies,
49-- the products' operands, the backward's gradients: bfloat16, binary32's
50-- exponent range with an 8-bit significand.  Under binary16 the gradients of
51-- the attention scores lay below its subnormals whatever one static scale
52-- (a scale that lifted them overflowed layer 0), and the upper layers'
53-- queries and keys did not learn; bfloat16 holds them.  The device images
54-- are moved to it together (Coppelius.Build.DeviceImages,
55-- Accelerator.SM86.HalfFormat).
56def coppeliusHalfFormat : (family SM86HalfFormat) =
57  (constructor SM86HalfFormat SM86BFloat16)
58
59def coppeliusHalfFormatIdentity : Bytes =
60  b"bfloat16"
61
62-- loss scaling: the backward runs on the loss times this, and AdamW's
63-- epsilon is scaled by the same factor, so the update is the unscaled
64-- loss's: S m / (S sqrt v + S eps).  bfloat16's range needs none (1): the
65-- factor binary16 needed (8,192) is what its range lacked.
66def coppeliusLossScale : Nat = 1
67-- the first update's step number (bias correction counts from 1)
68def coppeliusFirstStep : Nat = 1