Building a Language Model: From Pretraining to Function Calling

Build one decoder-only language model from random initialization, specialize it for formal proofs, and teach it to use proof tools.

Build ProofLM, a small decoder-only language model, through one continuous and auditable project. The course starts with raw natural-language, mathematical, and generated proof data; trains a causal language model from random initialization; specializes it for formal proof synthesis; and then teaches it to call deterministic proof tools. Deep-learning concepts arrive when the running implementation needs them, and every stage is evaluated against both its intended improvement and regressions in earlier capabilities.

The course is for readers with strong scientific Python skills and undergraduate mathematics. No prior deep-learning experience is assumed. PyTorch tensors, modules, autograd, optimizers, devices, and serialization are introduced directly through the model that the course ultimately trains.

What you will build

The completed course produces one documented checkpoint family rather than a set of unrelated demonstrations:

• a byte-level BPE tokenizer trained on the declared corpus;
• a roughly 54M-parameter causal decoder pretrained from random initialization;
• proof-oriented SFT, DPO, and verifier-guided reinforcement-learning branches;
• a deterministic proof-tool environment with call, no-call, and recovery behavior;
• matched full-fine-tuning and rank-8 LoRA tool-calling branches; and
• a frozen evaluation harness that compares proof validity, tool use, shifted behavior, retention, cost, and concrete failures.

The target is not a general-purpose assistant. ProofLM learns enough natural and mathematical language to accept proof requests, synthesize and repair propositional natural-deduction proofs, find countermodels, and use proof-oriented tools. Each stage is complete only when it connects a derivation, the reusable PyTorch implementation, a controlled experiment, and an evidence record identifying the data, checkpoint, evaluator, compute budget, improvement, and regression.

Read Chapter 00: ProofLM and the evidence contract before beginning the implementation. It defines what “from scratch” means, how the checkpoint lineage branches, which execution profiles are supported, and what counts as a course result.

Learning path

Phase	Chapter	Build and evidence
Orientation	00. ProofLM overview	Fix the model, artifact lineage, compute profiles, data boundary, and evidence standard.
Data and foundations	01. Corpus and data systems	Build manifests, proof-data fixtures, structural splits, and leakage audits.
	02. Tokenization and batching	Train the real tokenizer and freeze packing, masking, and serialization contracts.
	03. PyTorch foundations and baselines	Derive cross-entropy and train n-gram, bigram, and MLP baselines on the smoke corpus.
	04. Decoder-only Transformer	Implement and qualify the trainable ProofLM decoder.
	05. Causal pretraining	Complete the CPU smoke run and canonical CUDA base pretraining.
	06. Optimization and systems	Measure schedules, accumulation, clipping, memory, throughput, and exact recovery.
	07. Checkpoint evaluation	Freeze likelihood, proof, calibration, memorization, and retention suites.
Posttraining and adaptation	08. Proof supervised fine-tuning	Train response-only proof behavior and measure structural transfer.
	09. Preference learning and DPO	Optimize verifier-labeled preferences while controlling length bias and drift.
	10. Verifier-guided reinforcement learning	Optimize checked proof rewards and expose weak-evaluator exploits.
	11. Proof-tool calling	Train typed calls, no-call decisions, result use, and recovery from tool errors.
	12. LoRA and full fine-tuning	Compare matched tool adaptation branches from the same parent checkpoint.
Reliability and capstone	13. Measured failure modes	Populate the reliability taxonomy with checkpoint-family effect sizes and failures.
	14. End-to-end proof-model study	Reproduce the smoke pipeline and compare every frozen branch under one evaluator.

Prerequisites

Tooling:

• Python and comfort reading small packages, tests, and experiment configurations.
• PyTorch for the complete core implementation; NumPy is not a parallel teaching track.
• Git for source identity and checkpoint provenance. The substantial path uses a RunPod account, while the complete smoke path runs locally on CPU.

Assumed knowledge:

• vectors, matrices, derivatives, probability, logarithms, and basic statistics;
• ordinary Python data structures, functions, classes, and iteration; and
• willingness to treat data boundaries and evaluators as part of the mathematical claim rather than as surrounding bookkeeping.

Execution at a glance

Profile	Default environment	Contract
smoke	PyTorch CPU	About 5M parameters and 2M tokens; completes every chapter’s logical path locally using the same schemas as the standard run.
standard	Qualified RunPod CUDA	About 54M parameters and 1B pretraining tokens; owns the canonical checkpoint lineage and published substantial results.
MLX comparison	16 GB M5, optional appendix	Ports only the smoke pretraining path and remains separate from the canonical PyTorch lineage.

The first release keeps all RunPod compute, storage, and transfer under a cumulative $20 ceiling. Hardware is selected from measured sustained throughput and memory headroom, not from advertised peak performance. A learner can complete the full conceptual and artifact path without purchasing remote compute, while inspecting the stored standard-run reports.

Important notes

Reusable computation belongs in projects/proof-lm/; the notebooks introduce, exercise, and interpret that package. Large corpora and checkpoints remain outside Git. Configurations, small fixtures, manifests, hashes, tests, and compact metric reports stay in the repository.

Every reported result identifies the model configuration, tokenizer and dataset manifests, parent and child checkpoint hashes, random seed, optimizer updates, processed tokens or examples, device, wall time, cost when applicable, and evaluator version. A decreasing loss without those records is not a course result.

Content safety, governance, deployment security, and general agent harnesses remain adjacent subjects. This course’s reliability question is narrower: did a declared training signal produce the intended proof behavior under held-out structure, distribution shift, and correction, without silently erasing earlier capabilities?