Large Language Models for Code and Proof

Contents

• Introduction and overview
• 0. Review: language models, gradients and formal languages
• 1. Transformers, attention and the KV cache
• 2. Tokenization for text and code
• 3. Pretraining code models and scaling laws
• 4. Fine-tuning and low-rank adaptation
• 5. Decoding and evaluating generated code
• 6. Structured generation
• 7. Retrieval-augmented generation for code
• 8. Formal verification and automated theorem proving
• 9. Execution feedback, repair and software-engineering agents
• 10. Research directions and open problems
• Exercises
• Projects and assessment
• References

Introduction and overview

Audience: a student who has trained a transformer in PyTorch and wants to understand what changes when the model writes programs and formal proofs, whose output is executed or checked rather than read.

Empirical first: sample 100 programs from a code model for one task. At low temperature they are nearly identical; at a higher temperature, at least one of them is far more likely to pass the hidden tests. Chen et al. (2021) report best temperatures of about 0.2 for pass@1 and 0.8 for pass@100 on their benchmark.

A compiler, a test suite or a proof assistant then accepts or rejects each sample, with no partial credit. This course explains how such models are built, adapted, decoded, constrained, evaluated and plugged into verifiers.

The course goes from the transformer and its tokenizer to the research frontier of program synthesis and machine-checked mathematics. It builds on Deep Learning, Advanced Learning for Text and Graph Data (ALTEGRAD), Theoretical Foundations of Deep Learning and Foundations of Large Language Models. It shares tools with Training and Deploying Large-Scale Models and Algorithms for Speech and Natural Language Processing.

What you will be able to do

• Write the equations of causal multi-head attention and prove that a KV cache returns exactly the outputs of a full recomputation.
• Size the KV cache of a code model and explain how grouped-query attention reduces it.
• Train a byte-level BPE tokenizer on source code and measure its compression on held-out files.
• Derive the compute-optimal split between model size and data from a parametric scaling law.
• Fine-tune a frozen model with LoRA, count its trainable parameters and merge the adapter.
• Compare greedy, beam, temperature, top-k and nucleus decoding, and choose a temperature for pass@1 or pass@k.
• Compute the unbiased pass@k estimator and prove that the plug-in estimator is biased.
• Constrain generation with a finite automaton or a grammar, and quantify the distortion that token masking introduces.
• Build and evaluate a retriever (BM25, dense) for code and documentation.
• Analyse sample-and-test, self-repair and agent loops under a fixed budget of model calls.
• Formulate theorem proving as a search problem over tactic states and run a best-first prover whose output is checked.
• Check candidate loop invariants against the verification conditions of Hoare logic.

Official objectives and syllabus (2026–2027)

The course description on master-mva.com starts from the observation that recent advances in large language models (LLMs) have enabled remarkable progress in program synthesis and code generation. It explores the foundations and methods of modern neural code generation, with a focus on Transformer-based architectures and LLM techniques.

The description sets two objectives. The first is a deep understanding of the core techniques for training and fine-tuning neural models for code generation, including inference strategies and evaluation metrics specific to code. The second is an introduction to current research in neural program synthesis, with applications in software engineering, reasoning and formal verification.

By the end of the course, students are expected to gain both theoretical insights and hands-on experience in building and evaluating neural models for code generation. The description refers to the course page https://llm.labri.fr/ for the organisation of the sessions; the course can accommodate up to 90 students and is not open to external auditors.

Extensions beyond the syllabus: the review ch. 0, near-duplicate detection and fill-in-the-middle training in ch. 3, and the self-study research ch. 10.

Where this course fits in the programme

Official prerequisites: mastery of Python and PyTorch, and basic knowledge of linear algebra and optimization. The course description adds that any one of three MVA courses is enough to be up to speed: Deep Learning, Advanced Learning for Text and Graph Data, and Theoretical Foundations of Deep Learning. The instructors are Marc Lelarge (INRIA & ENS) and Guillaume Baudart (INRIA – Irif), as listed on master-mva.com.

• Refreshers — Scientific Python, NumPy and PyTorch for the code, Linear Algebra, Analysis and Optimization for ch. 1, 3 and 4, and Probability and Statistics for ch. 0, 5 and 6.
• First-semester courses that prepare it — the three named by the description, Deep Learning, ALTEGRAD and Theoretical Foundations of Deep Learning; also Foundations of Large Language Models and Fundamentals of Reproducible Research and Free Software.
• Related second-semester courses — Training and Deploying Large-Scale Models (serving, LoRA, post-training at scale), Algorithms for Speech and Natural Language Processing (tokenization, decoding), Reinforcement Learning (learning from test rewards, ch. 9) and Responsible Machine Learning.
• After the course — the Research Internship, for which ch. 10 lists open questions.

Course outline

• Review: language models, gradients and formal languages — the chain rule of probability, cross-entropy and perplexity, the softmax gradient, automata and grammars.
• Transformers, attention and the KV cache — attention and its invariances, the decoder-only block, rotary positions, the KV cache and its memory.
• Tokenization for text and code — byte-level BPE, unigram tokenization, and what is special about source code.
• Pretraining code models and scaling laws — code corpora and deduplication, fill-in-the-middle, compute-optimal scaling.
• Fine-tuning and low-rank adaptation — supervised fine-tuning, LoRA and its analysis, instruction data for code.
• Decoding and evaluating generated code — search and sampling, pass@k and its estimator, choosing among samples.
• Structured generation — masking with automata and grammars, and the distortion it creates.
• Retrieval-augmented generation for code — retrievers, RAG models, retrieval in repositories.
• Formal verification and automated theorem proving — proof assistants, proof search, autoformalization, invariants.
• Execution feedback, repair and software-engineering agents — filtering with tests, self-repair, agents, learning from execution (self-study).
• Research directions and open problems — verifiable rewards, test-time compute, benchmarks, formal mathematics (self-study).

Session plan

24 h in class = 8 sessions of 3 h.

The volume is the Université Paris-Saclay programme table (lectures 12 h, tutorials 12 h). master-mva.com refers to the course page for the organisation of the sessions; the split below is a proposal, with about 1.5 h of lecture and 1.5 h of tutorial in each session.

Level 1 = foundations, 2 = core results and algorithms, 3 = advanced or research-level material; the level never decreases.

Self-study, outside the 24 h (about 7 h in total): ch. 9 Execution feedback, repair and software-engineering agents (≈ 3 h, with Ex. 14) · ch. 10 Research directions and open problems (≈ 3 h, with Ex. 15 and 17) · the written-exam proposal of Projects and assessment as a self-test (≈ 1 h).

How to study this module

• Read ch. 0 first even if language models are familiar: the softmax gradient, the automata and the grammars it fixes are used without warning in ch. 5 and 6.
• Run every code block. They need NumPy, SciPy and PyTorch on a CPU, use fixed seeds or the Python standard library as data, and finish in a few seconds.
• After each session, solve the exercises of the Practice column; the ★★★ exercises are good starting points for a project.
• Read ch. 9 after session 8: it applies the generate-and-check pattern of ch. 8 to tests, repairs and agents, with the tools of ch. 5.
• Keep a small open code model at hand (a free GPU tier is enough for models up to about 1.5 billion parameters) to try every decoding, constraining and retrieval method on real samples.
• Follow the course page announced on master-mva.com, https://llm.labri.fr/, for the organisation of the sessions; the homework and exam subjects on this page are proposals, not the official ones.

0. Review: language models, gradients and formal languages

Every later chapter manipulates a probability distribution over token sequences, a softmax over a vocabulary, and a formal language that the output must belong to. This chapter fixes these three M1-level tools and the notation of the page.

0.1 Autoregressive language models

With base-2 logarithms the loss is in bits per token. A perplexity of 13 means the model is, on average, as uncertain as a uniform choice among 13 tokens.

Minimizing the next-token loss on a corpus therefore pushes the model towards the conditional distributions of the data. The loss can never go below the entropy of the source, which is why scaling laws (ch. 3) have an irreducible term.

import inspect, json.decoder, math
from collections import Counter

text = inspect.getsource(json.decoder)          # real Python code, shipped with Python
split = int(0.8 * len(text))
train, test = text[:split], text[split:]
V = len(set(text))

pairs = Counter(zip(train, train[1:]))           # bigram counts
first = Counter(train[:-1])

def logp(a, b):                                   # add-one smoothing
    return math.log2((pairs[(a, b)] + 1) / (first[a] + V))

nll = -sum(logp(a, b) for a, b in zip(test, test[1:])) / (len(test) - 1)
print(f"{V} distinct characters, uniform model: {math.log2(V):.2f} bits/char")
print(f"bigram model: {nll:.2f} bits/char, perplexity {2 ** nll:.1f}")

0.2 Softmax, temperature and the gradient

As \tau \to 0, the distribution concentrates on the largest logit when it is unique; as \tau \to \infty, it tends to the uniform distribution. Adding the same constant to every logit changes nothing.

Each training step therefore raises the logit of the observed token and lowers every other logit in proportion to its probability. The gradient vanishes only when the model puts all its mass on the observed token.

0.3 Automata and grammars

Programs, JSON documents and proofs must belong to a formal language. Two classes of languages are used in ch. 2 and ch. 6.

Brackets in code and nested JSON objects therefore need grammars, and checking a prefix needs a stack: this is the difference between the two constraint engines of ch. 6.

1. Transformers, attention and the KV cache

Almost every code and proof model in use is a decoder-only transformer. This chapter defines attention, explains how the model knows the order of the tokens, and shows why generation reuses past keys and values instead of recomputing them.

1.1 Scaled dot-product attention

In an unmasked layer without position information, a - b and b - a would get the same multiset of representations. Positions must therefore be injected, which is the role of Definition 1.6.

Dividing the scores by \sqrt{d_k} keeps their variance near 1 at initialization. Otherwise, with d_k = 128 the scores would have a standard deviation of about 11, the softmax would be almost one-hot, and its gradient (Proposition 0.5) almost zero.

1.2 The decoder-only block and positions

A pattern such as “the closing bracket three tokens later” is thus scored identically at every position of a file.

1.3 The KV cache

Generation produces one token per forward pass. A naive loop would recompute the whole prefix at every step.

import torch
torch.manual_seed(0); torch.set_num_threads(1)
d, T = 16, 10
Wq, Wk, Wv = (torch.randn(d, d) / d ** 0.5 for _ in range(3))
X = torch.randn(T, d)                       # embeddings of T tokens

