por que acredito que Bend pode tomar o lugar do Python em machine learning

Quando escrevi o primeiro manifesto, eu ainda não tinha rodado o Bend2. Gostava da proposta de declarar uma propriedade do programa e exigir uma prova dela, mas não tinha experiência pra dizer como isso funcionava no trabalho de verdade.

Desde então, fiz o bend-ml, com as peças matemáticas; o llama.bend, pra executar modelos de linguagem; e o BendTorch, pra treinar redes neurais. Encontrei bug meu, bug do compilador, prova que não consegui fechar e GPU perdendo pra CPU. Também consegui expressar coisas que eu gostaria de poder exigir dos meus programas em Python.

Depois desse mês de trabalho, acho que Bend pode tomar o lugar do Python no desenvolvimento de sistemas de machine learning, da experimentação à manutenção. Ainda uso Python e tenho bons motivos pra isso. Mas agora tenho código rodando em Bend pra sustentar a aposta.

o que eu quero dizer com tomar o lugar

Quando você escreve um modelo em Python, boa parte do cálculo pesado acontece em outro lugar. Uma multiplicação de matrizes no PyTorch chama implementações preparadas para CPU ou GPU. Você descreve o cálculo numa linguagem e depende de uma infraestrutura enorme por baixo dela.

Isso funciona muito bem. Permite que alguém treine uma rede sem aprender a programar uma placa de vídeo. Se eu precisasse de um resultado amanhã, essa infraestrutura pesaria bastante na escolha.

A divisão aparece quando quero mudar uma operação lá embaixo. Posso combinar operações existentes em Python, e a documentação de extensão do PyTorch também contempla implementações próprias em C++ e CUDA. Há ainda Triton, que permite escrever cálculos para GPU com sintaxe baseada em Python, e torch.compile, que pode transformar partes do programa em código otimizado. A facilidade de usar uma operação pronta e o trabalho de construir essa operação continuam sendo experiências diferentes.

O que me interessa no Bend é poder atravessar essa distância mantendo o mesmo sistema de tipos e de leis. No meu código, a multiplicação, a atenção e a atualização dos pesos são funções em Bend. Posso descer até o cálculo que quero mudar e escrever, ali, uma propriedade que vou exigir dele.

A troca teria de compensar o aprendizado e a migração, inclusive no trabalho com dados e ferramentas existentes. Meu código ainda perde bastante para PyTorch nas medições que mostro adiante. Já consigo expressar e verificar certas propriedades, mas ainda não medi um ganho de produtividade que justifique a mudança.

peças que precisam encaixar

Uma rede neural é uma sequência de transformações de números. Cada etapa recebe uma quantidade de valores e produz outra. Dá pra pensar em peças com encaixes: uma saída de 128 posições precisa encontrar uma entrada que aceite 128.

Se eu conecto essa saída a uma camada que espera 64, o programa está errado antes de olhar qualquer dado. Gostaria de saber disso antes de carregar pesos, preparar uma GPU ou começar um experimento.

No bend-ml, coloquei as dimensões das matrizes nos tipos, que são as descrições dos valores aceitos pelas funções. Assim, a informação sobre o encaixe chega ao compilador. No BendTorch, isso também vale para a composição das camadas e para os formatos dos gradientes. Um dos testes de rejeição publicados tenta justamente conectar uma saída de 128 a uma entrada de 64: o compilador recusa essa composição.

Experimente mudar as dimensões abaixo. As colunas da primeira matriz precisam coincidir com as linhas da segunda.

SOME PROOFS FAIL
Error:
- expected : Mat<3n, 5n>
- observed : Mat<4n, 5n>

Com isso, evito escrever um teste para cada combinação de dimensões. Essa checagem impede um erro de encaixe; escolher um bom modelo e conferir o cálculo de cada camada continuam sendo outros problemas.

o ajuste também precisa estar certo

