Resumo Técnico: Verificação de Amostradores Exatos para Distribuições Contínuas com uma Lógica de Programa Discreta

Declaração do Problema

A maioria das implementações de algoritmos de amostragem para distribuições de probabilidade contínuas depende da aritmética de ponto flutuante. Embora aceitável para muitas aplicações, as operações de ponto flutuante introduzem erros de arredondamento que são difíceis de analisar e podem levar a vulnerabilidades críticas de segurança, particularmente em privacidade diferencial, onde os algoritmos são frequentemente desenvolvidos formalmente sob a suposição de aritmética exata.

Uma alternativa é utilizar algoritmos de amostragem exata baseados em reais computáveis, que podem gerar preguiçosamente dígitos de uma amostra contínua com precisão arbitrária. No entanto, esses algoritmos são intrincados. Eles exigem uma combinação de recursos linguísticos semanticamente desafiadores, incluindo escolha probabilística, funções de ordem superior e estado mutável alocado dinamicamente. As lógicas de programa existentes para verificação probabilística são insuficientes para esta tarefa: trabalhos anteriores restringem o raciocínio a distribuições discretas ou assumem a existência de primitivas para amostragem de distribuições contínuas (muitas vezes dependendo de aritmética real não computável). Consequentemente, há uma falta de técnicas formais para verificar a correção de amostradores exatos e computáveis para distribuições contínuas que operam dentro de um modelo de programação discreto e com estado.

Metodologia

Os autores apresentam Continuous-Eris, uma lógica de separação de ordem superior projetada para verificar a correção de algoritmos de amostragem exata para distribuições computáveis. O Continuous-Eris estende o Eris (uma lógica para verificar a correção aproximada de programas probabilísticos discretos) e é construído sobre a estrutura da lógica de separação Iris.

A metodologia central baseia-se em preencher a lacuna entre o raciocínio discreto e contínuo através de três ingredientes lógicos fundamentais:

1. Créditos de Erro: Empréstimos do Eris, estes são recursos da lógica de separação $E(r)$ que representam um limite superior na probabilidade de uma especificação falhar. Eles permitem raciocínio modular sobre programas probabilísticos ao "gastar" créditos para excluir eventos de erro de baixa probabilidade.
2. Recibos de Tempo: Adaptados de Mével et al., estes são utilizados para internalizar a correção parcial da lógica. Ao rastrear o número de passos de execução restantes ($StepsLeft(k)$), a lógica pode raciocinar sobre prefixos finitos de execuções potencialmente infinitas. Isso é crucial porque amostradores exatos frequentemente envolvem avaliação preguiçosa, onde uma sequência infinita de bits nunca é totalmente gerada.
3. Fitas de Pré-amostragem: Adaptadas do Clutch, estas permitem que a prova determine antecipadamente os resultados de futuros comandos de amostragem aleatória. Enquanto fitas padrão são finitas, os autores combinam-nas com recibos de tempo para simular fitas de pré-amostragem infinitas. Este mecanismo permite que a lógica condicione créditos de erro a um número real específico $r$ (representado por uma string infinita de bits), mesmo que o programa gere apenas um número finito de bits durante qualquer execução finita.

Fundamentação Teórica

A lógica generaliza a especificação de correção discreta de Marionneau et al. para o cenário contínuo. Em vez de caracterizar um amostrador por uma função de massa de probabilidade discreta, o Continuous-Eris caracteriza um amostrador por uma integral de Riemann sobre uma função densidade de probabilidade.

O padrão de especificação central para um amostrador $U$ gerando um real uniforme em $[0, 1]$ é:
$$\forall F \in PC([0, 1]), \quad \left\{ E\left(\int_0^1 F(x) dx\right) \right\} U() \{ v. \exists r. E(F(r)) * IsReal\ v\ r \}$$
Aqui, $F$ é uma função limitada e contínua por partes. A lógica permite condicionar créditos ao valor amostrado $r$ como se fosse extraído uniformemente, desde que o valor esperado dos créditos seja preservado. A correção desta abordagem baseia-se no fato de que uma soma de Riemann (derivada da pré-amostragem finita) pode aproximar a integral arbitrariamente de perto, com o erro de discretização pago por créditos de erro "do nada" (thin-air).

Contribuições Principais

