bilingual · en / pt
llama.bend: language models with typed weights and cache
AI and machine learning#Bend#LLMs#typesThe first bend-ml post started with a small question: what if a matrix multiplication with incompatible dimensions could not compile? The next one followed the cost of making GPT-2 actually run, weights stored in bands, and parallelism disappearing from the generated C. llama.bend continues that story with another architecture and an extra requirement: carrying the model's structure and the cache's state in its types.
I built a package that runs SmolLM2-135M, SmolLM2-360M and SmolLM2-1.7B on the CPU. All three use the same Bend layers with a different configuration. In the published tests, generated tokens and decoded text match transformers. There are also 21 laws about the program's structure, checked by Bend and again with --verdict. Execution remains slower than the references; loading the model is especially expensive.
I will explain how text becomes a sequence of computations, why some of those computations let the checker reject swapped weights, what a causal cache means, and where a proof stops helping. Then come the numerical error that appeared in the larger model, the cache change, and the numbers, with the context of each comparison. The code and results used here are in the public llama.bend and bend-ml repositories, at fixed revisions.
- 2026-10-09tokenizer and one layer1 dayprepare the weights, adapt tokenization and compare the layer's pieces.
- 2026-10-10the whole model2 daysgeneration, a typed API, laws and all three SmolLM2 sizes.
- 2026-10-12array cache1 dayparallel heads and cache capacity required in the type.
- 2026-10-13Bend 2.0.37compiler update and the public performance comparison.
first, what the name means
Llama here means the architecture: the arrangement of operations that turn input tokens into scores for the next token. The weights I used are the public SmolLM2 family checkpoints, identified as HuggingFaceTB/SmolLM2-*. A checkpoint is the collection of numbers a training run has already found. Writing the operations in another language lets me use those numbers without repeating the training.
That matters when reading the result. I did not train a Llama model in this project, and the name does not mean I downloaded a Meta model's weights. I implemented inference, which means computing an answer with weights that are already available. The program receives text, reads the prepared weights and produces tokens. Those weights are not updated during the generation described in this post.
It is also not every model with “Llama” in its name. Preparation checks a particular combination: SwiGLU, no biases, plain RoPE and output weights shared with the embedding. Each condition corresponds to a piece of the program. A model with another positional variant, for example, is not supported merely because its matrices fit in memory. Architecture compatibility has to come before comparing results.
bend-ml provides the foundation for those computations. llama.bend imports the tensor and array tensor packages, and adapts tokenization from the GPT-2 work. The new package brings together the configuration, one layer's weights, the sequence of layers, the cache and the laws relating those pieces. That makes it possible to discuss the whole model without reimplementing matrix–vector multiplication in every layer.
In the public code, the three checkpoint revisions are pinned in reference/models.py. Separating code, configuration and weights helps with the rest of this post: code says how to compute; configuration supplies the sizes and some architecture choices; weights are the learned numbers. To reproduce a result, all three need to agree.
from text to the next token
This kind of model does not receive a sentence as a string. First, the tokenizer divides text into units from a vocabulary and returns their identifiers, which are integers. A unit can be part of a word, a space attached to a word fragment, or another piece. Counting words does not tell you how many tokens a sentence will have: that depends on the model's rules and vocabulary.
An identifier acts as an address into the embedding, a table of vectors. A vector is just a sequence of numbers; in the 135M, there are 576 numbers per token. Looking up the row for an identifier gives that position's initial representation. It then passes through the decoder layers, each using its weights and the allowed history to transform that representation. At the end there is another normalization and a projection into the vocabulary.
That final projection produces one number for every possible token: the logits. They are scores, not yet probabilities. The demo uses the simplest choice, called greedy decoding: take the identifier with the largest score. That token becomes part of the text and goes into the next step. Repeating this generates the sequence. The prompt has to be processed first so that every layer's cache contains the positions that have already appeared.
The SmolLM2 tokenizer needed its own adaptation. Reusing the GPT-2 tokenizer unchanged did not produce the same IDs. Preprocessing splits digits individually, including the Unicode digits recognized by the reference; merge numbering is different too. A merge is the rule that joins two fragments into a larger unit in BPE. Getting those rules right comes before investigating model differences: different inputs produce different computations.
There is a less tidy detail that also belongs here: some bytes have no token in this vocabulary and are dropped during preprocessing to match the reference. A law about undoing BPE merges therefore does not imply that every byte sequence passes through this complete tokenizer and comes back intact. The mathematical component and a particular model's convention are different parts of the path. The adaptation and tests are in the Bend tokenizer and the public October 9 notes.
what one layer computes
Imagine following the vector at one position. A layer needs to consult earlier positions and then transform the result. In llama.bend, this appears in two blocks: attention and a projection network called the MLP. Each block is preceded by RMSNorm and followed by an addition to the vector that entered it. That addition, the residual connection, preserves a direct path for the previous representation while the layer adds a transformation.
normalize before looking things up
The RMSNorm operation adjusts the scale of the numbers. It squares the components, computes their mean and uses the square root of that mean to obtain a scale factor. A small eps is added before the square root, and each component also receives a learned gain. This does not subtract the vector's mean: the operation uses the mean of its squares. The implementation preserves the reference's multiplication order, because floating-point ordering can change the last bits.
Attention starts by projecting the normalized vector into three others: query, key and value, or Q, K and V. You can read the query as what the position is looking for, the key as what lets each position be compared with that query, and the value as the information to combine. This is a way to follow the computation, not a literal translation of the meaning of each learned number.
The query is compared with the available keys through dot products. The computation is scaled and passed through softmax, which turns scores into positive weights adding up to one in the mathematical description of the operation. Those weights combine the values. The output therefore depends on the consulted positions with different strengths. The model does this in several heads, smaller parts of the vector that keep separate queries, then joins their results and applies an output projection.
the transformation after attention
After attention and the first residual addition come another RMSNorm and the MLP. Here it uses SwiGLU. Two projections, gate and up, receive the same vector. The first passes through the silu function; its result is multiplied component by component with the second. A third projection, down, restores the size used by the rest of the model. The resulting vector enters the second residual addition.
A useful way to read gate is as a transformation that modulates the other one, rather than simply chaining two matrices. The names do not mean a binary decision to open or close: the value is numerical. In the 135M, the 576-component vector is projected to 1536 inside the MLP and returns to 576. Returning to that size is necessary to add the result to the residual path, component by component.
The public function block lets you follow that entire path. It returns the vector, the updated cache, the weights and a record of intermediate values. This helps compare a layer internally: if the final result differs, the first normalization, Q/K/V, attention and MLP can be inspected separately. A generated sentence does not tell you which computation first introduced a difference.
nine queries, three sets of keys
In the most direct version of multi-head attention, each query head has a matching key head and value head. But their counts do not have to be equal. The 135M has nine query heads and only three key/value heads. Each set of keys and values serves three different queries. This is grouped-query attention, or GQA: grouping queries to share K and V.
Sharing does not make the queries identical. Each still produces its own scores and its own combination of values. What changes is the set it consults. For a fixed head size, storing fewer K/V sets also reduces the number of cache values compared with storing nine of them. That relationship is not a promise of a proportional reduction in whole-program time: the other products still exist.
The risk is in the address: making a query read the neighboring K/V head is still a numerical computation and may not cause a runtime error. In the package, queries are organized into groups, and each group is traversed alongside its K/V set. The gqa_head law establishes that this organization chooses the same head as the division used by the reference mapping.
In plain terms: with g queries per group, query index j·g + i, with i smaller than g, belongs to group j. The law proves that dividing that index by g gives j. The useful detail is “for any”: it does not merely enumerate the nine queries in the 135M. The argument holds for indices satisfying those conditions; concrete configurations are instances of that relationship.
In the 360M there are fifteen queries for five K/V sets, again three per group. In the 1.7B there are 32 for 32: g = 1. That case is ordinary multi-head attention, represented by the same general configuration. The group and array count laws complete the structural part, checking that grouping and cache creation have the expected counts. The package README explains the laws, and the code contains their statements and proofs.
position as rotation
So far I have explained how to compare queries and keys, but not how their positions enter the computation. In llama.bend that information comes through RoPE, rotary position embeddings. The operation rotates pairs of query and key components by an angle depending on the position and that pair's frequency. Values do not go through this rotation. The learned weights stay the same; the rotation changes with the position being processed.
Think of two coordinates as the tip of an arrow on a plane. Rotating that arrow changes its coordinates without adding a new component to the vector. Different pairs use different frequencies. When rotated queries and keys meet in a dot product, position already participates in the comparison. The drawing below only illustrates rotation: its angles and arrows are not measured prompt activations.
The pairing convention has to match the checkpoint. Here a head is split into two halves: component i of the first is paired with component i of the second. These are not simply neighboring pairs along the whole vector. The configuration stores half, half the head size, and computes the total size as 2·half. That makes the size even by construction, instead of relying on a comment asking for an even number.
The head_split law says something precise and narrower than “RoPE is correct”: splitting a list into those parts and joining them returns the original list in the same order. It prevents the rearrangement from losing or moving components. It does not prove the accuracy of sine, cosine or F32 multiplications. Those results are covered by numerical layer comparisons. A proof that the pieces return to their places is not a proof that every number computed with them matches the reference.
All three models use 64-component heads. The 1.7B also changes RoPE's base, theta: 130000, compared with 100000 in the two smaller models. Those values enter the frequency computation, not the matrix sizes. This is a configuration difference that would remain even if some shape could be reused. The RoPE implementation and the configurations make those choices explicit.
the configuration reaches the weight types
An ordinary configuration might just be a set of numbers read before allocating memory. Here it also participates in types. Cfg stores the K/V head count, queries per group, half the head size, MLP width, layer count, vocabulary and the normalization and position parameters. One layer's weight type is LW<c>: it depends on that configuration c.
type Cfg is Data:
Cfg{kv: Nat, g: Nat, half: Nat, f: Nat, layers: Nat, vocab: Nat, eps: F32, theta: F32}Three calculations follow from that record: query heads = kv·g; vector width = kv·g·2·half; K or V width = kv·2·half. In the 135M, that gives nine heads, a 576-component vector and 192 components in K and V. Each matrix has one row per output component and one column per input component, the convention used to load the weights. Storing only the total number of values is insufficient: the two dimensions play different roles.
| configuration | 135M | 360M | 1.7B |
|---|---|---|---|
| Q / K/V heads | 9 / 3 | 15 / 5 | 32 / 32 |
| vector width | 576 | 960 | 2048 |
| K or V width | 192 | 320 | 2048 |
| MLP inner width | 1536 | 2560 | 8192 |
| layers | 30 | 32 | 24 |
The easiest test to understand is swapping Q and K in the 135M. Q's matrix is Bands<576n, 576n>; K's is Bands<192n, 576n>. Bands is bend-ml's banded matrix representation, with rows and columns in the type. The excerpt below, from the public test, rebuilds the layer with those matrices reversed. It is a program meant to be rejected, not an example of correct usage.
def swap(lw: M.LW<M.smollm2_135m()>) -> M.LW<M.smollm2_135m()>:
match lw:
case M.LW{ln1, q, k, v, o, ln2, gate, up, down}:
M.LW{ln1, k, q, v, o, ln2, gate, up, down}The Q field requires 576 rows and receives a matrix with 192. The error appears before computing any token. It does not depend on choosing a prompt that reveals the problem or inspecting the text afterward. But the guarantee stops at the dimensions expressed by the type: swapping two matrices with the same shape does not automatically become a type error. Nor can the type discover on its own that a correctly sized file contains weights from another source.
The layout laws complement this by counting expected values: 134515008, 361821120 and 1711376384 for the three checkpoints. The loader checks each file's size against the expected shape and stops on a mismatch. These are checks of organization and quantity, alongside pinned revisions and tests; they are not a proof of the semantic authenticity of an arbitrary byte sequence. The weight types and layout laws show exactly where those boundaries lie.
a cache that knows how much has been written
To generate the next position, attention consults keys and values from earlier positions again. Recomputing everything from the beginning would repeat work. The KV cache stores those results per layer. It does not store a ready-made “answer” to reuse: it stores representations of each position, and each new query still has to consult the history. Having a cache therefore does not turn all of attention into a constant-cost operation.
There are two separate questions: which positions exist, and how much space is available for them? The type KV<cap, t> carries both. cap is the reserved capacity in positions; t is how many have been written. Before processing position index t, positions zero through t − 1 exist. The block writes the current position's key and value and returns a cache of type KV<cap, t + 1>. Attention then consults zero through t, including the current position.
This is the causal part: the current position consults its own step and the past, without reading a future position. causal and read_len relate the read to exactly t + 1 keys and scores. Physical capacity can be larger. Initializing spare space does not make it previous text, and confusing those two sizes would allow reading positions outside the sequence.
Writing additionally requires a proof that t is smaller than cap. kv_room connects that bound to the number of array slots, including the head size. The room proof is a required argument of KV.push, block and forward. The contract therefore does not remain only in a law someone might forget to apply: the functions advancing the model request that argument.
The capacity test attempts a third write into KV<2n, 2n>. Two positions already exist, and capacity is only two. The call would need to prove 2 < 2; the checker rejects the attempt. This matters especially because Bend array indices can wrap around: exceeding capacity could overwrite an earlier slot. The API requires the bound before reaching that write.
The proofs are erased during compilation. They determine whether the program is accepted or rejected, without a justification tree to traverse at every token. That does not eliminate allocation, memory reads or matrix products; it eliminates the runtime cost of the formal evidence. The full description is in the cache laws and the API change notes.
the proofs did not make the sum accurate
Running the other two sizes was a concrete way to test whether changing the configuration really was sufficient. The 1.7B exposed a problem unrelated to shapes: the layer 15 test failed on attention and MLP intermediates. The layer's final output was still close to the reference, but some internal values exceeded the comparison threshold. Looking only at the last vector would have hidden the difference.
The cause appeared in the first RMSNorm. It needed to sum 2048 squares, with components at very different scales. F32 stores numbers with finite precision. If an accumulated sum is already large, adding a small term can lose part of that term to rounding. Repeating the operation thousands of times is not numerically identical to adding real numbers with infinite precision, even when every dimension is correct.
The initial version added each square to a single accumulator. The correction was a tree sum: add neighboring pairs, then pairs of their results, until reaching the total. pair_sums and tree_sum do that. It does not change which components enter normalization, but it changes the order of rounding. This is exactly the sort of change where a structurally equivalent program can stop producing the same bits.
The public result gives a specific comparison for that first normalization in the 1.7B's layer 15: against the float64 execution used in the notes, Bend's reported error fell from 4.6e-6 with sequential summation to 1.5e-7 with pairwise summation. Those are numbers from that case, not a guarantee for every vector, ordering or machine. The point is that the change was compared with a numerical reference as well as continuing to pass the checker.
This also prevents treating PyTorch as a definition of real arithmetic. It computes in floating point too. Comparing with transformers asks whether my implementation tracks that reference under fixed versions and choices; a higher-precision comparison helps investigate a particular discrepancy. It does not turn every difference into a bug or every agreement into a proof of exactness. The account and results of this correction are in the RMSNorm notes.
changing the cache changed the cost
Storing K and V avoids recomputing their projections, but storing them has a cost of its own. The first representation kept history in lists. Attention had to reconstruct cache rows, reorganize them by head and build intermediate results while traversing positions. More history meant more list work in every new step. Reusing the numbers was not enough to reuse their organization.
The change was to flat arrays, with one key array and one value array per K/V head in each layer. A new position is written into its reserved space. Attention products read valid positions directly from those arrays with the appropriate strides. A stride is the step between elements in memory: it lets the same numbers be viewed as rows or columns without materializing a list transpose at every token.
Then came splitting K/V heads to execute groups in parallel. Since each group consults its own array set, different sets can be handed to different tasks and their results joined in group order. This adds to the banded weight products inherited from bend-ml. These are different places to divide work, with different costs; more tasks do not automatically mean less time.
The historical October 12 result helps separate the effects. With Bend 2.0.36 and tensor-array 0.1.7.0, on the 1.7B generating 128 tokens at 16 threads, the list version took 1692 ms per token. Arrays with sequential heads gave 427 ms; arrays with parallel heads gave 385 ms. The large gain in that comparison came from changing the cache representation. Parallelizing heads added another gain in that case.
Those numbers belong to that comparison among three versions, identified in the public benchmark. They should not be mixed with the final October 13 table to invent a compiler regression or gain. Nor are they a rule for one thread: creating and joining tasks costs something even when no additional cores are available to use them. The version measured on October 13 keeps heads sequential with up to two threads and parallelizes them above that.
The array cache still reads previous positions. In a 512-token generation on the 1.7B at 16 threads, the published first- and last-quarter times were 427 and 452 ms per token. There is measured growth; it became small relative to the earlier list problem, rather than disappearing through a mathematical property of caching. “Flatter over this interval” is more accurate than “context stopped costing anything.”
what I checked, and what each test says
A plausible-looking generation is weak evidence for an implementation. Even choosing the same token only shows that the largest score stayed in the same place. Two logit vectors can differ and still have the same maximum. The repository therefore separates numerical comparison, token selection and decoded text, alongside layer and tokenizer tests.
The forward test uses 11 prompts with 88 positions in total and compares each position's logits with transformers 5.19 in F32 and eager attention. “Eager” identifies the attention implementation selected in the reference; changing that path can change operation ordering. The reported measure divides the largest absolute logit difference by the largest absolute value in the reference vector. It is not each component's individual relative error.
| published result | 135M | 360M | 1.7B |
|---|---|---|---|
| worst logit error under this measure | 2.1e-5 | 4.8e-5 | 8.3e-5 |
| argmax at all 88 positions | same | same | same |
| 32 greedy tokens on 12 prompts | identical | identical | identical |
| decoded text on those prompts | identical | identical | identical |
The generation rows are a separate set: 12 prompts, with 32 tokens generated per case. The test checks prompt IDs, generated IDs and text, plus the chosen tokens' logits within tolerance. Those are not 12 prompts used to calculate the first table row. The two public scripts make the distinction explicit: forward examines the logit vector; generation examines the produced sequence.
Tokenization is checked separately too. The published result records matching IDs on 68 fixed texts and 600 random ones; decoding was compared on 1500 random ID sequences. These are documented expanded runs, not a claim that every default script invocation runs exactly those counts. Checking decoding independently matters because arbitrary ID sequences can form bytes that are not valid UTF-8.
The 21 laws belong in a different category. They cover head splitting, Q-to-K/V mapping, group and array counts, causal reads, write bounds and layout, supported by arithmetic lemmas. The package does not use @unsafe, ?TODO or axioms in place of those proofs. But vectors between layers remain lists without their lengths in their types, and F32 operations are still validated through tests. Saying “the whole inference process was formally proved” would exceed what is implemented.
There is also a public exception to “all systems produce the same tokens.” In the long 360M comparison, llama.cpp's text diverged after approximately 340 tokens. The benchmark records that llama.bend's sequence was checked with transformers. This does not invalidate the table's short comparisons, but it limits their scope. Matching tokens in tested runs is not a universal guarantee for every length, implementation or prompt.
the numbers still show the gap
The final published comparison was measured on October 13, 2026, on an Intel Core Ultra 7 155H with 32 GB RAM, on the CPU in F32. The measured code is commit 3ea435a, with tensor-array 0.1.7.0 and Bend 2.0.37. The revision used to document this post is later and contains that report; I am not presenting the table as a new measurement made today.
The references are transformers 5.19 with PyTorch 2.14.1, llama.cpp at commit 23b0202 using F32 GGUF, and candle at c68b249, also F32. The table below shows milliseconds per generated token, separating one thread and 16 threads. The 135M and 360M generate 32 tokens; the 1.7B generates 128. Weight loading and prompt processing are outside this metric. Complete results are in BENCHMARK.md.
| model and generation | system | 1 thread | 16 threads |
|---|---|---|---|
| 135M · 32 tokens | llama.bend | 121 | 76.7 |
| 135M · 32 tokens | transformers | 26.3 | 21.1 |
| 135M · 32 tokens | llama.cpp | 23.7 | 14.0 |
| 135M · 32 tokens | candle | 26.6 | 28.8 |
| 360M · 32 tokens | llama.bend | 283 | 133 |
| 360M · 32 tokens | transformers | 57.1 | 40.0 |
| 360M · 32 tokens | llama.cpp | 63.1 | 28.3 |
| 360M · 32 tokens | candle | 71.6 | 74.3 |
| 1.7B · 128 tokens | llama.bend | 1203 | 492 |
| 1.7B · 128 tokens | transformers | 231 | 132 |
| 1.7B · 128 tokens | llama.cpp | 324 | 101 |
| 1.7B · 128 tokens | candle | 292 | 295 |
The 1.7B needs a caveat already present in the report: the 492 ms carries loading-time variation in the published comparative metric. The generator's internal clock recorded 426 ms per token at 16 threads. These are different measurements, and replacing one with the other in the table would hide that difference. Internal timing helps interpret the spread; it does not justify choosing only the most favorable number for a system comparison.
Bend 2.0.37 includes the compiler correction discussed in the previous post, but this project did not gain speed from it in the published comparison. The 1.7B's internal times at 16 threads were 423 ms on 2.0.36 and 426 on 2.0.37. The update matters as an environment version; I will not credit it with gains that came from changing the cache. Having a relevant compiler fix and saving time in this program are claims requiring separate evidence.
waiting for the first token counts too
For someone opening the demo, waiting for weights to reach memory is part of the experience. The report also measures a run that loads the model and generates one token. The following table gives that total time and peak resident memory at 16 threads. It is neither an isolated loader measurement nor the cost of each token after the program is ready.
| system | 135M | 360M | 1.7B |
|---|---|---|---|
| llama.bend | 4.4 s · 781 MB | 11.5 s · 2332 MB | 66.4 s · 6935 MB |
| transformers | 2.7 s · 1168 MB | 2.7 s · 2469 MB | 4.1 s · 10189 MB |
| llama.cpp | 0.2 s · 743 MB | 0.2 s · 1752 MB | 0.5 s · 8116 MB |
| candle | 0.2 s · 791 MB | 0.4 s · 2107 MB | 2.5 s · 9844 MB |
Loading is llama.bend's slowest part. The read path produces lists with one cell per byte, and building and traversing those lists costs time. A lower peak than some references in this table does not automatically compensate for more than a minute until the 1.7B's first token. Nor is it a general guarantee of lower memory: the same report records an 8.4 GB peak for the 1.7B at one thread.
These results leave a clear gap to llama.cpp and transformers. The array cache removed a large cost, but did not make weight products or file reads disappear. The measurements describe this machine, these versions and these generations. They are not speed predictions for another processor, quantization or a GPU. This project runs on the CPU, and the numbers presented here use F32.
running what is published
The entry points are the public repository and the project page. The documented commands start by preparing the environment, downloading and converting the checkpoint, and checking the results. For the 135M, the README lists Linux x86_64 or WSL, clang, Python 3.14 and curl. Initial preparation also needs room for the Python environment and model files; it is not just the size of the Bend executable.
git clone https://github.com/nuxyel/llama.bend.git
cd llama.bend
make setup
make prep
make check
bend demo/gen.bend -o gen
./gen data/smollm2-135m "The capital of France is" 32make setup prepares the documented tool versions; make prep fetches the model and writes files the Bend program reads. make check checks laws, programs that must be rejected and reference comparisons. That does not mean Bend inference calls Python for every token: Python participates in preparation and verification. Generation in the example runs in the compiled executable.
To prepare and check another size, the public command is make prep check MODEL=smollm2-360m, or MODEL=smollm2-1.7b. The program receives the corresponding directory on the command line. The same API is published on BendHub as bend-ml-llama@0.1.0.0; its documentation describes forward, block, cache creation and the room proofs needed to advance one position.
import bend-ml-llama@0.1.0.0/main.bend as MThere is an API detail coming from affine types: products return the weights they received. Arrays have one owner, so computing with a matrix and continuing to use it requires explicitly passing it onward. block returns LW<c> and forward returns Model<c>. This explains why a call returns more than a logit vector. The result structure is part of how weights remain available for the next token.
What is published remains an inference implementation for base models, using greedy selection, without a chat template. It does not amount to opening a ready-to-chat assistant. It also does not include a proof of every intermediate value or automatic support for every architecture variant. Those limits belong alongside the results because they change what it makes sense to expect from the demo.
For me, the interesting part of this stage is being able to point to specific mistakes the API now excludes: incompatible Q and K weights in the wrong places, a query assigned to the wrong group under the proved mapping, a cache write without room. At the same time, the RMSNorm sum needed numerical investigation, and generation still loses to the references on time. The code and results let you inspect both parts: what the structure guarantees and what still needs measurement and tests.
O primeiro post sobre o bend-ml começou com uma pergunta pequena: e se uma multiplicação de matrizes com dimensões erradas não pudesse compilar? O seguinte foi atrás do custo de fazer o GPT-2 rodar de verdade, dos pesos guardados em bandas e do paralelismo que desaparecia no C gerado. O llama.bend continua essa história com outra arquitetura e uma exigência a mais: carregar a estrutura do modelo e o estado do cache nos tipos.
Construí um pacote que executa SmolLM2-135M, SmolLM2-360M e SmolLM2-1.7B na CPU. Os três usam as mesmas camadas em Bend, com outra configuração. Nos testes publicados, os tokens gerados e o texto decodificado correspondem ao transformers. Há também 21 leis sobre a estrutura do programa, checadas pelo Bend e novamente com --verdict. A execução continua mais lenta que as referências; carregar o modelo é especialmente caro.
Vou explicar como o texto vira uma sequência de contas, por que algumas dessas contas permitem rejeitar pesos trocados, o que significa um cache causal e onde uma prova deixa de ajudar. Depois vêm o erro numérico que apareceu no modelo maior, a troca do cache e os números, com o contexto de cada comparação. O código e os resultados usados aqui estão nos repositórios públicos llama.bend e bend-ml, em revisões fixas.
- 2026-10-09tokenizer e uma camada1 diapreparar os pesos, adaptar a tokenização e comparar as peças da camada.
- 2026-10-10o modelo inteiro2 diasgeração, API tipada, leis e os três tamanhos de SmolLM2.
- 2026-10-12cache em arrays1 diacabeças em paralelo e a capacidade do cache exigida no tipo.
- 2026-10-13Bend 2.0.37atualização do compilador e comparação pública de desempenho.
primeiro, o que esse nome quer dizer
Llama, aqui, é a arquitetura: a organização das operações que transformam os tokens de entrada nos escores do próximo token. Os pesos que usei são os checkpoints públicos da família SmolLM2, identificados como HuggingFaceTB/SmolLM2-*. Um checkpoint é o conjunto de números que um treinamento já encontrou. Escrever as operações em outra linguagem permite usar esses números sem refazer o treinamento.
Isso importa para ler o resultado. Não treinei um modelo Llama neste projeto, e o nome não diz que baixei os pesos de um modelo da Meta. Implementei a inferência, que é calcular a resposta com os pesos já prontos. O programa recebe o texto, lê os pesos preparados e produz tokens. Não há atualização desses pesos durante a geração que este post descreve.
Também não é qualquer modelo que tenha “Llama” no nome. A preparação confere uma combinação específica: SwiGLU, ausência de biases, RoPE comum e pesos de saída compartilhados com o embedding. Cada uma dessas condições corresponde a uma peça do programa. Um modelo com outra variante de posição, por exemplo, não fica suportado só porque suas matrizes cabem na memória. Compatibilidade de arquitetura precisa vir antes da comparação de resultados.
O bend-ml entra como base dessas contas. O llama.bend importa os pacotes de tensores e de tensores em arrays, e adapta a tokenização a partir do trabalho com GPT-2. O pacote novo reúne a configuração, os pesos de uma camada, a sequência de camadas, o cache e as leis que relacionam essas partes. Assim dá para discutir o modelo inteiro sem reimplementar o produto de matriz por vetor a cada camada.
No código público, as revisões dos três checkpoints ficam fixadas em reference/models.py. Essa distinção entre código, configuração e pesos ajuda a entender o resto do post: o código diz como calcular; a configuração diz os tamanhos e algumas escolhas da arquitetura; os pesos são os números aprendidos. Para reproduzir um resultado, as três coisas precisam corresponder.
do texto ao próximo token
Um modelo desse tipo não recebe uma frase como uma string. Primeiro, o tokenizer divide o texto em unidades de um vocabulário e devolve seus identificadores, números inteiros. Uma unidade pode ser parte de uma palavra, um espaço junto de um pedaço de palavra ou outro fragmento. Não dá para contar palavras e concluir quantos tokens uma frase terá: isso depende das regras e do vocabulário daquele modelo.
O identificador serve de endereço para o embedding, uma tabela de vetores. Um vetor é só uma sequência de números; no 135M, são 576 números por token. Buscar a linha correspondente ao identificador dá a representação inicial daquela posição. Depois ela atravessa as camadas do decoder, cada uma usando seus pesos e o histórico permitido para transformar essa representação. No fim há outra normalização e uma projeção para o vocabulário.
Essa última projeção produz um número por token possível: os logits. São escores, ainda não probabilidades. A demo usa a escolha mais simples, chamada greedy: pega o identificador do maior escore. Esse token passa a fazer parte do texto e entra no próximo passo. Repetir isso gera a sequência. O prompt precisa ser processado antes, para que os caches de todas as camadas tenham as posições que já apareceram.
O tokenizer do SmolLM2 exigiu uma adaptação própria. Reutilizar o do GPT-2 sem mudanças não dava os mesmos IDs. O pré-processamento separa dígitos individualmente, inclusive os dígitos Unicode reconhecidos pela referência; a numeração dos merges é outra. Um merge é a regra que junta dois fragmentos para formar uma unidade maior no BPE. Acertar essas regras vem antes de investigar qualquer diferença no modelo: entradas distintas produzem contas distintas.
Há um detalhe menos bonito que também precisa aparecer: alguns bytes não têm token nesse vocabulário e são descartados pelo pré-processamento para corresponder à referência. Por isso, uma lei sobre desfazer merges do BPE não implica que qualquer sequência de bytes atravesse esse tokenizer completo e volte intacta. O componente matemático e a convenção concreta de um modelo são partes diferentes do caminho. A adaptação e os testes estão no tokenizer em Bend e nas notas públicas de 9 de outubro.
o que uma camada calcula
Imagine acompanhar o vetor de uma posição. Uma camada precisa consultar as posições anteriores e depois transformar o resultado. No llama.bend, isso aparece em dois blocos: atenção e uma rede de projeções chamada MLP. Antes de cada bloco há uma RMSNorm; depois há uma soma com o vetor que entrou naquele bloco. É essa soma, a conexão residual, que conserva um caminho direto para a representação anterior enquanto a camada acrescenta uma transformação.
normalizar antes de consultar
A RMSNorm ajusta a escala dos números. Ela eleva as componentes ao quadrado, calcula a média e usa a raiz dessa média para obter um fator de escala. Um pequeno eps entra antes da raiz, e cada componente recebe também um ganho aprendido. Não é subtrair a média do vetor: o que essa operação usa é a média dos quadrados. A implementação mantém a ordem de multiplicações da referência, porque em ponto flutuante a ordem pode mudar os últimos bits.
A atenção começa projetando o vetor normalizado em três outros: query, key e value, ou Q, K e V. Dá para ler a query como o que a posição procura, a key como o que permite comparar cada posição com essa procura, e o value como a informação que será combinada. Essa é uma forma de acompanhar a conta, não uma tradução literal do significado de cada número aprendido.
A query é comparada com as keys disponíveis por produtos escalares. A conta recebe um ajuste de escala e passa por softmax, que transforma os escores em pesos positivos cuja soma é um, na descrição matemática da operação. Esses pesos combinam os values. Assim a saída depende das posições consultadas com intensidades diferentes. O modelo faz isso em várias cabeças, partes menores do vetor que mantêm consultas separadas; depois junta seus resultados e aplica uma projeção de saída.
a transformação depois da atenção
Depois da atenção e da primeira soma residual, vem outra RMSNorm e o MLP. Neste caso ele usa SwiGLU. Duas projeções, gate e up, recebem o mesmo vetor. A primeira passa pela função silu; o resultado é multiplicado componente a componente pela segunda. Uma terceira projeção, down, devolve o tamanho usado pelo restante do modelo. O vetor resultante entra na segunda soma residual.
Uma maneira útil de ler gate é como uma transformação que modula a outra, em vez de apenas encadear duas matrizes. Os nomes não significam uma decisão binária de abrir ou fechar: o valor é numérico. No 135M, o vetor de 576 componentes é projetado para 1536 no interior do MLP e volta a 576. Essa volta é necessária para somar o resultado ao caminho residual, posição a posição.
A função pública block permite seguir esse percurso inteiro. Ela devolve o vetor, o cache atualizado, os pesos e um registro dos intermediários. Isso ajuda a comparar uma camada por dentro: se o resultado final divergir, dá para olhar a primeira normalização, Q/K/V, a atenção e o MLP separadamente. Uma frase gerada não conta em qual dessas contas uma diferença começou.
nove consultas, três conjuntos de chaves
No desenho mais direto de atenção com várias cabeças, cada cabeça de queries tem uma cabeça de keys e uma de values correspondentes. Mas elas não precisam existir em igual quantidade. O 135M tem nove cabeças de queries e só três de keys e values. Cada conjunto de keys e values atende a três consultas diferentes. Isso é grouped-query attention, ou GQA: agrupar consultas para compartilhar K e V.
Compartilhar não torna as queries iguais. Cada uma continua produzindo seus próprios escores e sua própria combinação dos values. O que muda é o conjunto consultado. Para um mesmo tamanho de cabeça, guardar menos conjuntos K/V também reduz a quantidade de números no cache em relação a guardar nove deles. Essa relação não é uma promessa de redução proporcional no tempo do programa inteiro: os outros produtos continuam existindo.
O risco está no endereço: fazer uma query ler a cabeça K/V vizinha continua sendo uma conta com números e pode não provocar um erro de execução. No pacote, as queries são organizadas em grupos, e cada grupo caminha junto de seu conjunto K/V. A lei gqa_head demonstra que essa organização escolhe a mesma cabeça que a divisão usada pelo mapeamento da referência.
Em termos simples: se há g queries por grupo, a query de índice j·g + i, com i menor que g, pertence ao grupo j. A lei prova que dividir esse índice por g dá j. O detalhe útil é o “para qualquer”: ela não enumera apenas as nove queries do 135M. O argumento vale para os índices que satisfazem essas condições; as configurações concretas entram como casos dessa relação.
No 360M são quinze queries para cinco conjuntos K/V, de novo três por grupo. No 1.7B são 32 para 32: g = 1. Esse caso é atenção multi-head comum, representada pela mesma configuração geral. As leis de quantidade de grupos e de arrays completam a parte estrutural, conferindo que o agrupamento e a criação do cache têm as contagens esperadas. O README do pacote explica as leis e o código contém os enunciados e as provas.
posição como rotação
Até aqui expliquei como comparar queries e keys, mas falta dizer em qual posição cada uma está. No llama.bend essa informação entra pelo RoPE, os rotary position embeddings. A operação gira pares de componentes das queries e keys por um ângulo que depende da posição e da frequência daquele par. Os values não passam por essa rotação. Os pesos aprendidos continuam os mesmos; a rotação muda conforme a posição processada.
Pense em duas coordenadas como a ponta de uma seta num plano. Girar essa seta muda suas coordenadas sem precisar acrescentar uma componente nova ao vetor. Pares diferentes usam frequências diferentes. Quando queries e keys rotacionadas se encontram no produto escalar, a posição já participa da comparação. O desenho abaixo só ilustra a ideia de rotação: os ângulos e as setas não são uma medição das ativações de um prompt.
A forma de formar esses pares precisa corresponder ao checkpoint. Aqui a cabeça é dividida em duas metades: a componente de índice i da primeira se combina com a de índice i da segunda. Não são simplesmente pares vizinhos percorrendo o vetor inteiro. A configuração guarda half, metade do tamanho da cabeça, e calcula o tamanho total como 2·half. Isso torna o tamanho par por construção, em vez de depender de um comentário dizendo para escolher um número par.
A lei head_split diz algo preciso e mais restrito que “RoPE está correto”: cortar uma lista nessas partes e juntá-las devolve a lista original, na mesma ordem. Ela evita que a reorganização perca ou mova componentes. Não prova a precisão do seno, do cosseno ou das multiplicações em F32. Esses resultados entram nas comparações numéricas da camada. Uma prova de que as peças voltam ao lugar não é uma prova de que todos os números calculados com elas correspondem à referência.
Os três modelos usam cabeças de 64 componentes. O 1.7B muda também a base do RoPE, theta: 130000, contra 100000 nos dois menores. Esses valores entram no cálculo das frequências, não no tamanho das matrizes. É um exemplo de diferença de configuração que continuaria existindo mesmo se fosse possível reaproveitar algum shape. A implementação de RoPE e as configurações deixam essas escolhas explícitas.
a configuração chega aos tipos dos pesos
Uma configuração comum seria só um conjunto de números que o programa lê antes de alocar memória. Aqui ela participa também dos tipos. Cfg guarda a quantidade de cabeças K/V, a quantidade de queries por grupo, metade do tamanho da cabeça, a largura do MLP, o número de camadas, o vocabulário e os parâmetros da normalização e da posição. O tipo dos pesos de uma camada é LW<c>: ele depende daquela configuração c.
type Cfg is Data:
Cfg{kv: Nat, g: Nat, half: Nat, f: Nat, layers: Nat, vocab: Nat, eps: F32, theta: F32}Desse registro saem três contas: cabeças de queries = kv·g; largura do vetor = kv·g·2·half; largura de K ou V = kv·2·half. No 135M, isso dá nove cabeças, 576 componentes no vetor e 192 em K e V. Cada matriz tem uma linha por componente de saída e uma coluna por componente de entrada, a convenção usada para carregar os pesos. Não basta guardar a quantidade total de números: as duas dimensões têm papéis diferentes.
| configuração | 135M | 360M | 1.7B |
|---|---|---|---|
| cabeças Q / K/V | 9 / 3 | 15 / 5 | 32 / 32 |
| largura do vetor | 576 | 960 | 2048 |
| largura de K ou V | 192 | 320 | 2048 |
| largura interna do MLP | 1536 | 2560 | 8192 |
| camadas | 30 | 32 | 24 |
O teste mais fácil de entender é tentar trocar Q e K do 135M. A matriz de Q é Bands<576n, 576n>; a de K é Bands<192n, 576n>. Bands é a representação de matrizes em bandas do bend-ml, com linhas e colunas no tipo. O trecho abaixo, extraído do teste público, reconstrói a camada com as duas matrizes invertidas. É um programa que deve ser rejeitado, não um exemplo de uso correto.
def swap(lw: M.LW<M.smollm2_135m()>) -> M.LW<M.smollm2_135m()>:
match lw:
case M.LW{ln1, q, k, v, o, ln2, gate, up, down}:
M.LW{ln1, k, q, v, o, ln2, gate, up, down}O campo Q exige 576 linhas e recebe uma matriz com 192. O erro aparece antes de calcular qualquer token. Não depende de escolher um prompt que revele o problema ou de inspecionar o texto depois. Mas a garantia termina nas dimensões expressas pelo tipo: trocar duas matrizes com o mesmo shape não vira automaticamente um erro de tipos. Nem o tipo consegue descobrir sozinho que um arquivo com o tamanho certo contém pesos de outra origem.
As leis de layout complementam isso contando os valores esperados: 134515008, 361821120 e 1711376384 para os três checkpoints. O loader confere o tamanho de cada arquivo contra o shape esperado e para se não corresponder. São verificações de organização e quantidade, junto das revisões fixadas e dos testes; não uma prova de autenticidade semântica de qualquer sequência de bytes. Os tipos dos pesos e as leis de layout mostram exatamente onde essas fronteiras ficam.
um cache que sabe quanto já foi escrito
Para gerar a próxima posição, a atenção volta a consultar keys e values das posições anteriores. Recalcular tudo desde o início repetiria trabalho. O KV cache guarda esses resultados por camada. Ele não guarda “a resposta” pronta para reutilizar: guarda representações de cada posição, e cada nova query ainda precisa consultar o histórico. Por isso, ter cache não transforma a atenção inteira numa operação de custo constante.
Há duas perguntas separadas: quais posições existem e quanto espaço existe para elas? O tipo KV<cap, t> carrega ambas. cap é a capacidade reservada em posições; t é quantas já foram escritas. Antes de processar a posição de índice t, existem as posições de zero até t − 1. O bloco escreve a key e o value da posição atual e devolve um cache de tipo KV<cap, t + 1>. Só então a atenção consulta de zero até t, incluindo a posição atual.
Essa é a parte causal: a posição atual só consulta seu próprio passo e o passado, sem ler uma posição futura. causal e read_len relacionam a leitura a exatamente t + 1 keys e escores. A capacidade física pode ser maior. Inicializar espaço sobrando não faz dele texto anterior, e confundir esses dois tamanhos seria um jeito de ler posições que não fazem parte da sequência.
Para escrever, o programa precisa ainda de uma prova de que t é menor que cap. kv_room liga esse limite à quantidade de slots dos arrays, incluindo o tamanho de uma cabeça. A prova de espaço entra obrigatoriamente em KV.push, block e forward. Assim o contrato não fica só numa lei que alguém pode esquecer de aplicar: as funções que avançam o modelo pedem esse argumento.
O teste de capacidade tenta uma terceira escrita num KV<2n, 2n>. Já existem duas posições e só há capacidade para duas. A chamada precisaria provar 2 < 2; o checador rejeita a tentativa. Isso importa especialmente porque os índices dos arrays do Bend podem dar a volta: estar fora da capacidade poderia sobrescrever um slot anterior. A API exige o limite antes de chegar a essa escrita.
As provas são apagadas na compilação. Elas servem para aceitar ou rejeitar o programa, sem uma árvore de justificativas para percorrer a cada token. Isso não elimina alocação, leitura de memória ou produtos de matrizes; elimina o custo em execução da evidência formal. A descrição completa está nas leis do cache e nas notas da mudança de API.
as provas não fizeram a soma ficar certa
Rodar os outros dois tamanhos era uma maneira concreta de testar se a configuração realmente bastava. O 1.7B trouxe um problema que não era de shape: o teste da camada 15 falhou em intermediários da atenção e do MLP. A saída final da camada ainda estava perto da referência, mas algumas partes internas passavam do limite de comparação. Olhar só o último vetor teria escondido a diferença.
A causa apareceu na primeira RMSNorm. Ela precisava somar 2048 quadrados, com componentes de escalas muito diferentes. F32 guarda números com precisão finita. Se uma soma acumulada já é grande, acrescentar uma parcela pequena pode perder parte dela no arredondamento. Repetir essa operação milhares de vezes não é numericamente igual a somar números reais com precisão infinita, mesmo que todas as dimensões estejam corretas.
A versão inicial acrescentava cada quadrado a um único acumulador. A correção foi usar uma soma em árvore: somar pares vizinhos, depois pares dos resultados, até chegar ao total. pair_sums e tree_sum fazem isso. Não muda quais componentes entram na normalização, mas muda a ordem dos arredondamentos. É justamente o tipo de mudança em que um programa estruturalmente igual pode deixar de produzir os mesmos bits.
O resultado público dá uma comparação específica para essa primeira normalização da camada 15 do 1.7B: em relação à execução em float64 usada nas notas, o erro reportado do Bend caiu de 4.6e-6 com a soma sequencial para 1.5e-7 com a soma em pares. São números daquele caso, não uma garantia para qualquer vetor, qualquer ordem ou qualquer hardware. O ponto é que a mudança foi confrontada com uma referência numérica, além de continuar passando no checador.
Isso também impede tratar PyTorch como uma definição de número real. Ele calcula em ponto flutuante também. Comparar com transformers responde se a minha implementação acompanha aquela referência, sob versões e escolhas fixas; uma comparação em maior precisão ajuda a investigar uma divergência particular. Não transforma cada diferença em bug nem cada concordância em prova de exatidão. O relato e os resultados dessa correção estão nas notas sobre RMSNorm.
mudar o cache mudou o custo
Guardar K e V evita recalcular suas projeções, mas a maneira de guardá-los também custa. A primeira representação mantinha o histórico em listas. A atenção precisava reconstruir linhas do cache, reorganizá-las por cabeça e montar resultados intermediários enquanto percorria as posições. Quanto mais histórico, mais trabalho de listas havia em cada novo passo. Reutilizar os números não bastava para reutilizar sua organização.
A troca foi para arrays planos, com um array de keys e um de values por cabeça K/V em cada camada. A nova posição é escrita no espaço reservado para ela. Os produtos da atenção leem as posições válidas diretamente nesses arrays, com os strides apropriados. Um stride é o salto entre elementos na memória: ele permite olhar os mesmos números como linhas ou colunas sem materializar uma transposição em listas a cada token.
Depois veio a divisão entre cabeças K/V para executar grupos em paralelo. Como cada grupo consulta seu conjunto de arrays, dá para entregar conjuntos diferentes a tarefas diferentes e juntar os resultados na ordem dos grupos. Isso se soma aos produtos de pesos em bandas herdados do bend-ml. São lugares diferentes para dividir trabalho, com custos diferentes; mais tarefas não significam automaticamente menos tempo.
O resultado histórico de 12 de outubro ajuda a separar os efeitos. Com Bend 2.0.36 e tensor-array 0.1.7.0, no 1.7B gerando 128 tokens com 16 threads, a versão com listas levou 1692 ms por token. Arrays com as cabeças em sequência deram 427 ms; arrays com as cabeças em paralelo, 385 ms. O ganho grande daquela comparação veio de mudar a representação do cache. Paralelizar as cabeças acrescentou outro ganho naquele caso.
Esses números pertencem àquela comparação entre três versões, identificadas no benchmark público. Eles não devem ser misturados com a tabela final do dia 13 para inventar uma regressão ou um ganho do compilador. Também não são uma regra para uma thread: abrir e juntar tarefas tem custo, mesmo quando não há núcleos disponíveis para aproveitá-las. A versão medida no dia 13 mantém cabeças em sequência com até duas threads e as paraleliza acima disso.
O cache em arrays ainda lê as posições anteriores. Em uma geração de 512 tokens do 1.7B com 16 threads, os tempos publicados do primeiro e do último quarto foram 427 e 452 ms por token. Há crescimento medido; ele ficou pequeno em relação ao problema anterior de listas, não desapareceu por uma propriedade matemática do cache. “Ficou mais plano neste intervalo” é uma descrição mais fiel que “o contexto deixou de custar”.
o que eu conferi, e o que cada teste diz
Uma geração que parece plausível é uma demonstração fraca de uma implementação. Mesmo escolher o mesmo token só mostra que o maior escore continuou no mesmo lugar. Dois vetores de logits podem ser diferentes e ter o mesmo máximo. Por isso o repositório separa a comparação dos números, a escolha de token e o texto decodificado, além dos testes da camada e do tokenizer.
O teste de forward usa 11 prompts, com 88 posições ao todo, e compara os logits de cada posição com transformers 5.19 em F32 e atenção eager. “Eager” identifica a implementação de atenção escolhida na referência; trocar esse caminho pode mudar a ordem das operações. A medida reportada divide a maior diferença absoluta entre os logits pelo maior valor absoluto do vetor de referência. Ela não é o erro relativo de cada componente individual.
| resultado publicado | 135M | 360M | 1.7B |
|---|---|---|---|
| pior erro dos logits nessa medida | 2.1e-5 | 4.8e-5 | 8.3e-5 |
| argmax nas 88 posições | igual | igual | igual |
| 32 tokens greedy em 12 prompts | iguais | iguais | iguais |
| texto decodificado nesses prompts | igual | igual | igual |
As linhas de geração são outro conjunto: 12 prompts, com 32 tokens gerados por caso. O teste confere os IDs do prompt, os IDs gerados e o texto, além dos logits dos tokens escolhidos dentro da tolerância. Não são 12 prompts usados para calcular a primeira linha da tabela. Os dois scripts públicos deixam essa separação explícita: forward examina o vetor de logits; geração examina a sequência produzida.
A tokenização também é conferida separadamente. O resultado publicado registra os mesmos IDs em 68 textos fixos e 600 aleatórios; a decodificação foi comparada em 1500 sequências aleatórias de IDs. São execuções ampliadas documentadas, e não a afirmação de que toda chamada padrão do script roda exatamente essas quantidades. Comparar a decodificação isoladamente importa porque sequências arbitrárias de IDs podem formar bytes que não são UTF-8 válido.
As 21 leis ficam numa categoria diferente. Elas tratam de divisão de cabeças, associação entre Q e K/V, quantidade de grupos e arrays, leituras causais, limite de escrita e layout, apoiadas por lemas aritméticos. O pacote não usa @unsafe, ?TODO ou axiomas para substituir essas provas. Mas os vetores entre camadas ainda são listas sem o comprimento no tipo, e as operações F32 continuam verificadas por testes. Dizer “toda a inferência foi formalmente provada” ultrapassaria o que está implementado.
Também existe uma exceção pública à frase “todos os sistemas dão os mesmos tokens”. Na comparação longa do 360M, o texto do llama.cpp divergiu depois de aproximadamente 340 tokens. O benchmark registra que a sequência do llama.bend foi conferida com transformers. Isso não invalida as comparações curtas da tabela, mas delimita o alcance delas. Mesmos tokens nas execuções testadas não são uma garantia universal para qualquer duração, implementação ou prompt.
os números ainda mostram a distância
A comparação final publicada foi medida em 13 de outubro de 2026, num Intel Core Ultra 7 155H com 32 GB de RAM, na CPU e em F32. O código medido é o commit 3ea435a, com tensor-array 0.1.7.0 e Bend 2.0.37. A revisão usada para documentar este post é posterior e contém esse relatório; não estou apresentando a tabela como uma nova medição feita hoje.
As referências são transformers 5.19 com PyTorch 2.14.1, llama.cpp no commit 23b0202 usando GGUF F32 e candle no c68b249, também F32. A tabela abaixo mostra milissegundos por token gerado, separando uma thread e 16 threads. O 135M e o 360M geram 32 tokens; o 1.7B, 128. O custo de carregar os pesos e processar o prompt fica fora dessa métrica. Os resultados completos estão em BENCHMARK.md.
| modelo e geração | sistema | 1 thread | 16 threads |
|---|---|---|---|
| 135M · 32 tokens | llama.bend | 121 | 76.7 |
| 135M · 32 tokens | transformers | 26.3 | 21.1 |
| 135M · 32 tokens | llama.cpp | 23.7 | 14.0 |
| 135M · 32 tokens | candle | 26.6 | 28.8 |
| 360M · 32 tokens | llama.bend | 283 | 133 |
| 360M · 32 tokens | transformers | 57.1 | 40.0 |
| 360M · 32 tokens | llama.cpp | 63.1 | 28.3 |
| 360M · 32 tokens | candle | 71.6 | 74.3 |
| 1.7B · 128 tokens | llama.bend | 1203 | 492 |
| 1.7B · 128 tokens | transformers | 231 | 132 |
| 1.7B · 128 tokens | llama.cpp | 324 | 101 |
| 1.7B · 128 tokens | candle | 292 | 295 |
O 1.7B exige uma ressalva presente no próprio relatório: os 492 ms carregam a variação do tempo de carregamento na métrica comparativa publicada. O relógio interno do gerador marcou 426 ms por token com 16 threads. São medidas diferentes, e substituir uma pela outra na tabela esconderia essa diferença. O tempo interno ajuda a ler a dispersão; não autoriza escolher só o número mais favorável para comparar sistemas.
Bend 2.0.37 inclui a correção do compilador comentada no post anterior, mas este projeto não ganhou velocidade por causa dela na comparação publicada. Os tempos internos do 1.7B com 16 threads foram 423 ms em 2.0.36 e 426 em 2.0.37. A atualização importa como versão do ambiente; não vou atribuir a ela os ganhos que vieram de mudar o cache. Ter uma correção relevante no compilador e ganhar tempo neste programa são afirmações que precisam de evidências separadas.
esperar o primeiro token também conta
Para quem abre a demo, esperar os pesos entrarem na memória faz parte da experiência. O relatório mede também uma execução que carrega o modelo e gera um token. A tabela seguinte traz esse tempo total e o pico de memória residente com 16 threads. Ela não é uma medição isolada só do loader, nem o custo de cada token depois que o programa já está pronto.
| sistema | 135M | 360M | 1.7B |
|---|---|---|---|
| llama.bend | 4.4 s · 781 MB | 11.5 s · 2332 MB | 66.4 s · 6935 MB |
| transformers | 2.7 s · 1168 MB | 2.7 s · 2469 MB | 4.1 s · 10189 MB |
| llama.cpp | 0.2 s · 743 MB | 0.2 s · 1752 MB | 0.5 s · 8116 MB |
| candle | 0.2 s · 791 MB | 0.4 s · 2107 MB | 2.5 s · 9844 MB |
Carregar é a parte mais lenta do llama.bend. O caminho de leitura produz listas com uma célula por byte, e construir e percorrer essas listas tem custo. O pico de memória menor que algumas referências nessa tabela não compensa automaticamente mais de um minuto até o primeiro token do 1.7B. Também não é uma garantia geral de menor memória: o mesmo relatório registra pico de 8.4 GB para o 1.7B com uma thread.
Esses resultados deixam uma distância clara para llama.cpp e transformers. O cache em arrays resolveu um custo grande, mas não fez os produtos dos pesos nem a leitura dos arquivos desaparecerem. As medições descrevem essa máquina, essas versões e essas gerações. Não são projeções de velocidade em outro processador, com quantização ou com uma GPU. Este projeto executa na CPU e os números apresentados aqui usam F32.
rodar o que está publicado
O ponto de entrada está no repositório público e na página do projeto. Os comandos documentados começam preparando o ambiente, baixando e convertendo o checkpoint e conferindo os resultados. Para o 135M, o README lista Linux x86_64 ou WSL, clang, Python 3.14 e curl. O primeiro preparo também precisa de espaço para o ambiente Python e os arquivos do modelo; não é só o tamanho do executável Bend.
git clone https://github.com/nuxyel/llama.bend.git
cd llama.bend
make setup
make prep
make check
bend demo/gen.bend -o gen
./gen data/smollm2-135m "The capital of France is" 32make setup prepara as versões de ferramentas documentadas; make prep traz o modelo e escreve os arquivos que o programa Bend lê. make check confere as leis, os programas que devem ser rejeitados e as comparações com as referências. Não quer dizer que a inferência em Bend dependa de chamar Python a cada token: Python participa da preparação e da verificação. A geração do exemplo roda no executável compilado.
Para preparar e conferir outro tamanho, o comando público é make prep check MODEL=smollm2-360m, ou MODEL=smollm2-1.7b. O programa recebe o diretório correspondente na linha de comando. A mesma API também está publicada no BendHub como bend-ml-llama@0.1.0.0; a documentação do pacote descreve forward, block, a criação dos caches e as provas de espaço necessárias para avançar uma posição.
import bend-ml-llama@0.1.0.0/main.bend as MHá um detalhe na API que vem dos tipos afins: os produtos devolvem os pesos que receberam. Os arrays têm um dono, então calcular com uma matriz e continuar usando-a exige passá-la adiante explicitamente. block devolve LW<c> e forward devolve Model<c>. Isso explica por que uma chamada retorna mais que um vetor de logits. A estrutura dos resultados faz parte de como os pesos permanecem disponíveis para o próximo token.
O que está publicado ainda é uma implementação de inferência para modelos base, com escolha greedy, sem template de chat. Não equivale a abrir um assistente pronto para conversar. Também não inclui uma prova de todo valor intermediário nem suporte automático a qualquer variante da arquitetura. Essas limitações estão junto dos resultados porque mudam o que faz sentido esperar ao rodar a demo.
Para mim, a parte interessante deste estágio é poder apontar para erros específicos que já não passam pela API: Q e K incompatíveis no lugar errado, uma query ligada ao grupo errado no mapeamento provado, uma escrita sem espaço no cache. Ao mesmo tempo, a soma da RMSNorm precisou de investigação numérica e a geração continua perdendo em tempo para as referências. O código e os resultados permitem olhar as duas partes: o que ficou garantido na estrutura e o que ainda precisa ser medido e testado.
follow the next posts
Add this RSS feed to your feed reader to follow new posts. No account or email required.