Treinar uma rede envolve medir seu erro e ajustar os pesos, os números internos que determinam sua resposta. Pra escolher o ajuste, calculo quanto cada peso influencia esse erro. Essa informação é o gradiente: como descobrir em que direção um botão deve girar pra melhorar o resultado.

O cálculo que volta pela rede, chamado backward, precisa corresponder ao cálculo que produziu a resposta. Um erro nessa volta pode deixar todas as dimensões certas e ainda assim ensinar a rede usando uma direção errada.

O PyTorch calcula gradientes automaticamente a partir das operações executadas. É uma das razões pra usá-lo. Ao escrever minhas próprias camadas, passei a ser responsável por esse trabalho e quis conferir a relação entre a ida e a volta.

Uma das leis do BendTorch trata dessa ida e volta numa camada linear, que multiplica a entrada pelos pesos. Ela exige que medir uma influência na saída ou transportá-la de volta até a entrada dê o mesmo resultado matemático. A lei fala de um modelo exato desse cálculo; a execução numérica do treinamento é conferida também por testes.

law adjoint:
  for w: List<&2, List<&2, Nat>>
  for g: List<&2, Nat>
  for +v: List<&2, Nat>
  {Spec.dotn(g, Spec.mv(w, v)) == Spec.dotn(Spec.mtv(w, g), v) : Nat}

Pode ignorar os detalhes da sintaxe. w representa os pesos, v uma entrada e g o sinal que chega na volta. A última linha escreve essa identidade algébrica, que fundamenta a fórmula usada para levar o gradiente até a entrada da camada.

O for diz que a relação vale para todos os valores descritos ali. Pra aceitar a prova, o checador precisa conferir um argumento geral. A especificação dessa lei usa listas; a compatibilidade entre dimensões vem dos tipos das camadas, separadamente.

Essa lei usa números naturais, Nat, num modelo matemático exato. O treinamento usa números com arredondamento, F32. Pra conferir se a implementação numérica segue as fórmulas desse modelo, também dependo dos testes contra PyTorch. Eu não provei o treinamento inteiro.

No llama.bend, cheguei a ter um erro na soma da normalização mesmo com leis estruturais passando. A propriedade que eu tinha provado não dizia que aquela soma estava numericamente boa. Desde então, pergunto o que cada garantia cobre antes de confiar nela.

o que eu quero cobrar do código gerado

Quando peço a uma máquina que escreva código, quero poder cobrar essas mesmas propriedades da implementação que ela entrega. Era essa a preocupação do primeiro manifesto: o que eu continuo mantendo quando a máquina escreve uma parte cada vez maior do programa?

Pra mim, uma parte importante é a descrição do comportamento esperado. Se uma camada precisa preservar um formato ou obedecer a uma relação matemática, quero que isso fique escrito de um jeito que outra ferramenta possa conferir.

Continuo revisando e testando o código. Com a prova, uma mudança que altera a propriedade declarada também precisa enfrentar o checador. Tenho mais um critério verificável pra decidir se aceito a implementação.

Também posso escrever uma lei fraca ou formalizar a coisa errada. Escolher uma propriedade relevante exige entender o problema. E continuo dependendo do checador, do compilador e do runtime, o suporte que executa o programa, para confiar no resultado final.

Quero poder pedir uma otimização e continuar cobrando a mesma propriedade do código. Assim, parte do comportamento que espero fica registrada enquanto a implementação muda.

dividir trabalho sem mudar de linguagem

Se tenho dois cálculos independentes, quero poder escrever isso e deixar que a infraestrutura distribua o trabalho.

O Bend atual exige chamadas paralelas explícitas e divisões equilibradas. Eu preciso organizar o cálculo para aproveitar os núcleos; a linguagem não descobre sozinha uma boa divisão para qualquer programa.

Mesmo assim, gostei de poder trabalhar nessa organização dentro das próprias funções matemáticas. Em bend-ml depois do lançamento, contei como copiar pesos atrapalhava a execução em vários núcleos. Melhorar exigiu entender a representação dos dados, além de marcar trabalho como paralelo.

