flowchart LR
subgraph data_pipeline[" "]
direction TB
raw_text["Text"] --> examples["Examples"] --> token_ids["Token IDs"]
end
subgraph evaluation[" "]
direction TB
evidence["Evidence"]
checkpoint["Checkpoint"]
end
token_ids --> language_model["Language<br/>model"] --> checkpoint
checkpoint -->|evaluation| evidence
classDef base fill:#ffffff,stroke:#1f2937,stroke-width:2px,color:#111827
classDef model fill:#fed7aa,stroke:#c2410c,stroke-width:3px,color:#111827,font-size:20px,font-weight:bold
classDef state fill:#fef3c7,stroke:#92400e,stroke-width:2px,color:#111827
classDef result fill:#dcfce7,stroke:#166534,stroke-width:2px,color:#111827
class raw_text,examples,token_ids base
class language_model model
class checkpoint state
class evidence result
Corpus and Reproducible Data Systems
machine-learning
language-models
data
Define the mixed language-and-proof corpus, structural splits, and auditable data pipeline consumed by every later chapter.
A language model inherits the boundaries of its corpus. Before implementing a tokenizer or a neural network, make those boundaries explicit: record where each document or generated proof family came from, normalize it by a named rule, split by stable structural identities, and retain enough metadata to reproduce every later claim. This chapter establishes the corpus contract that the remaining chapters consume.
The first examples are deliberately small. They are not miniature pretraining corpora; they are test fixtures in which provenance, duplicate content, leakage, structural identity, and random state can be inspected by hand. The same invariants will survive when the fixtures become the mixed natural-language, mathematical, and verifier-generated proof corpus used by ProofLM.
Data and model lifecycle
The course follows one model through a sequence of transformations:
At each arrow, three questions keep the implementation honest. What information is added? Which behavior is encouraged? Which new failure modes become possible? A manifest adds provenance but cannot establish that a license is valid. A tokenizer adds a discrete representation but can create long sequences or awkward unknown-token behavior. Training adds parameters that fit the objective, but the objective is still only a proxy for useful language behavior.
The division between pretraining, posttraining, and specialized fine-tuning is therefore a division of data and objectives, not a claim that the parameter state is reset between stages. Pretraining learns from next-token continuation on broad text. Posttraining changes interactive behavior through demonstrations, preferences, rewards, or tool traces. Specialization narrows the distribution again. Every stage must be compared with a held-out general suite because later updates can alter earlier capabilities.
Data splits
Let D = \{(x_i, m_i)\}_{i=1}^n be documents paired with metadata m_i, and let \ell_\theta(x) be a loss computed by a model. Training estimates an empirical risk,
\widehat{R}_{\mathrm{train}}(\theta) = \frac{1}{|D_{\mathrm{train}}|} \sum_{x \in D_{\mathrm{train}}} \ell_\theta(x),
while the quantity of interest is performance on a separate distribution P_{\mathrm{eval}}:
R_{\mathrm{eval}}(\theta) = \mathbb{E}_{x \sim P_{\mathrm{eval}}}[\ell_\theta(x)].
A test example copied into training makes the empirical training and evaluation samples dependent. In the extreme case, a model can return a memorized continuation with low loss without learning a rule that transfers. The split is therefore not bookkeeping around the experiment; it determines what the experiment can establish.
A practical leakage predicate operates on stable identities. If h(x) is a canonical content hash, a basic audit asks whether
\{h(x):x\in D_{\mathrm{train}}\} \cap \{h(x):x\in D_{\mathrm{test}}\} = \varnothing.
Document identity and content identity answer different questions. A document-level split prevents chunks from one document crossing the boundary. Hashing additionally catches duplicate documents that were assigned different identifiers.
Dataset manifests
The first fixture stays small enough to inspect by hand, but its reusable invariants now live in projects/proof-lm/. The package supplies immutable document records, canonical normalization and hashing, generated proof examples, independent verification, checked countermodels, structural split assignment, and dataset-manifest construction. The notebook imports those functions so that the later tokenizer and trainer consume the same artifact rather than a parallel notebook-only implementation.
from collections import defaultdict
import json
import re
import numpy as np
from proof_lm.data import (
Document,
build_dataset_manifest,
build_mixed_smoke_corpus,
content_hash,
manifest_record,
normalize_text,
split_examples,
)
from proof_lm.logic import generate_examples, verify_proof
SEED = 17
documents = [
Document(
"d00",
"synthetic",
"course-fixture-v1",
"A manifest records provenance. A split is a contract. Hashes make changes visible.",
),
Document(
"d01",
"synthetic",
"course-fixture-v1",
"A tokenizer maps text to symbols. Shorter sequences reduce compute. Boundaries affect behavior.",
),
# Different surface form, identical canonical content: a duplicate to find.
Document(
"d02",
"synthetic",
"course-fixture-v1",
"A MANIFEST records provenance. A split is a contract. Hashes make changes visible.",
),
Document(
"d03",
"synthetic",
"course-fixture-v1",
"Validation estimates transfer. Test data should stay unseen. Every claim needs a split.",
),
Document(
"d04",
"synthetic",
"course-fixture-v1",
"A checkpoint stores parameters. A seed fixes a trajectory. A log records the budget.",
),
]
# The duplicate report is useful even before a split has been selected.
hash_groups = defaultdict(list)
for document in documents:
hash_groups[content_hash(document.text)].append(document.document_id)
duplicates = [ids for ids in hash_groups.values() if len(ids) > 1]
print("duplicate groups:", duplicates)
print(json.dumps(manifest_record(documents[0], "train"), indent=2, sort_keys=True))
assert duplicates == [["d00", "d02"]]
# The reusable proof generator supplies the verified formal slice of the corpus.
proof_examples = generate_examples(count=12, seed=SEED)
proof_splits = split_examples(proof_examples, seed=SEED)
proof_dataset, proof_manifest = build_dataset_manifest(proof_examples, proof_splits)
positive_examples = [example for example in proof_examples if example.kind == "positive"]
negative_examples = [example for example in proof_examples if example.kind == "negative"]
print("verified positives:", len(positive_examples))
print("controlled negatives:", len(negative_examples))
print("proof manifest:", proof_dataset.dataset_manifest_id)
assert all(verify_proof(example.proof).valid for example in positive_examples)
assert all(not verify_proof(example.proof).valid for example in negative_examples)
assert proof_dataset.total_examples == len(proof_manifest)
# One manifest now joins language, mathematics, and generated proof records.
mixed_dataset, mixed_manifest = build_mixed_smoke_corpus(seed=SEED, proof_count=12)
source_counts = defaultdict(int)
for row in mixed_manifest:
source_counts[row["source_kind"]] += 1
print("mixed manifest:", mixed_dataset.dataset_manifest_id)
print("mixed source counts:", dict(sorted(source_counts.items())))
assert set(source_counts) == {"language", "mathematics", "generated-proof"}
assert mixed_dataset.total_examples == len(mixed_manifest)duplicate groups: [['d00', 'd02']]
{
"characters": 82,
"document_id": "d00",
"provenance": "course-fixture-v1",
"sha256": "92335f11bcab276e009891f2a2f33f70464d6915b352152051c84aca164a2f18",
"size_bytes": 82,
"source": "synthetic",
"split": "train",
"whitespace_tokens": 13
}
verified positives: 12
controlled negatives: 24
proof manifest: dataset-prooflm-smoke-v1
mixed manifest: dataset-prooflm-mixed-smoke-v1
mixed source counts: {'generated-proof': 36, 'language': 2, 'mathematics': 2}The duplicate report catches d00 and d02 even though their raw strings differ. The hash is short enough to scan in a report only because the full SHA-256 value is retained in the manifest; truncation would make collisions easier. A production pipeline would add license, collection time, preprocessing version, and the hash of the exact input artifact.
Identity-based splits
A deterministic split needs two ingredients: a stable unit of assignment and a recorded seed. Assigning chunks independently is tempting because it balances row counts, but it permits near-duplicate context from one document to appear on both sides. Assign complete documents first, then create windows inside each split.
def document_split_ids(documents, seed=SEED, train_fraction=0.6, valid_fraction=0.2):
ids = np.array(sorted(document.document_id for document in documents))
order = np.random.default_rng(seed).permutation(len(ids))
shuffled = ids[order]
n_train = int(train_fraction * len(ids))
n_valid = int(valid_fraction * len(ids))
return {
"train": set(shuffled[:n_train]),
"validation": set(shuffled[n_train:n_train + n_valid]),
"test": set(shuffled[n_train + n_valid:]),
}
def chunks_for(document: Document):
sentences = [part.strip() for part in re.split(r"(?<=[.!?])\s+", document.text) if part.strip()]
return [{"document_id": document.document_id, "chunk_id": i, "text": sentence}
for i, sentence in enumerate(sentences)]
def ids_in(rows):
return {row["document_id"] for row in rows}
doc_splits = document_split_ids(documents)
row_chunks = [chunk for document in documents for chunk in chunks_for(document)]
# A deliberately naive row split: alternating rows guarantees a visible boundary violation.
row_train, row_validation = row_chunks[::2], row_chunks[1::2]
doc_train = [chunk for chunk in row_chunks if chunk["document_id"] in doc_splits["train"]]
doc_validation = [chunk for chunk in row_chunks if chunk["document_id"] in doc_splits["validation"]]
row_overlap = ids_in(row_train) & ids_in(row_validation)
doc_overlap = ids_in(doc_train) & ids_in(doc_validation)
manifest = [
manifest_record(document, next(split for split, ids in doc_splits.items()
if document.document_id in ids))
for document in documents
]
print("document split sizes:", {name: len(ids) for name, ids in doc_splits.items()})
print("naive row split document overlap:", sorted(row_overlap))
print("document split overlap:", sorted(doc_overlap))
print("manifest rows:", len(manifest))
assert row_overlap
assert not doc_overlap
assert sum(len(ids) for ids in doc_splits.values()) == len(documents)document split sizes: {'train': 3, 'validation': 1, 'test': 1}
naive row split document overlap: ['d00', 'd01', 'd02', 'd03', 'd04']
document split overlap: []
manifest rows: 5The row split leaks document identity by construction, while the document split does not. Notice the remaining caveat: d00 and d02 can still land in different document partitions because they have different identifiers. The duplicate report must be applied before assignment, or duplicate groups must be treated as one split unit.
Both split functions are deterministic under a fixed seed; only one keeps every chunk of a document on the same side. Determinism makes a run repeatable, while the boundary decides what the measured loss estimates. The hash-overlap audit in the next section is the check that distinguishes the two.
Contamination and leakage
The most useful audit is one that can fail on purpose. Compare a clean document-level boundary with a contaminated boundary in which one validation string is copied into training. Keep the evaluator and all other settings fixed. If the metric improves only after contamination, the improvement is evidence about leakage, not learning.
For the running fixture, the checks are structural rather than statistical: count shared document IDs and shared canonical hashes. On a real corpus, add near-duplicate search, source-level overlap, temporal overlap, length distributions, language or domain proportions, and manual examples selected from both boundaries.
def hash_overlap(left, right):
left_hashes = {content_hash(row["text"]) for row in left}
right_hashes = {content_hash(row["text"]) for row in right}
return left_hashes & right_hashes
clean_train = [
{"text": "the model predicts the next token"},
{"text": "a checkpoint records the training state"},
]
clean_test = [
{"text": "the evaluator measures held-out behavior"},
{"text": "a split protects the strength of the claim"},
]
contaminated_train = clean_train + [clean_test[0]]
print("clean hash overlap:", len(hash_overlap(clean_train, clean_test)))
print("contaminated hash overlap:", len(hash_overlap(contaminated_train, clean_test)))
assert not hash_overlap(clean_train, clean_test)
assert hash_overlap(contaminated_train, clean_test)clean hash overlap: 0
contaminated hash overlap: 1The contaminated split is not a toy version of a harmless mistake. It changes the estimand: the measured test loss now partly asks whether the pipeline can recognize data it has already seen. A lower number may still be useful for a memorization study, but it cannot be reported as held-out generalization. Keep contaminated fixtures in tests and name them as such.
Data reliability
The manifest fields defined above are what make a later result interpretable. Suppose a later chapter reports that validation loss fell from 2.4 to 1.9. The first question to ask is whether any validation document shares a canonical hash with a training document. If the hashes and split identities were never recorded, the question has no answer, and the 1.9 cannot be classified as a transfer result, a memorization result, or a preprocessing artifact. The split audit is therefore part of the model artifact rather than a one-time check: every later chapter inherits this boundary.
The same reasoning produces the reporting habit used for the rest of the course. Evaluate on three inputs and report the scores side by side: training-like inputs estimate fit, held-out inputs estimate transfer, and shifted inputs estimate dependence on surface features of the training distribution. A large gap between the first two scores is evidence of overfitting or leakage, and the next action is a hash-overlap audit of the boundary rather than an architecture change. A large gap between the last two is evidence of shortcut features, which Chapter 13 makes directly measurable.
Structural proof splits
The package manifest records more than a row count. Each generated example carries a source revision, license, generator version, normalization version, token budget, theorem family, proof shape, depth, variable family, paraphrase template, perturbation, tool schema, and structural key. The audit below verifies that no structural group crosses a boundary and that every positive and negative fixture is represented exactly once.
split_by_id = {}
for split, ids in proof_splits.items():
for example_id in ids:
split_by_id[example_id] = split
keys_by_split = {}
for example in proof_examples:
key = example.structural_key
keys_by_split.setdefault(key, set()).add(split_by_id[example.example_id])
mixed_hash_splits = {}
mixed_structural_splits = {}
for row in mixed_manifest:
split = row["split"]
mixed_hash_splits.setdefault(row["sha256"], set()).add(split)
mixed_structural_splits.setdefault(row["structural_key"], set()).add(split)
split_sizes = {name: len(ids) for name, ids in proof_splits.items()}
mixed_sizes = {
name: part.examples for name, part in mixed_dataset.splits.items()
}
manifest_fields = sorted(proof_manifest[0])
print("proof split sizes:", split_sizes)
print("mixed split sizes:", mixed_sizes)
print("structural groups:", len(keys_by_split))
print("manifest field count:", len(manifest_fields))
print("manifest fields:")
for start in range(0, len(manifest_fields), 4):
print(" ", ", ".join(manifest_fields[start : start + 4]))
assert all(len(split_names) == 1 for split_names in keys_by_split.values())
assert set(split_by_id) == {example.example_id for example in proof_examples}
assert all(
row["source_revision"] == "generated-proof-fixture-v1" for row in proof_manifest
)
assert all(row["generator_version"] == "proof-generator-v1" for row in proof_manifest)
assert all(len(splits) == 1 for splits in mixed_hash_splits.values())
assert all(len(splits) == 1 for splits in mixed_structural_splits.values())
assert sum(mixed_sizes.values()) == mixed_dataset.total_examplesproof split sizes: {'train': 21, 'validation': 7, 'test': 8}
mixed split sizes: {'train': 23, 'validation': 8, 'test': 9}
structural groups: 30
manifest field count: 19
manifest fields:
characters, example_id, generator_version, kind
license, normalization_version, paraphrase_template, perturbation
proof_depth, proof_shape, sha256, source_revision
split, structural_key, theorem_family, token_budget
tool_schema, variable_family, verifiedThe formal fixture has a stronger boundary than the document toy. A structural split assigns every generated theorem family, proof shape, variable family, paraphrase template, perturbation, and tool schema to one partition. Inspect the keys directly before treating the manifest as training data.
Summary
- A language-model experiment is a chain of data and parameter transformations; every arrow introduces a new assumption.
- Empirical risk is only evidence about a separate evaluation distribution when the boundary is meaningful.
- Canonical hashes catch duplicate surface forms; document-level assignment prevents chunk leakage.
- Seeds, manifests, split identities, and preprocessing versions make a result reproducible and auditable.
Chapter 02 turns the clean text boundary into token IDs and attention-ready batches. It keeps the same discipline: define the representation, test its invariants, and measure what changed.
Exercises
Use the exercises to separate a reproducible pipeline from a merely repeatable script. Solutions are hidden in the notebook source and are available through the course tooling when needed.
[P1.1] Split audit
Split audit. Explain why assigning chunks independently can make validation loss optimistic even when the random seed is fixed. Give one invariant for document identity and one for canonical content hashes.
[P1.2] Canonical duplicate groups
Manifest implementation. Complete the starter so it returns the number of canonical duplicate groups in a list of documents. Treat whitespace and case differences as identical.
def duplicate_group_count(texts):
# Return the number of hash groups containing at least two texts.
pass[P1.3]
Source-preserving mixed manifests. build_mixed_smoke_corpus returns one dataset manifest whose rows come from language, mathematics, and generated-proof sources. Implement source_counts(records) so it returns a dictionary keyed by source_kind, then explain why source kind belongs on each row even when all rows share one dataset manifest ID.
def source_counts(records):
# Count rows by their source_kind field.
pass