def causal_attention(X):                    # full recomputation, O(T^2 d)
    Q, K, V = X @ Wq, X @ Wk, X @ Wv
    S = Q @ K.T / d ** 0.5
    mask = torch.triu(torch.ones(len(X), len(X), dtype=torch.bool), 1)
    return torch.softmax(S.masked_fill(mask, float("-inf")), dim=-1) @ V

K_cache, V_cache, outs = [], [], []
for t in range(T):                          # one token at a time, O(t d) per step
    x = X[t]
    K_cache.append(x @ Wk); V_cache.append(x @ Wv)
    K, V = torch.stack(K_cache), torch.stack(V_cache)
    a = torch.softmax(K @ (x @ Wq) / d ** 0.5, dim=0)
    outs.append(a @ V)

err = (torch.stack(outs) - causal_attention(X)).abs().max().item()
print(f"max difference cached vs full: {err:.1e}")    # 6.0e-07: rounding only

1.4 Grouped-query attention and memory-bound decoding

Each decoding step reads all the weights and the whole cache to produce one token per sequence, so decoding is limited by memory bandwidth, not arithmetic. Larger batches, smaller caches and fewer bytes per number are the remedies; serving is studied in Training and Deploying Large-Scale Models.

2. Tokenization for text and code

A model never sees characters: it sees integers from a fixed vocabulary. This chapter explains how that vocabulary is learnt, why its choice changes the cost and the behaviour of a code model, and where tokens and syntax disagree.

2.1 What a tokenizer must do

Characters give short vocabularies but long sequences; whole words give short sequences but an open vocabulary with unknown words. Since attention costs grow with the square of the length (Proposition 1.9), every factor gained in compression is a large saving.

Unicode text is first encoded in UTF-8, where each code point takes 1 to 4 bytes. Starting from the 256 byte values guarantees that every string, in any language or programming language, can be encoded.

2.2 Byte-pair encoding

The idea comes from a compression algorithm of Gage (1994); GPT-2 (Radford et al., 2019) popularized the byte-level version.

Each step makes the locally best choice, and BPE need not minimize the final length over all vocabularies of the same size. It is a greedy heuristic, and the merges learnt on one corpus can transfer poorly to another.

import inspect, json.decoder, json.encoder
from collections import Counter

def merge(ids, pair, new_id):                # replace left to right, no overlaps
    out, i = [], 0
    while i < len(ids):
        if i + 1 < len(ids) and (ids[i], ids[i + 1]) == pair:
            out.append(new_id); i += 2
        else:
            out.append(ids[i]); i += 1
    return out

def train_bpe(data: bytes, n_merges: int):
    ids, merges = list(data), {}
    for new_id in range(256, 256 + n_merges):
        pair = Counter(zip(ids, ids[1:])).most_common(1)[0][0]
        merges[pair] = new_id
        ids = merge(ids, pair, new_id)
    return merges

def encode(data: bytes, merges):             # apply the merges in the order learnt
    ids = list(data)
    for pair, new_id in merges.items():
        ids = merge(ids, pair, new_id)
    return ids

def show(t, merges):
    inv = {v: k for k, v in merges.items()}
    return bytes([t]) if t < 256 else show(inv[t][0], merges) + show(inv[t][1], merges)

train = inspect.getsource(json.decoder).encode()
test = inspect.getsource(json.encoder).encode()
for n in (0, 50, 200, 500):
    merges = train_bpe(train, n)
    print(f"{n:3d} merges: {len(train) / len(encode(train, merges)):.2f} bytes/token on "
          f"json.decoder, {len(test) / len(encode(test, merges)):.2f} on json.encoder")
print([show(t, merges).decode() for t in list(merges.values())[:10]])

2.3 Unigram tokenization and SentencePiece

SentencePiece (Kudo and Richardson, 2018) implements BPE and unigram tokenization on raw text, with the space treated as an ordinary symbol, so that decoding is exact.

2.4 What is special about code

• Whitespace. Indentation is syntax in Python, and runs of spaces are frequent. Chen et al. (2021) added tokens for whitespace runs to the GPT-3 tokenizer and report about 30 % fewer tokens for code.
• Identifiers. Names such as parse_json_file or parseJsonFile are split into frequent pieces; a split that respects the word boundaries helps the model reuse what it knows about each word.
• Numbers. LLaMA (Touvron et al., 2023) splits every number into single digits, so that all numbers share a small and regular set of tokens.
• Boundaries. A token may straddle a syntactic boundary, for example ): or \n return. Constraints written at the level of characters must then be translated to tokens (ch. 6).

The model sees only canonical tokenizations during training, so most terms of the sum are tiny. A prompt that ends in the middle of a canonical token forces a non-canonical continuation.

3. Pretraining code models and scaling laws

A code model is first pretrained on a large corpus of source code and text. This chapter covers the three decisions made before training starts: which data to keep, which objective to train on, and how to split a compute budget between model size and data.

3.1 Code corpora and near-duplicates

Public code corpora are built from software repositories, filtered by licence and file type. The Stack (Kocetkov et al., 2022) gathers 3.1 TB of permissively licensed source code in 30 programming languages.

Repositories copy files, forks and generated code massively. Duplicates waste compute, encourage memorization, and inflate benchmark scores when test problems leak into the training data (Allamanis, 2019; Lee et al., 2022).

With k independent hashes, the fraction of agreements estimates J with variance J(1 - J)/k. Locality-sensitive hashing groups the k values into bands, so that only pairs agreeing on a whole band are compared, and near-duplicates are found without comparing all pairs of files.

3.2 Training objectives: left-to-right and fill-in-the-middle

Causal language modelling (Definition 0.1) trains the model to continue a file. An editor, however, needs to insert code between a prefix and a suffix, for example the body of a function whose callers are already written.

The sentinel tokens make the transformation invertible, so no information is lost; by the chain rule, the model learns the distribution of the middle given both sides. Bavarian et al. (2022) report that FIM rates up to 90 % leave the left-to-right perplexity essentially unchanged, a property they call FIM for free.

import random

def fim(doc: str, rng: random.Random, rate=0.5):
    """Fill-in-the-middle transformation, prefix-suffix-middle order."""
    if rng.random() > rate:
        return doc                                   # keep some plain left-to-right data
    i, j = sorted(rng.sample(range(len(doc) + 1), 2))
    prefix, middle, suffix = doc[:i], doc[i:j], doc[j:]
    return f"<PRE>{prefix}<SUF>{suffix}<MID>{middle}<EOT>"

def undo(sample: str) -> str:                        # sentinels make it invertible
    if not sample.startswith("<PRE>"):
        return sample
    prefix, rest = sample[5:].split("<SUF>")
    suffix, middle = rest.split("<MID>")
    return prefix + middle.removesuffix("<EOT>") + suffix

doc = "def area(r):\n    return 3.14159 * r ** 2\n"
s = fim(doc, random.Random(3), rate=1.0)
print(repr(s))
print(undo(s) == doc)                                 # True

3.3 Scaling laws and the compute-optimal model

import numpy as np
from scipy.optimize import curve_fit

E, A, B, a, b = 1.69, 406.4, 410.7, 0.34, 0.28       # fit of Hoffmann et al. (2022)
def loss(N, D):
    return E + A / N ** a + B / D ** b

def optimum(C):                                       # Theorem 3.7
    G = (a * A / (b * B)) ** (1 / (a + b))
    N = G * (C / 6) ** (b / (a + b))
    return N, C / (6 * N)

for C in (1e21, 1e23):
    N, D = optimum(C)
    grid = np.logspace(np.log10(N) - 1, np.log10(N) + 1, 2001)
    N_num = grid[np.argmin(loss(grid, C / (6 * grid)))]   # brute-force check
    print(f"C = {C:.0e}: N* = {N:.2e} (grid {N_num:.2e}), D* = {D:.2e}, loss {loss(N, D):.3f}")

rng = np.random.default_rng(0)                        # noisy synthetic runs
N = rng.uniform(7, 10, 40); D = rng.uniform(9, 12, 40)        # log10 of the sizes
L = loss(10 ** N, 10 ** D) + 0.01 * rng.standard_normal(40)
f = lambda X, E, A, B, a, b: E + A / 10 ** (a * X[0]) + B / 10 ** (b * X[1])
p, _ = curve_fit(f, (N, D), L, p0=(2, 300, 300, 0.3, 0.3), maxfev=20000)
print("fitted alpha = %.3f, beta = %.3f, E = %.2f" % (p[3], p[4], p[0]))

Kaplan et al. (2020) had recommended growing the model much faster than the data. Hoffmann et al. (2022) point to the learning-rate schedule, which Kaplan et al. did not adapt to the length of each run, as one cause of the difference.

3.4 When data run out

Public code is finite, and a large code model can see all of it. Muennighoff et al. (2023) fit scaling laws with repeated data: up to about 4 epochs, repeated tokens are worth almost as much as new ones, and their value then decays quickly. They also find that filling up to half of a natural-language budget with code costs little; symmetrically, code models are trained on a mix of code, natural language and mathematics.

The compute-optimal model is not the cheapest to serve. A model used for billions of completions is better trained longer and kept smaller, beyond the Chinchilla ratio, a trade-off studied in Exercise 17 and ch. 10.

4. Fine-tuning and low-rank adaptation

A pretrained model continues files; a useful assistant follows instructions, and a specialized one masters a library, a language or a proof assistant. Fine-tuning adapts the model on a small data set, and low-rank adaptation does it while training a tiny fraction of the parameters.

4.1 Supervised fine-tuning

Full fine-tuning updates all N parameters and needs their gradients and optimizer states: with Adam in mixed precision, about 16 bytes per parameter, 112 GB for a 7-billion-parameter model. It can also degrade abilities that the small data set does not exercise.

4.2 Low-rank adaptation

How much can a rank-r update express? The answer is given by the singular value decomposition.

LoRA works when the useful update has a fast-decaying spectrum. Aghajanyan et al. (2021) measured that fine-tuning succeeds within random subspaces of surprisingly low dimension, which motivated the low-rank hypothesis.

import torch
torch.manual_seed(0); torch.set_num_threads(1)              # tiny tensors: one thread
d, k, r, alpha = 64, 64, 4, 4.0

class LoRALinear(torch.nn.Module):
    def __init__(self, W0):
        super().__init__()
        self.W0 = W0                                        # frozen, not a Parameter
        self.A = torch.nn.Parameter(torch.randn(r, W0.shape[1]) / W0.shape[1] ** 0.5)
        self.B = torch.nn.Parameter(torch.zeros(W0.shape[0], r))
    def forward(self, x):
        return x @ self.W0.T + (alpha / r) * (x @ self.A.T) @ self.B.T

W0 = torch.randn(d, k) / k ** 0.5                           # "pretrained" weight
delta = torch.randn(d, 2) @ torch.randn(2, k) / k           # the task needs a rank-2 change
X = torch.randn(512, k); Y = X @ (W0 + delta).T

layer = LoRALinear(W0)
print("output unchanged at init:", torch.allclose(layer(X), X @ W0.T))
opt = torch.optim.Adam(layer.parameters(), lr=1e-2)
for step in range(500):
    opt.zero_grad()
    loss = ((layer(X) - Y) ** 2).mean()
    loss.backward(); opt.step()
merged = W0 + (alpha / r) * layer.B.detach() @ layer.A.detach()
print(f"trainable: {r * (d + k)} instead of {d * k}; final loss {loss.item():.1e}")
print(f"relative error of the merged weight: {((merged - W0 - delta).norm() / delta.norm()).item():.1e}")

4.3 QLoRA and other parameter-efficient methods

QLoRA (Dettmers et al., 2023) stores the frozen weights in 4 bits and trains LoRA adapters in 16 bits on top of them; it fine-tunes a 65-billion-parameter model on a single 48 GB GPU. Earlier parameter-efficient methods insert small bottleneck layers, called adapters (Houlsby et al., 2019), or learn continuous prefixes prepended to the keys and values of every layer (Li and Liang, 2021).

4.4 Instruction data for code

Instruction pairs for code are expensive to write by hand, so most are generated by models. Self-Instruct (Wang et al., 2023) bootstraps tasks from a few seeds. Evol-Instruct, used for WizardCoder (Luo et al., 2024), rewrites tasks into harder ones. OSS-Instruct, used for Magicoder (Wei et al., 2024), starts from real open-source snippets.

Generated answers can be wrong. Code has an advantage over text here: candidate answers can be run against tests and filtered before training, the idea that ch. 9 turns into a learning loop.

5. Decoding and evaluating generated code

The same model can be an excellent or a poor programmer depending on how its outputs are chosen. This chapter compares search and sampling, defines the execution-based metric pass@k with its unbiased estimator, and explains why the best temperature depends on k.

5.1 Search: greedy and beam decoding

In code, greedy decoding is nevertheless a strong baseline for pass@1, because next-token distributions are often sharply peaked.

5.2 Sampling: temperature, top-k and nucleus

Truncation removes the long tail of individually unlikely tokens, which together carry much probability and produce incoherent text. Temperature controls the diversity of what remains.

5.3 Execution-based evaluation and pass@k

Text metrics such as BLEU (Papineni et al., 2002) compare tokens with a reference, but two programs can differ in every token and behave identically, or differ in one character and fail. Code is therefore evaluated by running it.

HumanEval (Chen et al., 2021) contains 164 hand-written Python problems, each with a signature, a docstring and unit tests. MBPP (Austin et al., 2021) contains 974 short crowd-sourced problems.

import numpy as np
from math import comb

def pass_at_k(n, c, k):                     # unbiased estimator (Theorem 5.6)
    if n - c < k:
        return 1.0
    return 1.0 - np.prod(1.0 - k / np.arange(n - c + 1, n + 1))

print(pass_at_k(200, 13, 1), pass_at_k(200, 13, 10), pass_at_k(200, 13, 100))
print("check with binomials:", 1 - comb(187, 10) / comb(200, 10))

rng = np.random.default_rng(0)              # bias of the plug-in estimator
p, n, k = 0.05, 20, 10
c = rng.binomial(n, p, size=200_000)
print(f"true pass@{k} = {1 - (1 - p) ** k:.4f}")
print(f"unbiased estimator: {np.mean([pass_at_k(n, ci, k) for ci in c]):.4f}")
print(f"plug-in estimator:  {np.mean(1 - (1 - c / n) ** k):.4f}")

5.4 Temperature and k

For a single problem, pass@k grows with p, so the temperature that maximizes p maximizes every pass@k. Over a benchmark, the problems differ: on some, the correct program is the mode; on others, it is a less probable sample that a cold model never draws.

A low temperature maximizes the average of p, pass@1. A higher temperature spreads the mass, lowers p on easy problems, where 1 - (1-p)^{100} stays close to 1 anyway, and makes the correct program reachable on hard ones. Chen et al. (2021) found optimal temperatures of about 0.2 for pass@1 and 0.8 for pass@100.

import numpy as np
rng = np.random.default_rng(1)
P, M = 500, 1000                                # problems, candidate programs per problem
z = rng.normal(0.0, 1.0, size=(P, M))           # model logits of the candidates
z[:, 0] = z.max(1) + rng.normal(-1.5, 1.5, P)   # candidate 0 is correct, sometimes the mode

for tau in (0.1, 0.2, 0.4, 0.6, 0.8, 1.0):
    w = np.exp(z / tau - (z / tau).max(1, keepdims=True))
    p = w[:, 0] / w.sum(1)                      # probability of sampling the correct one
    print(f"tau = {tau:.1f}: pass@1 = {p.mean():.3f}, pass@100 = {(1 - (1 - p) ** 100).mean():.3f}")

5.5 Choosing among samples

A user wants one answer, not k. Selection methods turn many samples into few submissions:

• Ranking by likelihood. Chen et al. (2021) found that choosing the sample with the highest mean token log-probability beats a random choice.
• Filtering by tests. Samples that fail the examples of the problem statement are discarded. AlphaCode (Li et al., 2022) generated very large numbers of programs per competitive programming problem, filtered them this way, and clustered the survivors by their behaviour on generated inputs before submitting 10.
• Voting. Samples that produce the same outputs are grouped and the largest group wins, the code analogue of self-consistency (Wang et al., 2023).

The metric n@k counts a problem as solved when one of n submissions, selected from k samples, is correct. Filtering is studied as a probabilistic procedure in ch. 9.

6. Structured generation

A program that does not parse, a JSON object with a missing brace or a SQL query with a stray token is useless, however likely it was. Structured generation forbids such outputs during decoding. This chapter shows how to do it efficiently with automata and grammars, and proves that the naive method changes the distribution it samples from.

6.1 Constrained decoding

Termination is not guaranteed: a model may keep extending a viable prefix forever. A maximum length is handled by requiring that L be reachable within the remaining budget, as in Code 6.7.

6.2 Regular constraints

Many formats are regular: numbers, identifiers, dates, and JSON objects with a fixed schema and bounded nesting. For a DFA, a state is live if an accepting state can be reached from it, and a prefix is viable exactly when it leads to a live state.

The index is computed once per constraint, not once per step. Because the automaton reads characters, tokens such as ": or ), that straddle syntactic boundaries are handled correctly.

6.3 Grammar constraints

Programming languages need at least context-free grammars (Proposition 0.8). The viable-prefix test then needs a parser that works on prefixes.

PICARD (Scholak et al., 2021) rejects inadmissible SQL tokens with an incremental parser; Synchromesh (Poesia et al., 2022) constrains generation with completion engines; Geng et al. (2023) apply grammar-constrained decoding to structured prediction without fine-tuning.

6.4 Masking distorts the distribution

What should constrained decoding sample? The natural target is the model’s distribution conditioned on validity, p(y \mid y \in L) = p(y)\, \mathbb{1}[y \in L] / p(L).

import itertools
import numpy as np

def step(q, ch):                       # DFA of -?1[01]*: 0 start, 1 after '-', 2 accept
    if q in (0, 1) and ch == "1": return 2
    if q == 0 and ch == "-": return 1
    if q == 2 and ch in "01": return 2
    return None                        # dead state

def run(q, token):
    for ch in token:
        q = None if q is None else step(q, ch)
    return q

tokens = ["0", "1", "-", "10", "01", "-1", "<eos>"]
EOS, T = len(tokens) - 1, 3            # at most 3 tokens, then <eos> is forced
rng = np.random.default_rng(2)
logits = rng.normal(0, 1.5, size=(len(tokens) + 1, len(tokens)))   # last row: <bos>
def p_next(prev):
    e = np.exp(logits[prev]); return e / e.sum()

def viable(q, m):                      # can q reach acceptance within m more tokens?
    return q == 2 or (m > 0 and any(run(q, t) is not None and viable(run(q, t), m - 1)
                                    for t in tokens[:-1]))

def allowed(q, m):                     # the mask of constrained decoding
    mask = [run(q, t) is not None and viable(run(q, t), m - 1) for t in tokens[:-1]]
    return np.array(mask + [q == 2])

exact, local = {}, {}
for n in range(1, T + 1):
    for seq in itertools.product(range(EOS), repeat=n):
        prev, q, p, ql = -1, 0, 1.0, 1.0
        for i, t in enumerate(seq + (EOS,)):
            probs = p_next(prev) if i < T else np.eye(len(tokens))[EOS]
            m = probs * allowed(q, T - i) if i < T else probs
            p, ql = p * probs[t], ql * (m[t] / m.sum() if m.sum() > 0 else 0.0)
            if t != EOS: q = run(q, tokens[t])
            prev = t
        if q == 2:
            exact[seq], local[seq] = p, ql

Z = sum(exact.values())
print(f"P(unconstrained sample is valid) = {Z:.3f}")
print(f"total variation: {0.5 * sum(abs(exact[s] / Z - local[s]) for s in exact):.3f}")
for s in sorted(exact, key=lambda s: -exact[s])[:4]:
    print("|".join(tokens[t] for t in s).ljust(8), f"p(.|L) = {exact[s] / Z:.3f}  masked = {local[s]:.3f}")

Sampling from the exact conditional is as hard as computing w, a sum over all continuations. Sequential Monte Carlo (Lew et al., 2023) corrects the distortion with importance weights over many particles, and grammar-aligned decoding (Park et al., 2024) learns estimates of w from samples; Exercise 15 builds the simplest such correction.

7. Retrieval-augmented generation for code

