Skip to content

Add token-id LM training, CUDA defaults, and kernel launch hygiene#11

Open
wadkisson wants to merge 2 commits into
lean-dojo:mainfrom
wadkisson:main
Open

Add token-id LM training, CUDA defaults, and kernel launch hygiene#11
wadkisson wants to merge 2 commits into
lean-dojo:mainfrom
wadkisson:main

Conversation

@wadkisson

Copy link
Copy Markdown
Collaborator

Summary

Three library changes

Part A — Token-id causal LM API

  • Add causalTransformerTokenLmScalarModuleDef for float-encoded token-id inputs
  • Add text helpers: causalLmTokenRows, causalLmTokenFloatVec, causalLmTokenSampleRowsFromTokenArray
  • Add floatVecToNatTensor op (Functional → Ops → TorchLean Functional → Trainer instances)
  • Add verifier stubs in Compile.lean and SpecEval.lean

Enables persistent-module LM training: token windows can change each step without rebuilding the module or one-hot tensors (Adam state stays on one session). Matches PyTorch nn.Embedding + cross_entropy structurally.

Part B — CUDA CLI + inference

  • --cuda auto-enables --fast-kernels (fastKernels := fastKernels || useGpu)
  • Add Options.noGrad; eval1NoGrad sets noGrad := true
  • README: CUDA quickstart no longer requires explicit --fast-kernels

Makes --cuda turn on fast kernels by default and fixes inference so eval1NoGrad runs without recording autograd state.

Part C — Native CUDA robustness

  • Add torchlean_cuda_clear_pending_error and torchlean_cuda_check_launch
  • Use before scalar unary kernel launches and in reduceMean

Clears stale CUDA driver errors before kernel launches so unrelated failures don’t break TorchLean’s native kernels.

wadkisson added 2 commits July 1, 2026 18:14
Token-id causal LM API for persistent-module training; --cuda enables
fast-kernels by default; noGrad for eval1NoGrad; clear stale CUDA errors
before kernel launches.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant