Resumo Técnico: Orquestração de Fluxos de Trabalho com Composição Declarativa Determinística–Probabilística

1. O Problema: Fragmentação e o Hiato de Dois Modos

Os atuais sistemas de fluxo de trabalho baseados em LLM sofrem de uma fragmentação fundamental. Profissionais devem dominar habilidades díspares — engenharia de prompt, orquestração em Python e gerenciamento de API — para construir sistemas que frequentemente exigem de 80 a 150 linhas de "código de colagem" (glue code) imperativo para tarefas simples de autorrefinamento. Os frameworks existentes (ex: LangGraph, AutoGen, CrewAI) operam exclusivamente em um modo probabilístico, produzindo saídas aproximadas e não reproduzíveis. Por outro lado, ferramentas simbólicas (SymPy, SageMath, Lean) operam em um modo determinístico, produzindo resultados exatos e mecanicamente verificáveis.

O artigo identifica um "hiato de dois modos": nenhum sistema de linguagem de fluxo de trabalho existente permite que um programador declare tanto "calcule este passo aproximadamente" quanto "calcule este passo exatamente" dentro de uma única especificação. Tarefas agênticas do mundo real (ex: um assistente de lição de casa) exigem ambos: planejamento e narração probabilísticos, acoplados à execução algébrica e verificação determinísticas. Atualmente, coordenar esses modos requer gerenciamento de estado manual e código específico da aplicação para fazer a ponte entre as fronteiras, criando um teto de expressividade e altas barreiras de entrada para especialistas de domínio.

2. Metodologia: A Linguagem SPL e a Arquitetura

Os autores apresentam a SPL (Structured Prompt Language), uma linguagem declarativa projetada para unificar esses modos de computação. A SPL é regida por cinco princípios de design:

1. Composição Declarativa: Os programadores especificam o que cada passo computa e seu modo, não como ele é executado.
2. Primitivos Coequais: A linguagem trata os modos probabilísticos (Sistema 1) e determinísticos (Sistema 2) como cidadãos de primeira classe.
3. Espaço de Variáveis Compartilhado: Um namespace unificado @variable permite o fluxo de dados contínuo entre os modos sem necessidade de marshaling manual.
4. DODA (Design Once, Deploy Anywhere - Projete uma Vez, Implante em Qualquer Lugar): A especificação .spl é invariante; provedores de modelos (Ollama, Anthropic, etc.) e verificadores (SymPy, Sage, Lean) são selecionados no momento da invocação via flags de CLI.
5. Alvo de Compilação: A linguagem produz uma Representação Intermediária (IR) otimizável.

Primitivos Principais

• Probabilístico (Sistema 1):
  • GENERATE: Invoca um LLM para produzir saídas aproximadas.
  • EVALUATE: Usa um LLM como juiz de tempo de execução para ramificação semântica (ex: checando por alucinações ou termos indefinidos).
  • WHILE: Itera com base em portões de qualidade julgados pelo LLM.
  • EXCEPTION: Lida com modos de falha específicos de LLM (alucinação, estouro de contexto).
• Determinístico (Sistema 2):
  • SOLVE: Despacha uma expressão Python para um kernel vivo (IPython) para computação exata.
  • ASSERT: Avalia uma expressão Booleana no kernel para controlar a continuidade do fluxo de trabalho.
  • CALL PARALLEL: Executa ramos concorrentes (ex: comparando um braço de solver vs. um braço apenas de LLM).

A Escada de Verificadores

A SPL implementa uma hierarquia de três níveis de verificadores simbólicos, selecionáveis em tempo de execução:

• R1 (SymPy): Para identidades algébricas e cálculo (milissegundos, zero dependências externas).
• R2 (SageMath): Para teoria dos números, geometria e combinatória (requer ambiente separado).
• R3 (Lean 4): Para provas formais contra Mathlib (minutos, alta confiança).
  A linguagem permite que fluxos de trabalho escalem de R1 para R2 ou R3 após uma falha de ASSERT, tudo expresso declarativamente sem condicionais em Python.

3. Principais Contribuições