A model knows only what was in its training data, up to a cut-off date. Private repositories, new library versions and project conventions are missing. Retrieval-augmented generation (RAG) fetches relevant documents at inference time and puts them in the context. This chapter covers retrievers, the probabilistic RAG model and the specifics of code.

7.1 Retrievers

Rare words weigh more, repeated words saturate, and long chunks are penalized. Sparse scores need exact word matches, so a query about a “checksum” misses a function documented as a “hash”.

Approximate nearest-neighbour indices therefore scale dense retrieval to millions of chunks.

import math, re
from collections import Counter

corpus = {
    "read_json":   "def read_json(path): load a JSON file and return a dict",
    "write_csv":   "def write_csv(rows, path): write rows to a CSV file",
    "parse_date":  "def parse_date(s): parse an ISO date string into a datetime",
    "http_get":    "def http_get(url, timeout): send a GET request and return the body",
    "retry":       "def retry(fn, attempts): call fn again until it succeeds",
    "lru_cache":   "def lru_cache(maxsize): memoize a function, evicting the least recently used",
    "sha256_file": "def sha256_file(path): hash a file with SHA-256 in chunks",
    "flatten":     "def flatten(nested): turn a list of lists into a flat list",
    "chunked":     "def chunked(xs, n): split a list into chunks of size n",
    "slugify":     "def slugify(title): lowercase a title and replace spaces by hyphens",
}
queries = {"how do I load a json config file": "read_json",
           "split list into batches of fixed size": "chunked",
           "compute the checksum of a large file": "sha256_file",
           "download a web page with a timeout": "http_get",
           "cache results of an expensive function": "lru_cache"}

def tok(s):                                   # split snake_case identifiers, lowercase
    return re.findall(r"[a-z0-9]+", s.lower().replace("_", " "))

docs = {k: tok(v) for k, v in corpus.items()}
M, avgdl = len(docs), sum(map(len, docs.values())) / len(docs)
df = Counter(w for d in docs.values() for w in set(d))

def bm25(query, doc, k1=1.2, b=0.75):         # Definition 7.2
    tf, s = Counter(doc), 0.0
    for w in tok(query):
        if w in tf:
            idf = math.log(1 + (M - df[w] + 0.5) / (df[w] + 0.5))
            s += idf * tf[w] * (k1 + 1) / (tf[w] + k1 * (1 - b + b * len(doc) / avgdl))
    return s

rr = []
for q, gold in queries.items():
    ranking = sorted(docs, key=lambda d: -bm25(q, docs[d]))
    rr.append(1 / (ranking.index(gold) + 1))
    print(f"{q[:38]:38s} -> {ranking[:2]}")
print(f"recall@1 = {sum(r == 1 for r in rr) / len(rr):.1f}, MRR = {sum(rr) / len(rr):.2f}")

7.2 Retrieval-augmented models

The retriever is thus trained, without relevance labels, to raise the chunks that best explain the target. Most systems in use skip this joint training and simply concatenate the retrieved chunks to the prompt. Their position matters: Liu et al. (2024) observe that models use information at the start or end of a long context better than in the middle.

7.3 Retrieval for code

• Repository context. Completing a function often needs the definitions of classes and helpers in other files. RepoCoder (Zhang et al., 2023) retrieves with the unfinished code, generates a draft, then retrieves again with the draft as query.
• Documentation. DocPrompting (Zhou et al., 2023) retrieves documentation pages before generating, which helps with functions that are absent or rare in the training data.
• Premises. In theorem proving, the chunks are the lemmas of a library; premise retrieval is the subject of ch. 8.
• Chunking. Cutting files along the syntax tree (functions, classes) keeps chunks meaningful, and the context budget of Example 1.12 limits how many fit.

8. Formal verification and automated theorem proving

A proof assistant accepts a proof only if every step checks. Pairing it with a language model gives a generator whose mistakes cost time but never correctness. This chapter formalizes proof search, studies how models guide it, and applies the same pattern to program verification.

8.1 Proof assistants and the Curry–Howard correspondence

The same statement can be proved by writing the term directly or by tactics, commands that transform the current goals and build the term behind the scenes:

theorem and_swap (p q : Prop) (h : p ∧ q) : q ∧ p :=
  ⟨h.2, h.1⟩                    -- a term: the pair (proof of q, proof of p)

theorem and_swap' (p q : Prop) (h : p ∧ q) : q ∧ p := by
  constructor                   -- two goals: q, then p
  · exact h.2
  · exact h.1

Tactic proofs suit language models: each step is a short string chosen from the visible goal, and the assistant reports the new goals or an error.

8.2 Proof search guided by a model

import heapq, math, itertools

def parse(s):                                  # right-associative implication
    toks = s.replace("(", " ( ").replace(")", " ) ").split()
    def expr(i):
        left, i = atom(i)
        if i < len(toks) and toks[i] == "->":
            right, i = expr(i + 1)
            return ("->", left, right), i
        return left, i
    def atom(i):
        if toks[i] == "(":
            e, i = expr(i + 1)
            return e, i + 1
        return toks[i], i + 1
    return expr(0)[0]

def premises(h, goal):                         # is h = A1 -> ... -> An -> goal ?
    out = []
    while isinstance(h, tuple):
        out.append(h[1]); h = h[2]
        if h == goal:
            return list(out)
    return None

def show(f):
    return f if isinstance(f, str) else f"({show(f[1])} -> {show(f[2])})"

def tactics(goal):                             # legal tactics on one goal
    hyps, f = goal
    if f in hyps: yield "assumption", []
    if isinstance(f, tuple): yield "intro", [(hyps | {f[1]}, f[2])]
    for h in sorted(hyps, key=str):
        ps = premises(h, f)
        if ps: yield f"apply {show(h)}", [(hyps, p) for p in ps]

PRIOR = {"assumption": 0.6, "intro": 0.3, "apply": 0.1}  # stand-in for a language model
def prove(formula, budget=1000):
    tie = itertools.count()
    frontier = [(0.0, next(tie), ((frozenset(), parse(formula)),), [])]
    while frontier and budget > 0:
        cost, _, goals, script = heapq.heappop(frontier); budget -= 1
        if not goals:
            return script                      # no goal left: proof found
        moves = list(tactics(goals[0]))
        z = sum(PRIOR[m.split()[0]] for m, _ in moves)
        for move, new in moves:
            p = PRIOR[move.split()[0]] / z
            heapq.heappush(frontier, (cost - math.log(p), next(tie), tuple(new) + goals[1:], script + [move]))
    return None

def check(formula, script):                    # the "kernel": replay every step
    goals = ((frozenset(), parse(formula)),)
    for move in script:
        new = dict(tactics(goals[0])).get(move) if goals else None
        if new is None:
            return False
        goals = tuple(new) + goals[1:]
    return not goals

for thm in ["(A -> B) -> (B -> C) -> A -> C", "((A -> B) -> A) -> A"]:
    script = prove(thm)
    print(thm, "|", "; ".join(script) if script else "no proof within budget")
    print("  checked:", script is not None and check(thm, script))

8.3 Learning to prove

• Data. Libraries such as Lean’s Mathlib (The mathlib Community, 2020) provide human proofs, extracted as (goal, tactic) pairs.
• Expert iteration. Polu et al. (2023) alternate proof search on a curriculum of statements and fine-tuning on the proofs found, turning compute into verified training data.
• Premise retrieval. ReProver (Yang et al., 2023) retrieves lemmas from the library with a dense retriever (Definition 7.3) before generating each tactic.
• Benchmarks. miniF2F (Zheng et al., 2022) formalizes 488 problems from AMC, AIME, IMO and courses; results are the fraction proved within a budget of attempts, a pass@k (Definition 5.5).

8.4 Autoformalization

Most mathematics is written informally. Wu et al. (2022) show that large language models can translate a sizeable fraction of competition statements into Isabelle/HOL. Draft, Sketch, and Prove (Jiang et al., 2023) generates an informal proof, turns it into a formal sketch with gaps, and closes the gaps with automated provers.

The checker guarantees that the formal proof proves the formal statement, not that the formal statement means the informal one. A mistranslated hypothesis can make a theorem trivially true, and only a human or a cross-check catches it.

8.5 Program verification and loop invariants

The same generate-and-check pattern verifies programs. The specification is a logical formula, the proof obligations are discharged by a solver, and the model supplies the creative part: the invariants.

Checking the three conditions is mechanical: tools such as Dafny (Leino, 2010) generate them as formulas and send them to an SMT solver such as Z3 (de Moura and Bjørner, 2008). Finding I is the creative step, and language models are good at proposing candidates.

# Program:  i, s = 0, 0;  while i < n: s, i = s + i, i + 1     Post: s == n(n-1)/2
pre  = lambda n, i, s: n >= 0 and i == 0 and s == 0
post = lambda n, i, s: 2 * s == n * (n - 1)
candidates = {                                   # invariants a model might propose
    "2s = i(i-1) and i <= n": lambda n, i, s: 2 * s == i * (i - 1) and i <= n,
    "2s = i(i-1)":            lambda n, i, s: 2 * s == i * (i - 1),
    "s >= 0":                 lambda n, i, s: s >= 0,
    "2s = i*i":               lambda n, i, s: 2 * s == i * i,
}
states = [(n, i, s) for n in range(12) for i in range(-3, 15) for s in range(-5, 80)]
for name, I in candidates.items():
    vcs = {
        "initiation":  all(I(*x) for x in states if pre(*x)),
        "consecution": all(I(n, i + 1, s + i) for n, i, s in states if I(n, i, s) and i < n),
        "exit":        all(post(n, i, s) for n, i, s in states if I(n, i, s) and not i < n),
    }
    print(f"{name:24s}", vcs)

9. Execution feedback, repair and software-engineering agents

This self-study chapter treats the second objective of the course description, applications in software engineering, as probabilistic procedures. A code model can run what it writes: tests filter samples, error messages guide repairs, and agents act on whole repositories. Each loop spends model calls, and each can be analysed with the tools of ch. 5.

9.1 Sample and test

Most tasks come with a few visible tests, such as the examples of a docstring, while correctness is judged by hidden ones. Sampling until a program passes the visible tests is a rejection sampler.

The precision \rho depends entirely on the quality of the visible tests. The same holds for benchmarks: EvalPlus (Liu et al., 2023) extended the tests of HumanEval automatically and found many wrong solutions that the original tests accepted, so the measured pass@k of the evaluated models dropped markedly.

