Introdução
Raciocínio de IA em matemática
Durante a maior parte da era do aprendizado profundo, a relação entre modelos de linguagem de grande escala e a matemática foi desconfortável: sistemas que se destacavam na geração de linguagem natural permaneciam pouco confiáveis em raciocínio de múltiplas etapas e matemática formal. Isso mudou rapidamente após 2024, quando sistemas de fronteira alcançaram desempenho de nível olimpíaco e começaram a se integrar diretamente com ambientes de verificação formal, como o Lean.
Mais interessante do que a progressão nos benchmarks em si, porém, é o que essa capacidade significa para os matemáticos em atividade. Terence Tao se tornou uma das vozes mais claras a articular o papel emergente da IA na pesquisa matemática. Em um artigo de janeiro de 2025 nos Notices of the American Mathematical Society sobre prova assistida por máquina, e depois por meio da divulgação de uma formalização flexível de seu livro Analysis I em Lean, Tao argumentou não que os modelos de linguagem haviam superado os matemáticos, mas que eles se tornaram colaboradores úteis. Seu valor está em reduzir a sobrecarga em torno da pesquisa: buscar literatura, verificar argumentos padrão, formalizar definições, escrever pequenos experimentos computacionais e testar se uma abordagem vale a pena ser perseguida. Em 2023, Tao já havia usado o ChatGPT junto com o Lean em trabalhos relacionados à formalização de aspectos de uma prova da Conjectura Polinomial de Freiman–Ruzsa.
A mudança relevante, portanto, não é meramente que os sistemas de IA podem resolver problemas matemáticos mais difíceis, mas que eles são cada vez mais capazes de operar em raciocínio formal, manipulação simbólica, geração de código e verificação dentro de um fluxo de trabalho unificado.
Raciocínio de IA em programação
A trajetória na engenharia de software é estruturalmente semelhante à da matemática, embora mais visível porque seus resultados são código incorporado, e não provas escritas. A mudança é de autocompletar no estilo de sugestão para sistemas agênticos que inspecionam repositórios, planejam edições em múltiplos arquivos, executam testes e iteram sobre falhas. Benchmarks como o SWE-bench Verified agora avaliam esses sistemas em problemas reais do GitHub extraídos de repositórios de produção, e em 2026 os agentes de fronteira já resolviam uma fração substancial das tarefas de engenharia de software de nível de repositório em bases de código previamente não vistas.
Além dos benchmarks, o sinal industrial é cada vez mais difícil de ignorar. Em 2026, os agentes de programação haviam se integrado aos fluxos de trabalho diários das principais organizações de engenharia para tarefas de refatoração, depuração, migração e geração de testes. Executivos da Anthropic afirmaram publicamente que o Claude já estava escrevendo a maior parte do código interno da empresa, enquanto o relatório DORA State of AI-Assisted Software Development de 2025 do Google encontrou a adoção da IA amplamente associada a maior produtividade de engenharia, com a produtividade dependendo tanto da infraestrutura de testes e da disciplina operacional quanto do modelo específico utilizado.
Lidos em conjunto, as trajetórias da IA para matemática e da IA para programação estão convergindo. Quando fornecidos com um artigo de pesquisa e uma base de código, os sistemas de fronteira podem participar de um ciclo acoplado de raciocínio e implementação: interpretar algoritmos, identificar condições de corretude, traduzi-los em código de produção, gerar testes de regressão e iterar por execução e verificação. O restante deste artigo relata um experimento deliberado exatamente nesse fluxo de trabalho, com o humano definindo objetivos de alto nível, aprovando estratégias de implementação e intervindo principalmente quando os testes expunham falhas algorítmicas ou de convergência.
A aplicação: expansão estocástica da geração
O LightBDMM.jl é um pacote Julia da PSR desenvolvido nesse ambiente. Ele implementa o algoritmo de Decomposição de Benders Acelerada com Múltiplos Mestres (a-BDMM) que foi introduzido no artigo: An Integrated Progressive Hedging and Benders Decomposition with Multiple Master Method to Solve the Brazilian Generation Expansion Problem (A. Soares, A. Street, T. Andrade e J. D. Garcia). A estrutura do pacote, a implementação, os testes de regressão, a documentação e a configuração de integração contínua foram gerados pelo Claude Code, depois iterativamente corrigidos por meio de execução, testes, depuração e revisão humana. Extensões subsequentes — decisões de primeira fase de inteiros mistos (MIP) com linearização de penalidade quadrática e execução distribuída via MPI — foram adicionadas pelo mesmo assistente.
O projeto foi deliberadamente configurado como um experimento de baixa interação: até onde um sistema agêntico de fronteira consegue levar uma implementação de matemática aplicada quando o autor humano se limita a objetivos de alto nível e à revisão do estado final, em vez de orientação passo a passo? A corretude durante o ciclo foi ancorada não na revisão humana das etapas intermediárias, mas em um conjunto de validação independente de ground-truth, descrito adiante.
Já tínhamos implementações de decomposição de Benders e Progressive Hedging em repositórios separados com paralelização MPI e representação de inteiros mistos. Esses repositórios foram fornecidos ao agente de programação como implementações de referência para padrões arquiteturais, procedimentos de teste e estrutura de documentação.
A estrutura matemática subjacente à expansão estocástica da geração é o programa estocástico de dois estágios: uma decisão de investimento hoje (quais unidades construir, quais linhas reforçar, quais contratos assinar) é tomada antes que a incerteza do próximo ano (demanda, hidrologia, preços de combustível, produção renovável) seja observada; uma decisão de recurso operacional é então tomada assim que cada cenário se materializa.
O ciclo de raciocínio matemático
O aspecto interessante dessa implementação não foi a matemática simbólica ou a prova de teoremas automatizada. O desafio foi traduzir um artigo de pesquisa em um pacote de otimização funcional: compreender a estrutura algorítmica, planejar a implementação, identificar desafios de convergência e corrigi-los iterativamente por meio de testes e validação. Este experimento só foi significativo porque a corretude pôde ser verificada de forma independente: cada implementação foi continuamente validada em relação a soluções de equivalente determinístico e comportamento de benchmark, em vez de julgada apenas pela aparência plausível do código gerado.
O algoritmo a-BDMM aumenta o Benders clássico em dois eixos. Os múltiplos mestres substituem o mestre agregado único por um mestre por cenário, cada um ancorado em um problema de recurso diferente e compartilhando um pool de cortes comum, produzindo uma aproximação de recurso mais rígida em menos iterações. A aceleração por Progressive Hedging adiciona uma penalidade de consenso quadrática que direciona as decisões por cenário em direção a um valor comum.
O que torna o algoritmo um teste útil do raciocínio matemático de IA é que várias de suas condições de corretude não são óbvias a partir da descrição principal e seriam fáceis de ignorar em uma reimplementação ingênua:
- Um LP separado para o limite inferior após a ativação do PH. Uma vez que a penalidade de consenso esteja ativa, o limite inferior do algoritmo deve ser calculado a partir de um mestre que contenha apenas o termo Lagrangiano ws (xs – x) e não a penalidade quadrática. A implementação mantém um segundo pool de mestres de limite inferior exatamente para esse propósito.
- Se o PH for inicializado em um ponto degenerado — por exemplo, com todos os componentes de x iguais a zero —, o algoritmo pode convergir prematuramente para uma solução de consenso que, no entanto, é subótima.
Trabalhar com essas questões exigiu um processo iterativo de planejamento e depuração. Antes de escrever o código, o assistente gerou planos de implementação, identificou riscos de convergência e propôs estratégias de estabilização. Essas observações ainda exigiam verificação humana, mas trazê-las à tona cedo reduziu a probabilidade de propagar erros conceituais para a própria implementação.hem early reduced the likelihood of propagating conceptual mistakes into the implementation itself.
O ciclo de programação
O ciclo de programação foi o segundo estágio do processo e seguiu o mesmo protocolo de baixa interação. O Claude Code gerou a estrutura do pacote, a implementação, os testes de regressão, a documentação e a configuração de integração contínua, enquanto o autor humano forneceu apenas especificações de alto nível no início de cada ciclo e revisou as saídas finais. O ponto importante não era que a primeira implementação fosse correta, mas que o agente pudesse manter o repositório, o algoritmo e o feedback dos testes em contexto enquanto iterava em direção a uma implementação validada.
A implementação inicial já reproduzia corretamente a maior parte da estrutura algorítmica, incluindo o fluxo de trabalho da decomposição de Benders e o problema de teste de referência do newsvendor. O primeiro problema importante apareceu na lógica de agregação de cortes: a implementação inicialmente produzia valores objetivos incorretos porque as contribuições dos cenários não estavam sendo combinadas adequadamente. Após corrigir a agregação e a ponderação dos cortes, a variante BDMM convergiu rapidamente e produziu a solução esperada.
A falha mais interessante emergiu na variante acelerada a-BDMM. Todas as variáveis de estado foram inicializadas em zero, e os termos de penalidade do Progressive Hedging imediatamente direcionaram o algoritmo para o consenso em torno desse ponto inicial desinformado. Como resultado, o método ficou preso em uma solução subótima de “não fazer nada” e não conseguiu melhorar. A correção final foi introduzir uma fase de aquecimento na qual a decomposição explorou livremente por várias iterações antes de ativar as penalidades de consenso. Uma vez implementada, essa estratégia de estabilização resolveu o problema de convergência nos problemas de benchmark e correspondeu à intuição de que os mecanismos de acordo não devem dominar antes que cortes informativos tenham sido gerados.
A lógica do limite inferior, porém, exigiu um processo de depuração muito mais interativo. Depois que as penalidades quadráticas do PH se tornaram ativas, o cálculo do limite inferior não se comportou mais de forma consistente. Várias tentativas de implementação falharam de maneiras diferentes: usar o limite superior como proxy produziu convergência artificial na primeira iteração; usar os objetivos brutos dos mestres causou limites inferiores oscilatórios após a ativação do PH; e subtrair as penalidades quadráticas diretamente às vezes gerava estados inválidos com LI > LS.
Ao contrário do mecanismo de aquecimento, que emergiu com relativamente pouca intervenção humana, a fase do limite inferior exigiu interação repetida entre o autor humano e o assistente. O processo de depuração acabou se tornando menos sobre engenharia de software e mais sobre interpretação computacional do próprio algoritmo: determinar quais quantidades permaneciam limites inferiores válidos após a ativação do PH, como a convergência deveria ser medida e quais partes do objetivo aumentado eram artefatos de otimização, e não componentes do programa estocástico original. A implementação final acabou recuperando um procedimento correto de limite inferior descrito no artigo.
No geral, o processo de depuração foi notável porque a maioria das falhas não eram problemas sintáticos ou de engenharia de software, mas desafios algorítmicos relacionados ao comportamento de convergência e à interação entre os mecanismos de decomposição e consenso.
Validação em um modelo de expansão da geração
O solver foi testado em um problema de expansão estocástica da geração — quinze usinas candidatas, quarenta e cinco clientes industriais e cinquenta cenários estocásticos de ativação. Cada método foi executado até um gap relativo de 0,1% na mesma tolerância.
Figura 1 — Gap de otimalidade relativo em função do número de iterações para cada algoritmo no testbed de expansão da geração. O a-BDMM colapsa o gap em 5 iterações, contra 8 para o BDMM simples, 21 para o Benders de corte múltiplo e 177 para o Benders de corte único.
O resultado qualitativo de interesse é a contagem de iterações. O a-BDMM fecha o gap de limite em 5 iterações, contra 177 iterações para o Benders de corte único clássico na mesma instância — uma redução de aproximadamente 35 vezes. O BDMM simples (sem a aceleração do Progressive Hedging) fica entre os dois, com 8 iterações, isolando a contribuição da penalidade de consenso.
O conjunto de validação
Em um protocolo de desenvolvimento de baixa interação, o conjunto de validação não é meramente uma ferramenta de garantia de qualidade; é o mecanismo que torna o fluxo de trabalho viável. Cada teste de regressão no conjunto é resolvido tanto pelo LightBDMM.jl quanto pelo equivalente determinístico monolítico — a formulação extensiva exata do programa estocástico usada como solução de referência independente. Os resultados devem corresponder em cada instância de benchmark, portanto a implementação é continuamente verificada em relação a um ground-truth externo, e não apenas em relação à sua própria lógica interna. Isso serve como a contrapartida numérica do ciclo de raciocínio anterior: as condições identificadas durante o planejamento e a depuração são revalidadas computacionalmente em relação a um benchmark que não compartilha nenhuma da implementação do LightBDMM.jl. Qualquer desvio conceitual ou de implementação introduzido durante o ciclo de programação agêntica apareceria como uma incompatibilidade com o equivalente determinístico antes de chegar à produção.
O conjunto completo de regressão é executado em integração contínua a cada mudança de código proposta. No momento em que este texto foi escrito, o pacote mantém aproximadamente 98% de cobertura de código automatizada.
Perspectivas
O experimento não demonstra engenharia matemática autônoma. Demonstra algo mais restrito, mas operacionalmente importante: quando os algoritmos têm estrutura matemática forte, comportamento de benchmark e procedimentos de validação independentes, os sistemas de programação agêntica podem reduzir substancialmente o custo de engenharia de traduzir métodos de pesquisa em implementações de produção.
A otimização estocástica de dois estágios é um dos frameworks mais antigos e bem compreendidos em pesquisa operacional, e o a-BDMM em si existe na literatura desde 2021. A mudança relevante, portanto, não é a novidade do algoritmo, mas a redução no custo e no tempo necessários para ir do artigo ao software testado. Neste caso, a combinação de estrutura matemática, validação de equivalente determinístico e desenvolvimento assistido por IA tornou possível construir uma implementação de qualidade de produção — incluindo variantes de decomposição, testes de regressão, infraestrutura de benchmarking, integração contínua e documentação — tudo dentro de um único ciclo de desenvolvimento.
De forma mais ampla, domínios matematicamente estruturados com soluções de referência independentes parecem especialmente compatíveis com fluxos de trabalho de desenvolvimento agêntico. Quando grandes partes da tradução do artigo para a produção podem ser aceleradas e continuamente validadas, as organizações ganham a capacidade de experimentar, operacionalizar e implantar uma fração muito maior da literatura de otimização do que era anteriormente prático.