1. Composição Declarativa de Dois Modos: A SPL introduz os primitivos SOLVE e ASSERT que roteiam a computação para um kernel vivo ao lado de GENERATE e EVALUATE. As atribuições de variáveis fluem entre esses modos através de um namespace compartilhado, gerenciado inteiramente pelo runtime.
2. O Princípio DODA: Um único arquivo .spl roda inalterado em nós locais, APIs de nuvem e grades distribuídas. A seleção de modelo e verificador é adiada para o momento da invocação, desacoplando o fluxo lógico da execução física.
3. A Escada de Verificadores: Uma hierarquia composível de garantias de correção (SymPy, SageMath, Lean 4) acessível via ASSERT. A lógica de escalonamento é declarada no fluxo de trabalho, não codificada em Python.
4. Avaliação Empírica Controlada: Um experimento de 1.200 execuções (10 modelos × 20 problemas × 2 braços × 3 repetições) através de 6 níveis de dificuldade, comparando um "Braço de Solver" (LLM decompõe, kernel executa/verifica) contra um "Braço apenas de LLM".

4. Resultados Experimentais

O experimento avaliou 10 modelos (incluindo gemma4:e2b, sonnet-4-6, qwen2.5) em problemas de matemática simbólica variando de polinômios de etapa única (T0) a ODEs especialistas (T5).

• Corretude Verificada vs. Produção de Saída: O braço apenas de LLM alcançou taxas de aprovação próximas a 100% (definidas como resposta não vazia), mas estas não foram verificadas. O braço do Solver, que exige corretude mecanicamente verificada, mostrou variância significativa:
  • gemma4:e2b alcançou 93% de corretude verificada (vs. 97% apenas de LLM).
  • sonnet-4-6 alcançou 85% de corretude verificada (vs. 100% apenas de LLM).
  • Modelos de nível inferior (ex: phi3) caíram para 32% de corretude verificada.
• Modos de Falha: O modo de falha dominante foi solver_error (expressões rejeitadas pelo kernel), não a não conformidade de formato (ex: cercas de markdown). Isso indica que modelos capazes de raciocinar frequentemente falham em produzir a sintaxe estrita expr|op exigida pelo motor determinístico.
• Dificuldade do Backend: Surgiu um gradiente onde problemas de SymPy (T0–T2) tiveram uma taxa de aprovação agregada de 78%, enquanto problemas de SageMath (T3–T5) caíram para 54%, atribuído tanto à matemática mais difícil quanto a superfícies de API menos familiares.
• Latência: Para muitos modelos, o braço do Solver foi mais rápido que o braço apenas de LLM devido ao "saída antecipada" (early exit) em erros de solver (pulando a etapa final de narração) e ao curto-circuito da cadeia de pensamento (chain-of-thought) do kernel. No entanto, modelos de alta precisão como gemma4:e2b incorreram em um aumento de 25% na latência devido à conclusão de cadeias completas.

5. Significância e Alegações

O artigo afirma que a SPL muda fundamentalmente o papel do LLM em fluxos de trabalho matemáticos e lógicos de um raciocinador para um tradutor de formato.

• Distinção Epistêmica: Os autores argumentam que a distinção entre Sistema 1 e Sistema 2 é epistêmica (probabilística vs. determinística), não temporal (rápido vs. lento). A SPL formaliza isso tornando a fronteira de modo visível no código fonte.
• Separabilidade de Habilidades: Os resultados demonstram que a "conformidade de formato" (produzir planos estruturados expr|op) é uma capacidade separável do "raciocínio matemático". Um modelo pequeno e de código aberto (gemma4:e2b, ~2B parâmetros) superou modelos maiores em corretude verificada porque produziu confiavelmente o formato estruturado exigido, enquanto o kernel lidou com a derivação real.
• Privacidade e Acessibilidade: Ao desacoplar a especificação do backend de execução, a SPL permite fluxos de trabalho offline e preservadores de privacidade (usando Ollama local e SymPy), onde os dados do estudante nunca deixam o dispositivo, mas ainda se beneficiam da corretude mecanicamente verificada.
• Teto de Expressividade: O artigo postula que a atual abordagem de "código de colagem" imperativo é um teto de expressividade. A composição declarativa da SPL permite otimizações futuras (loteamento, cache, roteamento de modelo) que são impossíveis em código de orquestração imperativo porque a intenção é explícita na IR.

Os autores concluem que a SPL fecha o hiato entre a geração probabilística e a verificação determinística, tornando a computação de alta qualidade e verificada acessível sem exigir profundos conhecimentos de engenharia de software ou acesso a modelos proprietários.