import random

candidates = {
    "return sorted(set(xs))[-2]": 0.25,                       # correct
    "return max(x for x in xs if x != max(xs))": 0.10,        # correct
    "return sorted(xs)[-2]": 0.30,                            # ignores duplicates
    "return sorted(xs, reverse=True)[1]": 0.20,               # ignores duplicates
    "return sorted(set(xs))[1]": 0.15,                        # second smallest
}
def compile_candidate(body):          # our own strings here; real samples need a sandbox
    env = {}
    exec("def f(xs):\n    " + body, env)
    return env["f"]

rng = random.Random(0)
hidden = []
for _ in range(200):
    xs = [rng.randint(0, 9) for _ in range(rng.randint(2, 8))]
    if len(set(xs)) >= 2:
        hidden.append((xs, sorted(set(xs))[-2]))

def passes(f, tests):
    return all(f(list(xs)) == y for xs, y in tests)

weak = [([1, 2, 3], 2), ([5, 1, 4], 4)]
strong = weak + [([7, 7, 3], 3)]                              # one test with a duplicate
correct = {b for b in candidates if passes(compile_candidate(b), hidden)}
print(f"pass@1 = {sum(candidates[b] for b in correct):.2f}")
for name, visible in (("weak", weak), ("strong", strong)):
    ok = {b for b in candidates if passes(compile_candidate(b), visible)}
    q = sum(candidates[b] for b in ok)
    rho = sum(candidates[b] for b in ok & correct) / q
    print(f"{name} visible tests: P(pass) = {q:.2f}, P(correct | pass) = {rho:.2f}")

Generated code must never run unconfined: evaluation harnesses execute it in a separate process or container, without network access, with time and memory limits.

9.2 Self-repair

Instead of a fresh sample, the model can receive its failed program and the error message and propose a fix. Self-Debugging (Chen et al., 2024) and Reflexion (Shinn et al., 2023) build such loops. Olausson et al. (2024) compare them with resampling at an equal budget and find the gains modest, limited mainly by the quality of the feedback the model writes about its own code.

The comparison must be made at equal cost: a repair call reads a longer prompt (the program and the feedback), and on hard problems r can be smaller than p because the failed program anchors the model on a wrong idea.

9.3 Agents for software engineering

An agent alternates between generating an action (read a file, run a command, edit code, run the tests) and reading its result, in the reason-then-act format of ReAct (Yao et al., 2023). SWE-bench (Jimenez et al., 2024) evaluates such systems on 2 294 real GitHub issues from 12 Python repositories. An issue counts as resolved when, after the generated patch, the tests that the reference fix made pass now pass and the other tests still pass.

9.4 Learning from execution

Tests are a reward. Let R(x, y) \in \{0, 1\} indicate that program y passes the tests of task x. The pass rate is

J(\theta) = \mathbb{E}_{y \sim p_\theta(\cdot \mid x)}\big[R(x, y)\big] .

Fine-tuning on one passing sample per solved task, as in STaR (Zelikman et al., 2022) or in the expert iteration of ch. 8, is therefore stochastic gradient ascent on the sum of the log pass rates of the tasks.

Pooling all the passing samples of a fixed number of draws per task weights each task by its pass rate J instead. Since J\, \nabla \log J = \nabla J, it ascends the sum of the pass rates themselves.

CodeRL (Le et al., 2022) uses the policy gradient directly, with a learned critic. Subtracting a baseline from R, such as the average reward of other samples for the same task, keeps the first gradient unbiased and reduces its variance.

10. Research directions and open problems

This self-study chapter surveys active questions around the course, with entry points into the literature. It reports published results in a neutral voice; the field moves quickly, and the papers below are starting points, not a ranking.

10.1 Reinforcement learning from verifiable rewards

Code and formal proofs come with automatic checkers, which makes them natural targets for reinforcement learning. Shao et al. (2024) introduced group relative policy optimization (GRPO), which replaces a learned critic by the average reward of a group of samples for the same prompt, the baseline of Proposition 9.5. DeepSeek-AI (2025) reports that reinforcement learning with rule-based rewards on mathematics and code makes long chains of reasoning emerge in a pretrained model.

Open questions include reward hacking when tests are weak (Proposition 9.1 with small \rho), credit assignment over outputs of thousands of tokens, and how far gains on verifiable domains transfer to others.

10.2 Test-time compute

Brown et al. (2024) observe that the fraction of problems solved by at least one of k samples, the coverage, keeps growing over several orders of magnitude of k. The bottleneck then moves to selection: without hidden tests, how is the right sample recognized? Snell et al. (2024) study how to allocate inference compute between sampling, search against learned verifiers and sequential revision.

On the training side, Sardana et al. (2024) extend the compute-optimal analysis of ch. 3 to include inference costs, which favours smaller models trained on more tokens (Exercise 17). Besiroglu et al. (2024) attempt to replicate the fit of Definition 3.6 and report re-estimated parameters consistent with the two other approaches of Hoffmann et al. (2022).

10.3 Evaluation and contamination

Public benchmarks leak into web-scale training data. LiveCodeBench (Jain et al., 2024) collects contest problems over time and evaluates each model only on problems published after its training cut-off. Repository-level benchmarks such as SWE-bench (ch. 9) measure tasks closer to real work but are costly to run and to keep uncontaminated.

Functional correctness is also not the only criterion. Pearce et al. (2022) built 89 security-relevant scenarios for GitHub Copilot and found about 40 % of the 1 689 generated programs vulnerable. Measuring security, maintainability and faithfulness to a specification remains largely open.

10.4 Formal mathematics

AlphaGeometry (Trinh et al., 2024) combines a language model with a symbolic deduction engine and solves olympiad geometry problems, trained on synthetic data only. DeepSeek-Prover (Xin et al., 2024) autoformalizes informal problems into Lean 4 to generate large synthetic training sets of statements and proofs, verified by the assistant.

Three questions recur: the faithfulness of autoformalized statements (ch. 8.4), premise selection in libraries that keep growing, and the gap between informal reasoning, where models are fluent, and formal proofs, where every step must check.

10.5 Verified code generation

The generate-and-check pattern of ch. 8.5 extends to whole programs annotated with specifications in verification-aware languages such as Dafny. The model writes the code, the invariants and the auxiliary lemmas, and the verifier either accepts or returns a precise error. The hard part moves to the specification: who writes it, and how is a specification itself validated?

10.6 Exact constrained sampling and tokenization

Theorem 6.5 shows that masking does not sample from the conditional distribution. Sequential Monte Carlo (Lew et al., 2023) and grammar-aligned decoding (Park et al., 2024) approximate the exact conditional, at a cost in samples that is not yet well understood. Tokenization interacts with constraints and prompts (Proposition 2.6), which motivates byte-level models such as ByT5 (Xue et al., 2022), whose longer sequences make attention more expensive.

Exercises

The exercises are sorted by level: ★ applies the course, ★★ combines results or proves a short statement, ★★★ is open-ended. The Practice column of the session plan says when to attempt each one.

1. ★ The KV cache of a code model. A model has L = 40 layers, H = 40 query heads of dimension d_h = 128 and grouped-query attention with n_{kv} = 8, with a bf16 cache. (a) What is the cache size per token? (b) How many prompts of 32 768 tokens fit in 40 GB left free after loading the weights? (c) What would (b) be without grouped-query attention?

   Solution: (a) By Proposition 1.9, 2 \times 40 \times 8 \times 128 \times 2 = 163\,840 bytes, 160 KiB per token. (b) One prompt takes 163\,840 \times 32\,768 \approx 5.37 GB, so 7 prompts fit. (c) With n_{kv} = 40 each prompt takes five times more, 26.8 GB, so only one fits.

2. ★ BPE by hand. Run three merges of Algorithm 2.2 on the string aaabdaaabac, starting from its 11 characters. Give the merges, the final sequence and its length, and check Proposition 2.3.

   Solution: The adjacent pair aa is counted 4 times, twice in each aaa, but only 2 non-overlapping replacements are made.

   • Merge 1: aa → Z, giving Z a b d Z a b a c (length 9).
   • Merge 2: ab and Za tie with 2 occurrences; choosing ab → Y gives Z Y d Z Y a c (length 7).
   • Merge 3: ZY → X (2 occurrences), giving X d X a c (length 5).

   The length drops from 11 to 11 - 2 - 2 - 2 = 5, as Proposition 2.3 states. Choosing Za at the second merge also ends with 5 symbols.

3. ★ A compute-optimal budget. With the constants of Definition 3.6, compute N^\star, D^\star and the predicted loss for C = 10^{23} FLOPs, and the number of tokens per parameter. How does it compare with C = 10^{21}?

   Solution: Theorem 3.7 gives N^\star \approx 1.46 \times 10^{10} parameters, D^\star \approx 1.14 \times 10^{12} tokens and L \approx 2.005 (Code 3.9 prints them). The ratio is about 78 tokens per parameter, against 50 at 10^{21}: with \beta < \alpha, data grow faster than parameters.

4. ★ The size of a LoRA adapter. A 7-billion-parameter model has L = 32 blocks of width d = 4096. LoRA of rank r = 16 is applied to the four attention projections W_Q, W_K, W_V, W_O of every block. (a) Count the trainable parameters. (b) What fraction of the model is it? (c) How much memory do their Adam states take in fp32?

   Solution: (a) Each 4096 \times 4096 matrix gets 16 \times (4096 + 4096) = 131\,072 parameters, so 4 \times 32 \times 131\,072 = 16\,777\,216 in total, about 1.7 \times 10^7. (b) About 0.24 % of 7 \times 10^9. (c) Two fp32 states of 4 bytes per parameter: 134 MB.

5. ★ pass@k by hand. For one problem, 10 samples are drawn and 3 pass. Compute the unbiased estimates of pass@1, pass@3 and pass@5, and the plug-in estimates for k = 3 and k = 5.

   Solution: pass@1 = 3/10 = 0.3. pass@3 = 1 - \binom{7}{3}/\binom{10}{3} = 1 - 35/120 \approx 0.708. pass@5 = 1 - \binom{7}{5}/\binom{10}{5} = 1 - 21/252 \approx 0.917. The plug-in values are 1 - 0.7^3 = 0.657 and 1 - 0.7^5 \approx 0.832, lower, as Proposition 5.7 predicts.

