🤖 machine learning

PPDL: LLM-Based Flows as Probabilistic Programs

Este artigo apresenta o PPDL, uma linguagem de programação probabilística que permite aos desenvolvedes quantificar e propagar incerteza através de fluxos de aplicações baseadas em LLM e experimentar técnicas de escalonamento de inferência sem modificar a lógica central, conforme demonstrado por meio de um agente de prova de teoremas para o provador Rocq.

Autores originais: Louis Mandel, Guillaume Baudart, Mandana Vaziri, Martin Hirzel

Publicado 2026-08-07

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Louis Mandel, Guillaume Baudart, Mandana Vaziri, Martin Hirzel

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando resolver um quebra-cabeça realmente difícil, mas em vez de fazê-lo sozinho, você tem um amigo superinteligente e criativo que pode conversar com você. Esse amigo é uma Inteligência Artificial chamada Modelo de Linguagem Grande (LLM). Eles são incríveis em escrever histórias, resolver problemas matemáticos e até escrever código de computador. No entanto, eles não são perfeitos. Às vezes, eles ficam confiantes sobre a resposta errada, ou podem inventar fatos que parecem reais, mas não são. Isso é chamado de "incerteza".

Imagine que você precisa resolver um problema realmente difícil que requer muitas etapas. Você pede um plano para o seu amigo de IA, depois pede para ele escrever o código baseado nesse plano, depois pede para ele verificar o código e assim por diante. Cada vez que você faz uma pergunta, a IA dá uma resposta, mas essa resposta pode ser um pouco instável. Se você encadear dez dessas respostas instáveis, o resultado final pode ser uma bagunça total. É como tentar construir uma torre de blocos de Jenga onde cada bloco é ligeiramente bambo; quanto mais alto você vai, maior a probabilidade de toda a estrutura desmoronar. Desenvolvedores e usuários costumam se sentir perdidos aqui: "Esta resposta está certa? O quanto temos de certeza? Devo confiar nela?"

Para corrigir isso, cientistas tentaram alguns truques. Uma ideia popular é o "escalonamento de inferência" (inference scaling). Pense nisso como pedir ao seu amigo de IA para tentar o mesmo quebra-cabeça dez vezes diferentes e ver qual resposta aparece com mais frequência. É como pedir a um grupo de amigos para adivinhar a resposta de um enigma e seguir a maioria dos votos. Mas aqui está o detalhe: fazer isso manualmente é bagunçado. Você tem que escrever um código especial para executar essas dez tentativas, acompanhar quais parecem boas e descartar as ruins. É como ter que construir uma nova fábrica toda vez que você quer assar uma fornada de cookies apenas para garantir que eles tenham um sabor bom. É complicado, caro e difícil de mudar se você quiser tentar uma forma diferente de assar.

A Grande Ideia do Artigo: A "Ficha de Pontuação Mágica"

Este artigo apresenta uma nova ferramenta chamada PPDL (Probabilistic Prompt Declaration Language). Você pode pensar no PPDL como uma "ficha de pontuação mágica" para fluxos de trabalho de IA. Em vez de apenas fazer uma pergunta à IA e obter uma única resposta, o PPDL permite que você escreva um programa que entende naturalmente que a IA pode estar incerta.

Veja como funciona em linguagem simples:

O Fluxo: Você escreve suas instruções para a IA como faria normalmente (ex: "Planejar o código", depois "Escrever o código", depois "Verificar o código").
O Fator Mágico: Você adiciona uma instrução especial chamada factor (fator). Isso é como uma ficha de pontuação onde você diz à IA: "Ei, se o plano parecer lógico, dê uma pontuação alta. Se o código tiver erros, dê uma pontuação baixa."
O Resultado: Quando você executa o programa, o computador não fornece apenas uma resposta. Ele executa todo o processo muitas vezes em paralelo (como se houvesse cem versões diferentes de você tentando o quebra-cabeça ao mesmo tempo). Ele usa sua "ficha de pontuação" para pesar os resultados. Se um caminho parece muito promissor, o computador foca mais energia nesse caminho. Se um caminho parece ruim, ele o descarta.

A parte mais legal é que você não precisa escrever o código complexo de "executar dez vezes" você mesmo. O PPDL cuida de todo esse trabalho pesado nos bastidores. Você apenas escreve a lógica uma vez, e o sistema descobre automaticamente a melhor maneira de explorar todas as possibilidades.

O Que Eles Descobriram

Os autores testaram essa ideia em vários desafios, desde a resolução de problemas matemáticos do ensino fundamental até a escrita de códigos de computador complexos e até a prova de teoremas matemáticos.