1. Lógica Continuous-Eris: Uma lógica de programa inovadora que combina créditos de erro, recibos de tempo e fitas de pré-amostragem para verificar algoritmos de amostragem contínua computáveis. Ela suporta funções de ordem superior, estado mutável e alocação dinâmica.
2. Verificação Formal de Amostradores Exatos: Os autores fornecem implementações formalmente verificadas de amostradores exatos para:
   • A distribuição Uniforme sobre $[0, 1]$.
   • A distribuição Gaussiana (Normal).
   • A distribuição Laplace.
     Estas implementações baseiam-se em algoritmos de Karney e utilizam representações preguiçosas de listas de bits.
3. Aritmética de Reais Construtivos Verificada: Uma biblioteca para aritmética de reais exatos (uma adaptação do CReal) verificada dentro do Continuous-Eris. Esta biblioteca suporta operações (adição, negação, escalonamento, comparação) em números reais preguiçosos, permitindo a construção de distribuições complexas a partir de outras mais simples.
4. Limite de Precisão para Privacidade Diferencial: Uma prova formal de que o amostrador Laplace verificado satisfaz um limite de precisão específico utilizado na literatura de privacidade diferencial. Isso demonstra que a saída do amostrador adere às garantias teóricas exigidas para mecanismos de preservação de privacidade, sem depender de aproximações de ponto flutuante.
5. Mecanização: Todos os resultados foram mecanizados no assistente de provas Rocq (anteriormente Coq), baseando-se na estrutura Iris e na biblioteca de análise real Coquelicot.

Resultados

O artigo demonstra a utilidade do Continuous-Eris através da verificação do programa MaxU2 (calculando o máximo de duas amostras uniformes) e do amostrador Gaussiano de Karney completo.

• MaxU2: Os autores provam que o programa retorna um valor distribuído com densidade de probabilidade $\mu_{max}(x) = 2x$. A prova envolve integrais iteradas e indução de Löb para lidar com comparações recursivas de bits.
• Amostrador Gaussiano: A verificação segue uma estrutura modular, verificando sub-rotinas para ensaios de Bernoulli, partes inteiras e loops de amostragem por rejeição. A prova estabelece que o amostrador gera valores com a densidade Gaussiana correta.
• Amostrador Laplace: Os autores verificam um amostrador para a distribuição Laplace e derivam o limite de cauda $P[|L_{\epsilon, \mu} - \mu| > \frac{\log(1/\beta)}{\epsilon}] \leq \beta$ diretamente da lógica, sem adicioná-lo como um axioma primitivo.

Significado e Alegações

O artigo afirma preencher uma lacuna crítica na verificação formal ao fornecer a primeira técnica capaz de verificar amostradores exatos e computáveis para distribuições contínuas que utilizam estado mutável e funções de ordem superior.

• Correção sem Aproximação: Diferentemente de trabalhos anteriores que assumem primitivas contínuas ou utilizam aritmética de ponto flutuante, o Continuous-Eris verifica algoritmos que geram amostras exatas (com precisão arbitrária) usando apenas primitivas discretas (ensaios de Bernoulli).
• Gerenciamento de Complexidade: A lógica gerencia com sucesso os desafios semânticos de combinar aleatoriedade, estado mutável e funções de ordem superior, que são tipicamente difíceis de raciocinar denotacionalmente.
• Relevância Prática: Ao verificar o amostrador Laplace e seus limites de precisão, o trabalho fornece uma base para construir sistemas de privacidade diferencial com garantias rigorosas contra erros de ponto flutuante.
• Modéstia: Os autores reconhecem limitações. A abordagem atual depende da integração de Riemann, exigindo que as funções de distribuição de créditos sejam contínuas por partes. Isso impede o raciocínio sobre distribuições com descontinuidades não enumeráveis (por exemplo, evitando todos os pontos racionais). Além disso, o artigo foca na correção parcial; provar a terminação quase certa para estes amostradores fica para trabalhos futuros ou outras lógicas como o Total Eris.

Em resumo, o Continuous-Eris oferece uma estrutura rigorosa e mecanizada para verificar que programas complexos e com estado implementam corretamente a amostragem exata de distribuições contínuas, preenchendo a lacuna entre a análise computável teórica e a verificação prática de programas.