6. ★ A nucleus by hand. The next-token probabilities are 0.45, 0.25, 0.12, 0.08, 0.05, 0.03, 0.02. Give the distribution used by top-3 sampling and by nucleus sampling with threshold 0.85.

   Solution: Top-3 keeps the first three tokens, of total 0.82, and renormalizes them to 0.549, 0.305 and 0.146. The nucleus is the smallest prefix of total at least 0.85: the first four tokens, of total 0.90, renormalized to 0.5, 0.278, 0.133 and 0.089.

7. ★★ Shifting positions in RoPE. (a) Show with Proposition 1.7 that RoPE attention scores, and hence the attention weights, are unchanged if every position is shifted by the same integer. (b) For d_k = 2, so that the only frequency is \theta_0 = 1, and q = k = (1, 0), compute the score as a function of n - m.

   Solution: (a) The score between positions m + c and n + c is q^\top R_{(n+c)-(m+c)} k = q^\top R_{n-m} k. Each score is unchanged, and so is each softmax row.

   2. R_{n-m} k = (\cos(n-m), \sin(n-m)), so the score is \cos(n - m). It is maximal at distance 0 but does not decrease with the distance: distance 6 scores \cos 6 \approx 0.96, almost as much as distance 0, and the sign of n - m is lost. Several frequencies \theta_i are needed to separate distances robustly.

8. ★★ Banding for near-duplicate detection. The k = br MinHash values of a file are split into b bands of r values. Two files become a candidate pair if they agree on all values of at least one band.

   1. Show that a pair of Jaccard similarity J becomes a candidate with probability

   1 - (1 - J^r)^b .

   2. Compute it for b = 20, r = 5 and J \in \{0.3, 0.8\}.

   Solution: (a) By Proposition 3.2 and the independence of the hashes, a band agrees with probability J^r, and the b bands are independent.

   2. The two similarities give:
   • for J = 0.8, J^5 = 0.328 and 1 - 0.672^{20} \approx 0.9996;
   • for J = 0.3, J^5 = 0.00243 and 1 - 0.99757^{20} \approx 0.047.

   The curve switches near (1/b)^{1/r} \approx 0.55: pairs above that similarity are almost always compared, pairs well below it almost never.

9. ★★ When n equals k. (a) Show that for n = k the unbiased estimator of Theorem 5.6 is \mathbb{1}[c \ge 1] and explain why it is unbiased. (b) For n = k = 2, compute the expectation of the plug-in estimator and its bias.

   Solution: (a) If c \ge 1, \binom{n-c}{n} = 0 and the estimator is 1; if c = 0 it is 1 - 1 = 0. Its expectation is the probability that one of k samples passes, pass@k itself.

   2. The count c takes the values 0, 1 and 2 with probabilities (1-p)^2, 2p(1-p) and p^2. The plug-in estimator then takes the values 0, 3/4 and 1.

   Its expectation is \frac{3}{2}p(1-p) + p^2, while pass@2 is 2p - p^2. The bias is

   -\tfrac{1}{2}\, p(1 - p) .

10. ★★ Distortion by hand. The valid strings are ab and b. The model emits a with probability 0.7 and b with probability 0.3; after a it emits b with probability 0.2 and an invalid token otherwise; after b it ends. (a) Compute p(\cdot \mid L). (b) Compute the distribution of masked decoding and the total variation distance. (c) Check the formula of Theorem 6.5 at the first step.

    Solution: (a) p(L) = 0.7 \times 0.2 + 0.3 = 0.44, so p(\texttt{ab} \mid L) = 0.14 / 0.44 \approx 0.318 and p(\texttt{b} \mid L) \approx 0.682.

    2. Both first tokens are viable, and after a only b is allowed: masking gives 0.7 and 0.3. The total variation distance is 0.7 - 0.318 = 0.382.

    3. w(\texttt{a}) = 0.2, w(\texttt{b}) = 1 and w(\varepsilon) = 0.44, so the exact first step gives a the probability 0.7 \times 0.2 / 0.44 \approx 0.318.

11. ★★ (Python) Truncated sampling. Implement top-k and nucleus truncation, sample 100 000 tokens from the nucleus distribution of Exercise 6, and check the empirical frequencies.

    Solution:

    import numpy as np
    rng = np.random.default_rng(0)
    
    def truncate(p, top_k=None, top_p=None):
        order = np.argsort(-p)
        keep = np.zeros_like(p, dtype=bool)
        if top_k is not None:
            keep[order[:top_k]] = True
        if top_p is not None:                       # smallest prefix reaching top_p
            n = np.searchsorted(np.cumsum(p[order]), top_p) + 1
            keep[order[:n]] = True
        q = np.where(keep, p, 0.0)
        return q / q.sum()
    
    p = np.array([0.45, 0.25, 0.12, 0.08, 0.05, 0.03, 0.02])
    q = truncate(p, top_p=0.85)
    draws = rng.choice(len(p), size=100_000, p=q)
    freq = np.bincount(draws, minlength=len(p)) / len(draws)
    print("nucleus 0.85 keeps", np.flatnonzero(q).tolist(), "with", np.round(q, 3).tolist())
    print("max |empirical - target| =", np.abs(freq - q).max().round(4))
    print("top-3:", np.round(truncate(p, top_k=3), 3).tolist())

    The empirical frequencies are within 0.002 of the target, of the order of the standard deviation \sqrt{q(1-q)/10^5} \approx 0.0016. A threshold equal to a partial sum, such as 0.9 here, is fragile in floating point: compare with a tolerance.

12. ★★ (Python) Stop words in code retrieval. In Code 7.5, compute recall@2, then remove the stop words a, an, the, of, with, to, and, into, do, I, how, in, by and the keyword def. Recompute recall@1, recall@2 and the MRR, and explain the change.

    Solution:

    import math, re
    from collections import Counter
    
    corpus = {
        "read_json":   "def read_json(path): load a JSON file and return a dict",
        "write_csv":   "def write_csv(rows, path): write rows to a CSV file",
        "parse_date":  "def parse_date(s): parse an ISO date string into a datetime",
        "http_get":    "def http_get(url, timeout): send a GET request and return the body",
        "retry":       "def retry(fn, attempts): call fn again until it succeeds",
        "lru_cache":   "def lru_cache(maxsize): memoize a function, evicting the least recently used",
        "sha256_file": "def sha256_file(path): hash a file with SHA-256 in chunks",
        "flatten":     "def flatten(nested): turn a list of lists into a flat list",
        "chunked":     "def chunked(xs, n): split a list into chunks of size n",
        "slugify":     "def slugify(title): lowercase a title and replace spaces by hyphens",
    }
    queries = {"how do I load a json config file": "read_json",
               "split list into batches of fixed size": "chunked",
               "compute the checksum of a large file": "sha256_file",
               "download a web page with a timeout": "http_get",
               "cache results of an expensive function": "lru_cache"}
    STOP = {"a", "an", "the", "of", "with", "to", "and", "into", "do", "i", "how", "in", "by", "def"}
    
    def evaluate(stop=frozenset()):
        tok = lambda s: [w for w in re.findall(r"[a-z0-9]+", s.lower().replace("_", " ")) if w not in stop]
        docs = {k: tok(v) for k, v in corpus.items()}
        M, avgdl = len(docs), sum(map(len, docs.values())) / len(docs)
        df = Counter(w for d in docs.values() for w in set(d))
        def bm25(q, doc, k1=1.2, b=0.75):
            tf = Counter(doc)
            return sum(math.log(1 + (M - df[w] + 0.5) / (df[w] + 0.5)) * tf[w] * (k1 + 1)
                       / (tf[w] + k1 * (1 - b + b * len(doc) / avgdl)) for w in tok(q) if w in tf)
        ranks = [sorted(docs, key=lambda d: -bm25(q, docs[d])).index(g) + 1 for q, g in queries.items()]
        return {k: sum(r <= k for r in ranks) / len(ranks) for k in (1, 2)}, sum(1 / r for r in ranks) / len(ranks)
    
    print("no stop words removed:", evaluate())
    print("stop words removed:   ", evaluate(STOP))

    Before: recall@1 = 0.8, recall@2 = 1.0, MRR = 0.90. After: all three equal 1.0. The word “with” no longer favours sha256_file, and “timeout” decides the fourth query. The synonym problem remains: no query word matches “GET request”.

13. ★★ A loop invariant for multiplication. The program r, i = 0, 0; while i < b: r, i = r + a, i + 1 runs from a state with b \ge 0. Find an invariant that proves the postcondition r = ab, and check the three conditions of Theorem 8.8.

    Solution: I \equiv (r = a i) \wedge (i \le b).

    • Initiation: r = 0 = a \cdot 0 and 0 \le b.
    • Consecution: if r = ai and i < b, then r + a = a(i + 1) and i + 1 \le b.
    • Exit: I and i \ge b give i = b, hence r = ab.

    The conjunct i \le b is necessary, exactly as in Code 8.9.

14. ★★ Resample or repair, with three calls. A fresh sample is correct with probability p = 0.3. Compare, with a budget of three calls, three independent samples and the chain sample–repair–repair, for a repair success probability r = 0.2 and r = 0.45, assuming independent attempts.

    Solution: Resampling succeeds with probability 1 - 0.7^3 = 0.657. The chain succeeds when the sample, the first repair or the second repair is correct, with probability

    p + (1-p)\,r + (1-p)(1-r)\,r .

    • For r = 0.45: 0.3 + 0.315 + 0.173 = 0.788, better than resampling.
    • For r = 0.2: 0.3 + 0.14 + 0.112 = 0.552, worse.

    As in Proposition 9.3, the comparison turns on r against p.