Melhor Precisão: Em seus testes, usar o PPDL com essas "fichas de pontuação" tornou a IA significamente mais precisa. Por exemplo, em um teste de matemática chamado GSM8k, uma IA padrão acertou cerca de 83,8% das respostas. Mas quando usaram o PPDL com um método chamado "Amostragem de Importância" (que é como uma maneira inteligente de escolher as melhores suposições), a precisão saltou para 93,7%.
O Jeito "Inteligente" Vence: Eles compararam diferentes maneiras de usar as fichas de pontuação. Às vezes, apenas tomar a "votação da maioria" (a resposta mais comum) funcionava bem. Mas, frequentemente, os métodos mais inteligentes (como a Amostragem de Importância e o Monte Carlo Sequencial) eram muito melhores. Esses métodos são como ter um detetive que não apenas conta votos, mas realmente investiga por que uma resposta é boa ou ruim, descartando caminhos ruins precocemente e focando nos bons.
O Estudo de Caso do Provador de Teoremas: Para testar o sistema ao limite, eles construíram um agente de IA para provar teoremas matemáticos usando uma ferramenta chamada Rocq. Esta é uma tarefa muito difícil, onde a IA tem que escrever uma prova, verificar se está errada e corrigi-la repetidamente. Eles descobriram que o método "inteligente" (Monte Carlo Sequencial) foi muito melhor para encontrar a prova correta do que apenas tentar suposições aleatórias repetidamente. Ele podia explorar muitos caminhos ao mesmo tempo e abandonar rapidamente aqueles que não estavam levando a lugar nenhum.

O Que Eles Não Afirmaram

Os autores são cuidadosos ao não dizer que isso é uma "solução mágica" para tudo. Eles apontam que as "fichas de pontuação" (os fatores) são tão boas quanto as informações que você coloca nelas. Se sua ficha de pontuação for ruim, o sistema não irá consertar magicamente. Além disso, embora este método torne a IA mais confiável, não significa que a IA seja subitamente perfeita; significa apenas que temos uma maneira muito melhor de medir o quão seguros devemos estar sobre a resposta.

Por Que Isso Importa

Este artigo sugere que, ao tratar fluxos de trabalho de IA como "programas probabilísticos" (programas que entendem a incerteza), podemos tornar as aplicações de IA muito mais confiáveis sem torná-las incrivelmente complicadas de construir. É como dar aos desenvolvedores um novo conjunto de ferramentas que lidam automaticamente com o negócio bagunçado de "tentar novamente e novamente", para que possam focar em construir coisas legais enquanto o computador descobre a melhor maneira de obter a resposta correta.

Resumo Técnico: PPDL: Fluxos Baseados em LLM como Programas Probabilísticos

Declaração do Problema

Construir aplicações confiáveis utilizando Grandes Modelos de Linguagem (LLMs) é um desafio devido à incerteza inerente e à falta de métricas de confiança nos outputs dos LLMs. Este problema é exacerbado em "fluxos" — sequências de múltiplas chamadas de LLM e interações com ferramentas — onde a incerteza se acumula ao longo do traço de execução. Embora técnicas de escalonamento de inferência (ex: repetir tarefas, usar verificadores) possam melhorar a precisão, as implementações atuais são frequentemente ad hoc, fortemente acopladas à lógica do programa e carecem de um framework principista para rastrear a incerteza ou explorar caminhos de execução alternativos. Desenvolvedores lutam para avaliar a correção das respostas ou experimentar diferentes estratégias de escalonamento sem reescrever a lógica central do fluxo.

Metodologia

O artigo apresenta o PPDL (Probabilistic Prompt Declaration Language), a primeira linguagem de programação probabilística especificamente projetada para fluxos baseados em LLM. O PPDL unifica a programação de prompts com a programação probabilística ao desacoplar a lógica central do programa da estratégia de escalonamento de inferência.

Construtos Principais da Linguagem

O PPDL é construído sobre o PDL (Prompt Declaration Language), uma linguagem declarativa para compor chamadas de LLM e de ferramentas. O PPDL estende o PDL com um único primitivo ortogonal: o factor.

sample (Implícito): Chamadas de LLM atuam como operações de amostragem de uma distribuição definida pelo modelo e pelo contexto atual.
factor: Este construto atualiza a probabilidade do traço de execução atual com base em restrições especificadas pelo usuário (suaves ou rígidas). As restrições podem ser derivadas de avaliações de "LLM-as-a-judge", ferramentas baseadas em regras (ex: linters, suítes de teste) ou modelos de recompensa de processo.
Modelo de Execução: Em vez de retornar um único output, o PPDL trata o programa como uma distribuição sobre traços de execução. O tempo de execução explora essa distribuição usando motores de inferência probabilística.

Semântica e Inferência

O artigo formaliza a semântica do PPDL como um amostrador ponderado (weighted sampler).

