noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

1. O Problema

As Linguagens de Programação Probabilística (PPLs) são ferramentas poderosas para modelar distribuições de probabilidade complexas, sendo amplamente utilizadas em análise de texto, verificação de redes e inteligência artificial. No entanto, a maioria das PPLs modernas foca em distribuições discretas ou contínuas puramente probabilísticas, carecendo de suporte robusto para escolhas não-determinísticas (como as encontradas em Processos de Decisão de Markov - MDPs).

O desafio central abordado neste trabalho é a combinação de não-determinismo e condicionamento (observações) em programas probabilísticos.

• Não-Determinismo: Permite modelar comportamentos desconhecidos ou abstratos (ex: um adversário em um jogo ou um agente em aprendizado por reforço), onde o sistema pode escolher entre várias ações sem uma distribuição de probabilidade fixa.
• Condicionamento: Envolve atualizar crenças com base em evidências observadas (raciocínio bayesiano).

A combinação desses dois conceitos torna a inferência extremamente difícil porque:

1. O programa não modela mais uma única distribuição, mas um conjunto de distribuições (uma para cada resolução possível do não-determinismo).
2. A inferência deixa de ser composicional: a probabilidade máxima condicional de um programa inteiro não pode ser deduzida simplesmente das probabilidades máximas de seus subprogramas.
3. Abordagens existentes frequentemente falham em lidar com ambos simultaneamente ou exigem a construção de espaços de estados operacionais gigantescos, tornando a inferência computacionalmente inviável.

2. Metodologia: A Framework noDice

Os autores introduzem o noDice, uma engine de inferência que estende o motor existente Dice para lidar com programas discretos, não-determinísticos e condicionados. A metodologia segue um pipeline de três etapas principais:

A. Compilação Booleana (Boolean Compilation)

O programa noDice é compilado em uma representação lógica:

• O programa é transformado em um par de fórmulas booleanas:
  1. $\phi$ (Fórmula de Modelo): Representa o comportamento do programa (o valor de saída), ignorando observações.
  2. $\gamma$ (Fórmula de Aceitação): Representa exclusivamente as observações (condicionamento).
• Diferentemente do Dice original, o noDice gera um rastreio anotado (trace) das operações de "flip" (moeda). Cada variável booleana é anotada se pertence a um flip probabilístico (com probabilidade $\theta$) ou a um nflip não-determinístico (sem probabilidade fixa).

B. Construção de Diagramas de Decisão (Decision Diagrams)

As fórmulas booleanas são representadas internamente como Diagramas de Decisão Binária (BDDs).

• O algoritmo combina os dois BDDs ($\phi$ e $\gamma$) em um único Diagrama de Decisão Algébrica (ADD).
• Os ADDs são generalizações dos BDDs que permitem saídas além de binárias (neste caso, valores de saída do programa ou um valor de rejeição $R$).
• Vantagem Crítica: Os ADDs exploram a estrutura do programa (como independência condicional) para compactar a representação, eliminando redundâncias e reduzindo drasticamente o espaço de estados em comparação com uma representação operacional direta.

C. Elevação para Processos de Decisão de Markov (MDPs)

O ADD construído é usado como "andaime" para construir um MDP:

• Cada nó do ADD torna-se um estado no MDP.
• As arestas do ADD são elevadas a transições no MDP:
  • Nós com variáveis probabilísticas geram transições probabilísticas.
  • Nós com variáveis não-determinísticas geram transições não-determinísticas (escolhas de ações).
• Semântica: As distribuições modeladas pelo programa correspondem aos agendadores sem memória (memoryless schedulers) no MDP.
• Consulta de Inferência: A probabilidade máxima de o programa retornar um valor específico, dado que todas as observações foram bem-sucedidas, é equivalente à probabilidade de alcance condicional de um estado alvo no MDP, condicionada a não atingir o estado de rejeição ($R$).

Para resolver essa probabilidade de alcance condicional, o noDice utiliza um algoritmo de bissecção (implementado no verificador de modelo Storm), que é altamente eficiente em MDPs acíclicos.

3. Contribuições Principais

1. Linguagem noDice: Desenvolvimento de uma linguagem funcional não-recursiva de primeira ordem que suporta escolhas probabilísticas, escolhas não-determinísticas e observações de primeira classe.
2. Algoritmo de Inferência Teórico: Apresentação de uma fundação teórica que mapeia a semântica de programas com não-determinismo e condicionamento para propriedades de alcance condicional em MDPs, utilizando ADDs para compactação.
3. Implementação e Avaliação: Implementação de um protótipo em OCaml e avaliação empírica contra verificadores de modelo de última geração (como o Storm).
4. Prova de Correção: Demonstração formal de que a probabilidade máxima de alcance no MDP construído corresponde à máxima probabilidade condicional do programa original.

4. Resultados Empíricos

Os autores avaliaram o noDice em uma variedade de benchmarks, incluindo rastreamento de veículos, coleta de cupons, redes de computadores, protocolos de troca justa e redes bayesianas.

• Redução do Espaço de Estados: O noDice consegue construir MDPs significativamente menores do que a codificação direta (usada pelo Storm). Em muitos casos, o tamanho do MDP do noDice é ordens de magnitude menor devido à compactação via ADDs.
• Desempenho:
  • O noDice supera o Storm em benchmarks com alta dimensionalidade (muitas variáveis), como o problema do Coletor de Cupons e redes bayesianas grandes. Nesses casos, o Storm sofre com a explosão combinatória ao enumerar estados, enquanto o noDice explora a estrutura do programa.
  • Em benchmarks com baixa dimensionalidade ou pouca redundância estrutural (como o problema de Rede), o custo de compilar o ADD pode ser maior do que a verificação direta do Storm, tornando o Storm mais rápido nesses casos específicos.
• Influência do Não-Determinismo: O tempo de compilação do noDice é relativamente insensível à quantidade de não-determinismo no programa. O tempo de verificação de modelo aumenta ligeiramente, mas permanece negligenciável em comparação com o tempo de compilação.
• Compressão de Estados: Uma técnica de compressão de estados probabilísticos foi implementada, reduzindo ainda mais o tamanho do MDP, embora não tenha impactado drasticamente o tempo total de execução (já que a compilação é o gargalo).

5. Significado e Impacto

O trabalho noDice preenche uma lacuna importante no campo da programação probabilística ao fornecer uma ferramenta prática para inferência em programas que combinam não-determinismo e condicionamento.

• Viabilidade: Demonstra que é possível realizar inferência exata em programas complexos com não-determinismo, algo que anteriormente exigia aproximações ou era computacionalmente proibitivo.
• Eficiência Estrutural: A abordagem baseada em ADDs prova ser superior à modelagem direta de MDPs para problemas com alta dimensionalidade e estrutura condicional, evitando a explosão de estados.
• Aplicações: O método é particularmente útil para cenários onde se deseja analisar o pior caso (worst-case) sob incerteza parcial, como em segurança de redes, verificação de sistemas de controle autônomo e análise de protocolos com adversários.

Em resumo, o noDice estabelece um novo paradigma para a inferência em programas probabilísticos discretos, utilizando técnicas de verificação formal (MDPs e Diagramas de Decisão) para resolver problemas de raciocínio probabilístico complexo de forma escalável.