15. ★★★ Correcting the distortion. Let q be the distribution of masked decoding (Definition 6.1). Let Z_t(y_{<t}) be the total model probability of the tokens allowed at step t, and define the weight W(y) = \prod_t Z_t(y_{<t}).

    1. Show that every valid y satisfies q(y) = p(y) / W(y).

    2. Deduce that, for every function f,

    \mathbb{E}_q\big[f(Y)\, W(Y)\big] = \mathbb{E}_p\big[f(Y)\, \mathbb{1}[Y \in L]\big], \qquad \mathbb{E}_q[W] = p(L).

    3. Propose a self-normalized estimator of \mathbb{E}[f(Y) \mid Y \in L] and discuss its variance when p(L) is small.

    Hints and expected result: (a) Each factor of q is p(y_t \mid y_{<t}) / Z_t for an allowed token. (b) Multiply by W and sum over valid sequences; take f = 1 for the second identity.

    3. Draw y^{(1)}, \dots, y^{(m)} from q and use the ratio

    \frac{\sum_i W_i\, f(y^{(i)})}{\sum_i W_i} .

    It is consistent, and its variance grows with the spread of the weights, large when masking intervenes often. Sequential Monte Carlo (Lew et al., 2023) resamples particles to control it. On Code 6.7, the estimate converges to the exact conditional.

16. ★★★ (Python) A prover with conjunction and a learned policy. Extend Code 8.6 with conjunctions A \wedge B and two tactics. The tactic split turns a conjunctive goal into one goal per conjunct; the tactic cases h replaces a conjunctive hypothesis h by its two conjuncts. Then replace PRIOR by a policy learnt by expert iteration on random formulas.

    Hints and expected result: Extend the parser with a binary connective of higher precedence than ->, add the two tactics in tactics, and keep check unchanged: it only replays legal moves. The formula (A /\ B) -> (B /\ A) is then proved by intro, cases, split and two assumption steps.

    For the learning part, generate random provable formulas (for example, types of small lambda-terms), record the (goal, tactic) pairs of the proofs found, fit a classifier from goal features to tactics, and iterate (ch. 8.3). The success criterion is a larger fraction of held-out formulas proved within a fixed budget than with the fixed prior.

17. ★★★ Inference-aware scaling. A model will generate D_{\mathrm{inf}} tokens over its lifetime, at about 2N FLOPs per token. Minimize the total cost 6ND + 2ND_{\mathrm{inf}} under the constraint L(N, D) = \ell of Definition 3.6. (a) Write the optimality conditions. (b) Show that the optimal N decreases as D_{\mathrm{inf}} grows. (c) Discuss what this implies for code assistants serving many users.

    Hints and expected result: (a) With a multiplier \lambda: 6D + 2D_{\mathrm{inf}} = \lambda \alpha A N^{-\alpha-1} and 6N = \lambda \beta B D^{-\beta-1}.

    2. Along the constraint curve, D decreases when N increases. Raising D_{\mathrm{inf}} raises the marginal cost of parameters only, so the optimum moves towards smaller N and larger D. (c) Heavily used models are trained far beyond 20 tokens per parameter; Sardana et al. (2024) quantify this (ch. 10).

Projects and assessment

The official assessment (master-mva.com, “Mode de validation”) is homework worth 30 % and a final exam worth 70 %; the Université Paris-Saclay course detail describes it as partial continuous assessment (“Evaluation Continue non Intégrale”). The official homework subjects are not reproduced here; master-mva.com refers to the course page https://llm.labri.fr/ for the organisation of the sessions. The subjects below are proposals in the same spirit, sized for a laptop or a free GPU tier, with public or synthetic data and a measurable success criterion; the written exam proposal shows what a final exam on this material can look like.

Solo projects

1. [Solo · ≈ 20 h] Temperature and pass@k, reproduced. Paper study of Chen et al. (2021). Sample 50 programs per problem of HumanEval (164 problems, public) from a small open code model of at most 1.5 billion parameters, at temperatures 0.2 to 1.0, and run them in a sandbox.
   • Success criterion: unbiased pass@1 and pass@10 with bootstrap intervals over problems, showing the optimal temperature grow with k; compare random choice with mean log-probability ranking.
   • Deliverables: code, a 4–6 page report, a 10-minute talk. Chapters: ch. 5, 9. Evaluation: the rubric below.
2. [Solo · ≈ 20 h] Tokenizers for code. Paper study of Sennrich, Haddow and Birch (2016), with the whitespace observation of Chen et al. (2021). Train byte-level BPE and unigram tokenizers of 1 000 to 32 000 tokens on half of the CPython standard library sources, and on public-domain English books from Project Gutenberg.
   • Success criterion: held-out bytes per token against vocabulary size for code and text, and the measured gain of whitespace-run tokens and digit splitting.
   • Deliverables: code, a 4–6 page report, a 10-minute talk. Chapters: ch. 2. Evaluation: the rubric below.
3. [Solo · ≈ 20 h] Grammar-aligned decoding on a small model. Paper study of Park et al. (2024). Train a character-level transformer on synthetic arithmetic expressions with a fraction of corrupted ones, constrain it with the grammar of valid expressions, and compare masking with the importance-sampling correction of Exercise 15.
   • Success criterion: the total variation distance to the exact conditional, estimated by rejection sampling from the unconstrained model, is smaller with the correction for the same number of model calls.
   • Deliverables: code, a 4–6 page report, a 10-minute talk. Chapters: ch. 0, 6. Evaluation: the rubric below.

Group projects

1. [Group of 2–3 · ≈ 30 h each] A small code model with fill-in-the-middle. Paper study of Bavarian et al. (2022). Train a GPT of 10 to 30 million parameters on the deduplicated Python sources of the CPython standard library, with FIM rates 0, 0.5 and 0.9.
   • Success criterion: reproduce “FIM for free” qualitatively: left-to-right perplexity on held-out files within a few percent across FIM rates, and infilling exact match on single-line middles that grows strongly with the rate.
   • Split: tokenizer, MinHash deduplication and data pipeline; model and training; evaluation and report. Deliverables: code, a 6–8 page report, a 15-minute talk. Chapters: ch. 1–3. Evaluation: the rubric below, with individual questions on each member’s part.
2. [Group of 2–3 · ≈ 30 h each] LoRA on MBPP. Paper study of Hu et al. (2022). Fine-tune a small open code model of at most 1.5 billion parameters with LoRA of ranks 4 to 64 on the training split of MBPP (Austin et al., 2021), and evaluate on its test split in a sandbox.
   • Success criterion: pass@1 and pass@10 with the unbiased estimator and bootstrap intervals, a measured gain over the base model, and a rank ablation with trainable-parameter counts.
   • Split: data and training; sandboxed evaluation harness; statistical analysis and report. Deliverables: code, a 6–8 page report, a 15-minute talk. Chapters: ch. 4, 5, 9. Evaluation: the rubric below, with individual questions on each member’s part.
3. [Group of 2–3 · ≈ 30 h each] A tactic policy by expert iteration. Paper study of Polu and Sutskever (2020) and Polu et al. (2023) in a toy domain. Extend the prover of Code 8.6 with conjunction and disjunction, generate random provable formulas, and train a small policy network on the proofs found, round after round.
   • Success criterion: within a fixed expansion budget, the fraction of held-out formulas proved rises over three rounds above the fixed-prior baseline, and every proof is replayed by the checker.
   • Split: environment, checker and formula generator; policy model and training; search, expert iteration and evaluation. Deliverables: code, a 6–8 page report, a 15-minute talk. Chapters: ch. 8, 9.4. Evaluation: the rubric below, with individual questions on each member’s part.

Written exam (proposal)

Format: 2 hours, one handwritten A4 sheet allowed, no electronic devices, four questions.

1. Question (4 points). Explain why a transformer decoder can cache keys and values during generation. Give the cost of generating T tokens with and without the cache, the memory of the cache, and the effect of grouped-query attention.

   Expected: causality by induction on the layers (Proposition 1.8); the costs of Proposition 1.9; the size 2 L n_{kv} d_h e T bytes; grouped-query attention divides it by H / n_{kv}, with a numerical example.

2. Question (6 points). (a) For a problem, 20 samples are drawn and 4 pass: estimate pass@1 and pass@5 without bias. (b) Count the parameters of a rank-8 LoRA adapter on a 2048 \times 2048 matrix. (c) For the law of Definition 3.6 with \alpha = \beta = 0.5 and A/B = 1/4, compute N^\star and D^\star for C = 6 \times 10^{20}.

   Expected:

   • 1. pass@1 = 4/20 = 0.2, and by Theorem 5.6

     \text{pass@}5 = 1 - \binom{16}{5} \Big/ \binom{20}{5} = 1 - \frac{4368}{15504} \approx 0.718 .

   • 2. By Proposition 4.3, 8 \times (2048 + 2048) = 32\,768 parameters.
   • 3. G = 1/4 and \sqrt{C/6} = 10^{10}, so N^\star = 2.5 \times 10^{9} and D^\star = 4 \times 10^{10}: 16 tokens per parameter.

3. Question (5 points). Prove that 1 - \binom{n-c}{k}/\binom{n}{k} is an unbiased estimator of pass@k, and that the plug-in estimator 1 - (1 - c/n)^k is biased downward.

   Expected: the random-subset argument and the tower property of Theorem 5.6; concavity and Jensen’s inequality of Proposition 5.7.

4. Question (5 points). State the exact next-token distribution of a model conditioned on producing a string of a language L, prove it, and show on an example that masking invalid tokens samples from a different distribution.

   Expected: the formula of Theorem 6.5 with the completion probability w, by Bayes’ rule; an example in the style of Example 6.6 with the two distributions computed.

Grading rubric (proposal)

References

Official reference (master-mva.com):

• Course page announced on master-mva.com: https://llm.labri.fr/ — cited there for the organisation of the sessions.

Books:

• D. Jurafsky, J. H. Martin, Speech and Language Processing, 3rd edition draft, online, 2025.
• I. Goodfellow, Y. Bengio, A. Courville, Deep Learning, MIT Press, 2016.
• J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Pearson, 2006.
• C. D. Manning, P. Raghavan, H. Schütze, Introduction to Information Retrieval, Cambridge University Press, 2008.
• B. C. Pierce, Types and Programming Languages, MIT Press, 2002.
• T. Nipkow, L. C. Paulson, M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer, 2002.
• T. Nipkow, G. Klein, Concrete Semantics with Isabelle/HOL, Springer, 2014.

Chapters 1–2 (transformers and tokenization):