As versões rápidas e de GPU do BendTorch compartilham arrays por uma operação marcada @unsafe, fora das provas. Para carregar pesos, ainda uso um leitor temporário em outra linguagem. Preciso confiar nessas partes também. A matemática está em Bend, com essas exceções na implementação completa, descritas no README público.

A possibilidade de compilar também para JavaScript me interessa como forma de levar o cálculo a outro ambiente. Essa portabilidade não garante resultados numericamente idênticos: mudar a ordem de uma soma pode mudar o arredondamento, como explica a documentação de precisão numérica do PyTorch. As comparações em que obtive bits iguais valem para aquelas execuções verificadas.

o preço que ainda estou pagando

Na medição de 18 de outubro, registrada no benchmark público, comparei o tempo por passo de ajuste dos pesos do SmolLM2 de 135 milhões de parâmetros, os números ajustados no treinamento. Cada lote tem dois trechos de 128 tokens, unidades de texto que o modelo processa, e usa AdamW, o algoritmo de atualização. Todos começam dos mesmos pesos e recebem os mesmos dados.

Máquina: Intel Core Ultra 7 155H, 32 GB, Linux. Versões: Bend 2.0.37, clang 23.1.3, Python 3.14.8 e PyTorch 2.14.1. São medianas de três rodadas alternadas, com a máquina ociosa, medindo o laço de treinamento sem carregamento nem compilação. Há uma diferença no protocolo: BendTorch mede dois passos sem aquecimento, incluindo a preparação do estado do otimizador no primeiro; os outros sistemas medem três passos após dois de aquecimento. Nesse teste, as perdas, que medem o erro do modelo, são comparadas com uma tolerância numérica definida no benchmark.

Nesse recorte, BendTorch levou aproximadamente 5,8 vezes o tempo do PyTorch em execução direta. O README registra uma correção posterior de atenção, medida em 21/10: 4,0 segundos contra 0,93 segundo, ainda cerca de 4,3 vezes o tempo. São medições distintas; a segunda não substitui células da primeira tabela. Esses resultados descrevem esse trabalho, nessa máquina, e não estabelecem uma proporção geral entre as ferramentas.

Minha execução em GPU também continua perdendo para a CPU nos tamanhos medidos. Pra aproveitar bem a placa, ainda preciso resolver os custos de execução e de acesso à memória que encontrei.

Tem ainda o cotidiano: preparar dados, carregar formatos existentes, investigar problemas e entender tipos compridos. Python oferece uma quantidade enorme de bibliotecas, exemplos e pessoas que já passaram por essas dificuldades. Essa experiência acumulada faz parte da ferramenta que Bend teria de substituir.

Ainda estou tentando descobrir quanto as vantagens de Bend podem compensar o tempo de aprendizado e as conveniências que perco ao sair de Python.

por que eu continuo

Depois desse mês, consigo escrever matemática, executar um modelo e treinar uma rede na mesma linguagem, exigindo que algumas peças encaixem e que algumas relações matemáticas sejam provadas. Quando mudo a implementação, posso voltar a cobrar essas propriedades. Gostei de poder desenvolver uma operação e declarar o que ela deve preservar no mesmo lugar.

Pra eu escolher Bend num trabalho concreto, gostaria de conseguir implementar uma operação de um modelo de linguagem, declarar uma propriedade relevante dela, carregar os dados necessários e treinar e avaliar o modelo dentro do prazo e dos recursos daquele projeto. Ainda encontro obstáculos nesse percurso, sobretudo na integração com dados e no quanto as garantias alcançam o código realmente executado. Também quero ver outras pessoas construindo coisas com isso, sem depender das soluções que fui acumulando no meu projeto.

Uso Python porque ele resolve o meu trabalho. Em Bend, encontrei uma maneira de cobrar mais do código que escrevo, e é por isso que sigo construindo esses projetos. Se conseguir fazer isso com desempenho e bibliotecas que atendam ao trabalho do dia a dia, vejo motivo pra escolher Bend em projetos que hoje faria em Python.