Amostrador Ponderado: Um único traço de execução reduz um programa $p$ a um valor $v$ com um log-score associado (acumulado de declarações factor).
Semântica Ideal: Definida como uma soma infinita sobre todos os traços possíveis, normalizada para formar uma distribuição categórica sobre valores de saída.
Inferência Aproximada: Como a semântica ideal é intratável, o PPDL implementa algoritmos de aproximação de Monte Carlo:
- Amostragem de Importância (IS - Importance Sampling): Executa $N$ partículas independentes (traços) e as repondera com base em seus scores finais.
- Monte Carlo Sequencial (SMC - Sequential Monte Carlo): Introduz etapas de reamostragem em pontos de factor. Partículas com scores baixos são descartadas, e aquelas com scores altos são duplicadas, permitindo que o sistema foque recursos computacionais em traços parciais promissores precocemente no fluxo.
- Votação Majoritária: Um baseline onde todas as partículas são ponderadas igualmente.

Implementação

O PPDL é uma linguagem interpretada implementada com paralelização.

Paralelismo: Partículas independentes são executadas em paralelo. Dentro de uma única partícula, chamadas de modelo independentes são paralelizadas usando futures e estruturas de dados diferidas para minimizar o bloqueio.
Ortogonalidade: Usuários escrevem a lógica do fluxo uma única vez. O algoritmo de inferência (IS, SMC ou Votação Majoritária) e a contagem de partículas são configurados em tempo de execução sem modificar o código fonte.

Principais Contribuições

Linguagem PPDL: A primeira linguagem de programação de prompt probabilístico para fluxos de chamadas de LLM e ferramentas, introduzindo o factor como um mecanismo para pontuar e direcionar traços de execução.
Semântica Formal: Uma definição rigorosa do comportamento do PPDL, formalizando a interação entre amostragem baseada em prompt e fatores probabilísticos, e definindo a distribuição resultante de traços.
Framework de Escalonamento de Inferência: Uma demonstração de que o PPDL permite a experimentação sistemática com diferentes algoritmos de escalonamento de inferência (IS, SMC, Votação Majoritária) através de vários modelos e tarefas sem reescrever a lógica do fluxo.
Estudo de Caso: Implementação de um agente de prova de teoremas para o provador de teoremas Rocq, demonstrando a utilidade da inferência probabilística em fluxos de agentes complexos e iterativos.

Resultados Experimentais

Os autores avaliaram o PPDL em múltiplos benchmarks (GSM8k, Math500, MBPP, LiveCodeBench, Fever) e modelos (Granite, Llama, GPT-OSS).

Melhorias de Acurácia: O escalonamento de inferência geralmente superou o baseline (execução única, IS@1). Embora a Votação Majoritária tenha performado bem em alguns casos, a Amostragem de Importância (IS) e o Monte Carlo Sequencial (SMC) frequentemente produziram resultados superiores, particularmente quando as restrições de factor forneceram informações significativas para distinguir traços corretos de incorretos.
Vantagem do SMC: Em fluxos de múltiplos passos complexos (como prova de teoremas), o SMC superou significamente o IS. Ao reamostrar em pontos intermediários de factor, o SMC pôde redirecionar a computação para caminhos promissores mais cedo, evitando o desperdício de tokens em traços parciais incorretos.
Estudo de Caso de Prova de Teoremas: No benchmark MiniF2F-Rocq, o SMC com 40 partículas resolveu 39% dos problemas (95/244), comparado a 30% (72.7/244) para a estratégia baseline IS@1. Isso demonstrou que o direcionamento probabilístico pode melhorar o desempenho do modelo base em tarefas desafiadoras.

Significância e Alegações

O artigo afirma que o PPDL fornece uma maneira principista de lidar com a incerteza em aplicações de LLM. Ao tratar fluxos de LLM como programas probabilísticos, ele permite que desenvolvedores:

Quantifiquem a Incerteza: Usuários recebem uma distribuição de outputs, permitindo que avaliem a confiança em vez de depender de uma única resposta, potencialmente errônea.
Experimentem Eficientemente: Desenvolvedores podem alternar entre estratégias de escalonamento de inferência (ex: de votação simples para SMC complexo) alterando a configuração de tempo de execução em vez de refatorar o código.
Desacoplem a Lógica da Busca: A separação da lógica central do fluxo da estratégia de busca (motor de inferência) simplifica o desenvolvimento de fluxos de agentes robustos.

Os autores reconhecem que o escalonamento de inferência não é uma "solução mágica" e que a qualidade dos resultados depende da qualidade das restrições (fatores) fornecidas, que podem ser imperfeitas. No entanto, o PPDL oferece um framework flexível para integrar e testar várias fontes de restrição e algoritmos de inferência.