• A. Vaswani et al., “Attention Is All You Need”, NeurIPS 2017.
• J. Su, M. Ahmed, Y. Lu, S. Pan, W. Bo, Y. Liu, “RoFormer: Enhanced Transformer with Rotary Position Embedding”, Neurocomputing 568, 2024.
• N. Shazeer, “Fast Transformer Decoding: One Write-Head is All You Need”, arXiv, 2019.
• J. Ainslie, J. Lee-Thorp, M. de Jong, Y. Zemlyanskiy, F. Lebrón, S. Sanghai, “GQA: Training Generalized Multi-Query Transformer Models from Multi-Head Checkpoints”, EMNLP 2023.
• P. Gage, “A New Algorithm for Data Compression”, The C Users Journal 12(2), 1994.
• R. Sennrich, B. Haddow, A. Birch, “Neural Machine Translation of Rare Words with Subword Units”, ACL 2016.
• A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, I. Sutskever, “Language Models are Unsupervised Multitask Learners”, OpenAI technical report, 2019.
• T. Kudo, “Subword Regularization: Improving Neural Network Translation Models with Multiple Subword Candidates”, ACL 2018.
• T. Kudo, J. Richardson, “SentencePiece: A simple and language independent subword tokenizer and detokenizer for Neural Text Processing”, EMNLP 2018 (System Demonstrations).
• H. Touvron et al., “LLaMA: Open and Efficient Foundation Language Models”, arXiv, 2023.

Chapters 3–4 (pretraining, scaling, fine-tuning):

• A. Z. Broder, “On the Resemblance and Containment of Documents”, Compression and Complexity of Sequences, IEEE, 1997.
• M. Allamanis, “The Adverse Effects of Code Duplication in Machine Learning Models of Code”, Onward! 2019, ACM.
• K. Lee, D. Ippolito, A. Nystrom, C. Zhang, D. Eck, C. Callison-Burch, N. Carlini, “Deduplicating Training Data Makes Language Models Better”, ACL 2022.
• D. Kocetkov et al., “The Stack: 3 TB of permissively licensed source code”, arXiv, 2022.
• M. Bavarian, H. Jun, N. Tezak, J. Schulman, C. McLeavey, J. Tworek, M. Chen, “Efficient Training of Language Models to Fill in the Middle”, arXiv, 2022.
• J. Kaplan et al., “Scaling Laws for Neural Language Models”, arXiv, 2020.
• J. Hoffmann et al., “Training Compute-Optimal Large Language Models”, NeurIPS 2022.
• N. Muennighoff, A. M. Rush, B. Barak, T. Le Scao, A. Piktus, N. Tazi, S. Pyysalo, T. Wolf, C. Raffel, “Scaling Data-Constrained Language Models”, NeurIPS 2023.
• E. J. Hu, Y. Shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang, L. Wang, W. Chen, “LoRA: Low-Rank Adaptation of Large Language Models”, ICLR 2022.
• C. Eckart, G. Young, “The Approximation of One Matrix by Another of Lower Rank”, Psychometrika 1(3), 1936.
• A. Aghajanyan, L. Zettlemoyer, S. Gupta, “Intrinsic Dimensionality Explains the Effectiveness of Language Model Fine-Tuning”, ACL 2021.
• T. Dettmers, A. Pagnoni, A. Holtzman, L. Zettlemoyer, “QLoRA: Efficient Finetuning of Quantized LLMs”, NeurIPS 2023.
• N. Houlsby et al., “Parameter-Efficient Transfer Learning for NLP”, ICML 2019.
• X. L. Li, P. Liang, “Prefix-Tuning: Optimizing Continuous Prompts for Generation”, ACL 2021.
• Y. Wang et al., “Self-Instruct: Aligning Language Models with Self-Generated Instructions”, ACL 2023.
• Z. Luo et al., “WizardCoder: Empowering Code Large Language Models with Evol-Instruct”, ICLR 2024.
• Y. Wei, Z. Wang, J. Liu, Y. Ding, L. Zhang, “Magicoder: Empowering Code Generation with OSS-Instruct”, ICML 2024.

Chapters 5–7 (decoding, evaluation, structured generation, retrieval):

• M. Chen et al., “Evaluating Large Language Models Trained on Code”, arXiv, 2021.
• J. Austin et al., “Program Synthesis with Large Language Models”, arXiv, 2021.
• A. Holtzman, J. Buys, L. Du, M. Forbes, Y. Choi, “The Curious Case of Neural Text Degeneration”, ICLR 2020.
• K. Papineni, S. Roukos, T. Ward, W.-J. Zhu, “BLEU: a Method for Automatic Evaluation of Machine Translation”, ACL 2002.
• Y. Li et al., “Competition-Level Code Generation with AlphaCode”, Science 378, 2022.
• X. Wang et al., “Self-Consistency Improves Chain of Thought Reasoning in Language Models”, ICLR 2023.
• B. T. Willard, R. Louf, “Efficient Guided Generation for Large Language Models”, arXiv, 2023.
• J. Earley, “An Efficient Context-Free Parsing Algorithm”, Communications of the ACM 13(2), 1970.
• T. Scholak, N. Schucher, D. Bahdanau, “PICARD: Parsing Incrementally for Constrained Auto-Regressive Decoding from Language Models”, EMNLP 2021.
• G. Poesia, O. Polozov, V. Le, A. Tiwari, G. Soares, C. Meek, S. Gulwani, “Synchromesh: Reliable Code Generation from Pre-trained Language Models”, ICLR 2022.
• S. Geng, M. Josifoski, M. Peyrard, R. West, “Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning”, EMNLP 2023.
• A. K. Lew, T. Zhi-Xuan, G. Grand, V. K. Mansinghka, “Sequential Monte Carlo Steering of Large Language Models using Probabilistic Programs”, arXiv, 2023.
• K. Park, J. Wang, T. Berg-Kirkpatrick, N. Polikarpova, L. D’Antoni, “Grammar-Aligned Decoding”, NeurIPS 2024.
• S. Robertson, H. Zaragoza, “The Probabilistic Relevance Framework: BM25 and Beyond”, Foundations and Trends in Information Retrieval 3(4), 2009.
• V. Karpukhin et al., “Dense Passage Retrieval for Open-Domain Question Answering”, EMNLP 2020.
• P. Lewis et al., “Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks”, NeurIPS 2020.
• N. F. Liu et al., “Lost in the Middle: How Language Models Use Long Contexts”, Transactions of the ACL 12, 2024.
• F. Zhang et al., “RepoCoder: Repository-Level Code Completion Through Iterative Retrieval and Generation”, EMNLP 2023.
• S. Zhou, U. Alon, F. F. Xu, Z. Wang, Z. Jiang, G. Neubig, “DocPrompting: Generating Code by Retrieving the Docs”, ICLR 2023.

Chapters 8–9 (proof, verification, execution feedback):

• L. de Moura, S. Ullrich, “The Lean 4 Theorem Prover and Programming Language”, CADE-28, 2021.
• The mathlib Community, “The Lean Mathematical Library”, CPP 2020.
• S. Polu, I. Sutskever, “Generative Language Modeling for Automated Theorem Proving”, arXiv, 2020.
• S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, I. Sutskever, “Formal Mathematics Statement Curriculum Learning”, ICLR 2023.
• K. Yang et al., “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models”, NeurIPS 2023 (Datasets and Benchmarks).
• K. Zheng, J. M. Han, S. Polu, “miniF2F: a cross-system benchmark for formal Olympiad-level mathematics”, ICLR 2022.
• Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, C. Szegedy, “Autoformalization with Large Language Models”, NeurIPS 2022.
• A. Q. Jiang et al., “Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs”, ICLR 2023.
• C. A. R. Hoare, “An Axiomatic Basis for Computer Programming”, Communications of the ACM 12(10), 1969.
• K. R. M. Leino, “Dafny: An Automatic Program Verifier for Functional Correctness”, LPAR-16, Springer, 2010.
• L. de Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, TACAS 2008.
• J. Liu, C. S. Xia, Y. Wang, L. Zhang, “Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation”, NeurIPS 2023.
• X. Chen, M. Lin, N. Schärli, D. Zhou, “Teaching Large Language Models to Self-Debug”, ICLR 2024.
• N. Shinn et al., “Reflexion: Language Agents with Verbal Reinforcement Learning”, NeurIPS 2023.
• T. X. Olausson, J. P. Inala, C. Wang, J. Gao, A. Solar-Lezama, “Is Self-Repair a Silver Bullet for Code Generation?”, ICLR 2024.
• S. Yao et al., “ReAct: Synergizing Reasoning and Acting in Language Models”, ICLR 2023.
• C. E. Jimenez, J. Yang, A. Wettig, S. Yao, K. Pei, O. Press, K. Narasimhan, “SWE-bench: Can Language Models Resolve Real-World GitHub Issues?”, ICLR 2024.
• J. Yang et al., “SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering”, NeurIPS 2024.
• R. J. Williams, “Simple Statistical Gradient-Following Algorithms for Connectionist Reinforcement Learning”, Machine Learning 8, 1992.
• H. Le, Y. Wang, A. D. Gotmare, S. Savarese, S. C. H. Hoi, “CodeRL: Mastering Code Generation through Pretrained Models and Deep Reinforcement Learning”, NeurIPS 2022.
• E. Zelikman, Y. Wu, J. Mu, N. D. Goodman, “STaR: Bootstrapping Reasoning With Reasoning”, NeurIPS 2022.

Chapter 10 (research directions):

• Z. Shao et al., “DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models”, arXiv, 2024.
• DeepSeek-AI, “DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning”, arXiv, 2025.
• B. Brown et al., “Large Language Monkeys: Scaling Inference Compute with Repeated Sampling”, arXiv, 2024.
• C. Snell, J. Lee, K. Xu, A. Kumar, “Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters”, arXiv, 2024.
• N. Sardana, J. Portes, S. Doubov, J. Frankle, “Beyond Chinchilla-Optimal: Accounting for Inference in Language Model Scaling Laws”, ICML 2024.
• T. Besiroglu, E. Erdil, M. Barnett, J. You, “Chinchilla Scaling: A replication attempt”, arXiv, 2024.
• N. Jain et al., “LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code”, arXiv, 2024.
• H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, R. Karri, “Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions”, IEEE Symposium on Security and Privacy, 2022.
• T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong, “Solving Olympiad Geometry without Human Demonstrations”, Nature 625, 2024.
• H. Xin et al., “DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data”, arXiv, 2024.
• L. Xue et al., “ByT5: Towards a Token-Free Future with Pre-trained Byte-to-Byte Models”, Transactions of the ACL 10, 2022.