GPU-Accelerated Search and Certification of Bounded Indistinguishability in Finite Kripke Semantics

Resumo Técnico: Busca Acelerada por GPU e Certificação de Indistinguibilidade Limitada em Semântica de Kripke Finita

Enunciado do Problema
O artigo aborda duas questões fundamentais relativas à lógica modal e à teoria de modelos finitos que são decidíveis, mas computacionalmente dispendiosas:

1. Tamanho do Contramodelo Mínimo: Para fórmulas modais inválidas, quão grandes são os contramodelos mínimos na prática em comparação com os limites exponenciais padrão fornecidos pela Propriedade do Modelo Finito (FMP) e filtragem?
2. Indistinguibilidade Limitada: Quão grande deve ser um modelo finito para que possa distinguir entre duas fórmulas que parecem equivalentes em todos os modelos menores? Os autores definem um par de fórmulas como k-indistinguíveis se elas concordam em todos os frames de tamanho $\le k$, mas divergem em um frame de tamanho $k+1$.

Enquanto as técnicas padrão baseadas em BDD para verificação de modelos simbólica comprimem grandes espaços de estados para uma única fórmula, este trabalho visa o regime oposto: um censo completo de muitas fórmulas contra muitos frames pequenos simultaneamente.

Metodologia
Os autores aproveitam a natureza bit a bit da avaliação de Kripke finita para permitir um paralelismo massivo em GPUs.

• Codificação por Máscara de Bits (Bitmask Encoding): Mundos são codificados como inteiros e valorações como máscaras de bits. Conectivos booleanos mapeiam para operações bit a bit, enquanto operadores modais ($\Box$ e $\Diamond$) são reduzidos a testes de contenção e interseção em máscaras de sucessores (Lema 1). Isso elimina a necessidade de materializar o tensor de verdade $(frame \times valuation)$.
• Kernel CUDA Fundido (Fused CUDA Kernel): Um único kernel avalia um corpus inteiro de fórmulas contra todos os frames de um tamanho fixo em uma única passagem. Threads são atribuídas a frames, iterando através de valorações via índices de loop (evitando arrays de valoração) e reduzindo resultados usando memória compartilhada para minimizar a contenção atômica.
• Arquitetura de Verificação: O sistema emprega um paradigma de "busca rápida, verificação lenta". A GPU realiza a enumeração exaustiva, enquanto um avaliador recursivo separado na CPU (independente do motor de máscara de bits) verifica cada contramodelo relatado. Isso garante que os resultados sejam confiáveis, independentemente dos detalhes de implementação do acelerador.
• Síntese Ativa: Além da enumeração passiva, os autores utilizam um protocolo de síntese ativa para gerar pares de fórmulas candidatos (ex: $(\Box\Diamond)^m\top$) e buscar por "miragens semânticas" (pares indistinguíveis) usando geração de frames adversariais (Erdős–Rényi, gargalos de SCC, etc.) e solvers SAT para provas de minimalidade.
• Recuperação Guiada por Representação: O artigo constrói um "atlas semântico" (uma matriz de densidade de perfis de falha) e avalia várias técnicas de redução de dimensionalidade (PCA, UMAP, espectral) para recuperação de candidatos. Crucialmente, as visualizações são tratadas como interfaces de geração de candidatos, não como motores de descoberta autônomos; cada candidato é re-verificado via busca exaustiva.

Principais Contribuições e Resultados

1. Corretude e Complexidade: Os autores fornecem uma prova de corretude para o avaliador de máscara de bits (Teorema 1) e uma análise de complexidade mostrando que a abordagem evita o armazenamento do tensor de verdade (Proposição 1). Todos os 20.990 certificados gerados foram independentemente verificados.
2. Pequenos Contramodelos Mínimos: Em um corpus de 5.624 fórmulas sem constantes (até 7 nós, 2 variáveis), o estudo descobriu que os contamodelos mínimos são surpreendentemente pequenos.
   • Toda fórmula refutável na lógica K é refutada em no máximo 2 mundos (Proposição 3).
   • O limite padrão de filtragem ($2^{|Sub(\phi)|}$) é empiricamente frouxo; para fórmulas de 7 nós, o limite sugere até 128 mundos, mas o máximo observado foi 2 (Corolário 1).
3. Síntese de Indistinguibilidade Limitada: Os autores sintetizaram com sucesso um par 5-indistinguível ($\alpha_2 = (\Box\Diamond)^2\top$ e $\alpha_3 = (\Box\Diamond)^3\top$). Essas fórmulas concordam em todos os frames de tamanho $\le 5$, mas são separadas por um caminho específico de 6 mundos (Proposição 5).
   • Essa separação foi confirmada tanto pela enumeração exaustiva em GPU quanto por provas SAT simbólicas (Tabela 3).
   • A síntese de frames adversariais produziu 90 separações verificadas, das quais 78 não eram de template (ou seja, não eram simples caminhos ou ciclos).
4. Desempenho do Sistema:
   • A implementação fundida em H100 alcançou uma taxa sustentada de 60,2 bilhões de avaliações por segundo (1,63 $\times$ 10$^{14}$ avaliações totais em 45 minutos).
   • Foi 47,1$\times$ mais rápida que um CPU OpenMP bit-parallel e 7,06$\times$ mais rápida que uma linha de base explícita de CPU AVX-512 em cargas de trabalho correspondentes.
   • A calibração de hardware atingiu 18,87 source-level uint32 TOPS com 98,3% de tempo médio de ocupação NVML.
5. Representação e Recuperação:
   • Em uma tarefa de recuperação sobre 5,4 milhões de pares candidatos, as características brutas de alta dimensão tiveram o melhor desempenho em orçamentos de vizinhança apertados ($k=16$), enquanto um atlas 2D de PCA teve o melhor desempenho em orçamentos mais amplos ($k=1024$).
   • No entanto, os autores enfatizam que as visualizações 2D sofrem de clutter extremo (98,6% dos pontos compartilham um bin na escala de 100k) e não são ferramentas de descoberta autônomas. O pipeline depende de proposta guiada por representação seguida de verificação exaustiva.
6. Recuperação de Correspondência: O motor recuperou com sucesso condições de frame de primeira ordem para todos os axiomas de Sahlqvist (T, D, 4, 5, B, etc.) e identificou corretamente que o axioma de McKinsey não possui correspondente de primeira ordem no corpus testado, validando o sistema contra a teoria estabelecida.

Significância e Escopo
O artigo reivindica significância não como um novo procedimento de decisão para lógica modal geral (que permanece PSPACE-completo), mas como um protocolo reproduzível para explorar o "regime de modelos pequenos" e as fronteiras da indistinguibilidade.

• Modéstia das Alegações: Os autores declaram explicitamente que seus resultados são limitados. O censo decide a validade apenas para fórmulas onde o limite da FMP está dentro do tamanho pesquisado (até 5 mundos). Alegações sobre fórmulas que sobrevivem além desse intervalo são estimativas ou sobreviventes limitados, não teoremas.
• Descoberta vs. Verificação: O artigo distingue entre gerar candidatos (via síntese ou atlas visuais) e certificar esses candidatos (via verificação exaustiva). A "descoberta" do par 5-indistinguível é um resultado de síntese ativa e verificação exaustiva, não meramente inspeção visual.
• Complementaridade: O trabalho é apresentado como complementar à verificação de modelos simbólica (BDDs/SAT). Enquanto métodos simbólicos comprimem um grande espaço de estados, esta abordagem varre explicitamente muitos modelos pequenos contra muitas fórmulas, um regime onde métodos simbólicos podem não ser ideais.

Em resumo, o artigo demonstra que a avaliação bitwise acelerada por GPU permite o censo exaustivo de pequenos modelos de Kripke, revelando que os contamodelos mínimos são frequentemente muito menores do que os limites teóricos sugerem, e fornece um framework rigoroso para sintetizar e certificar a indistinguibilidade limitada em lógica modal.