Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization

Resumo Técnico: Revisitando a Complexidade de Caso Médio de Silogística Multinível

Enunciado do Problema
Este trabalho revisita o relatório técnico de 1995, TR1995-711, "The average case complexity of multilevel syllogistic", de Cox, Ericson e Mishra. O relatório original investigou se sublinguagens decidíveis da teoria dos conjuntos — especificamente Silogística Multinível (MLS) e Silogística Multinível Elementar (EMLS) — são tratáveis em média, apesar de serem NP-completas no pior caso. O relatório afirmou que esses problemas são NP-average completos, implicando que, sob distribuições de probabilidade simples e classificáveis por ranking, nenhum algoritmo eficiente de caso médio existe, a menos que as classes de complexidade NEXP e EXP colapsem. Embora o relatório original tenha fornecido provas matemáticas, faltou-lhe verificação verificada por máquina. Além disso, o campo da prova automática de teoremas posteriormente convergiu para resolvedores SMT e benchmarks empíricos em vez da análise formal de caso médio de fragmentos da teoria dos conjuntos. Este artigo aborda a lacuna entre as reivindicações teóricas originais e os padrões modernos de verificação formal, reimplementando a lógica, definições e teoremas do relatório em Lean 4.

Metodologia
Os autores empregam uma estratégia rigorosa de "programa de prova", priorizando definições formais sobre teoremas e evitando o uso de sorry (suposições não provadas) em definições finais. O desenvolvimento é estruturado em cinco fases:

1. Infraestrutura (Fase 0): Configuração do projeto Lake e do ambiente Lean.
2. Vocabulário de Complexidade de Caso Médio (AvCom) (Fase 1): Formalização do framework de Reischuk–Schindelhauer (1993) e das definições de complexidade de caso médio de Levin (1986). Isso inclui a definição de:
   • Distribuições: Distribuições de probabilidade de suporte finito sobre strings de bits.
   • Funções de Rank: Contagem de entradas com probabilidade maior ou igual a uma determinada entrada.
   • Classes de Complexidade: Definição de AvP (Tempo Polinomial Médio), distNP (NP distributivo) e AvDTime (Tempo Determinístico Médio) usando a desigualdade de soma de rank de RS93.
   • Reduções: Formalização de reduções distributivas com a condição de dominação para preservar a tratabilidade de caso médio.
3. Incorporação de MLS (Fase 2): Incorporação profunda da sintaxe e semântica de MLS e EMLS.
   • Sintaxe: Definições indutivas para termos (variáveis, união, interseção, diferença), relações (pertencimento, igualdade) e fórmulas.
   • Semântica: Uma semântica de conjuntos ZF (ZFSet) axiomática com funções de avaliação não computáveis.
   • Procedimento de Decisão: Implementação de um procedimento de decisão parcial baseado em Ferro–Omodeo–Schwartz (1980). Os autores provam a correção (soundness) e a completude parcial para um fragmento livre de pertinência, enquanto reconhecem que a completude total (exigindo a substituição do Passo 1 e a busca de modelo do Passo 4 completo) permanece em aberto.
4. Serialização e Membro em NP (Fase 3): Definição de codificações binárias para fórmulas MLS e prova de que o problema de satisfatibilidade (SatMLS) pertence a NP via um verificador baseado em certificado.
5. Dureza e Completude (Fases 4–5):
   • Reduções: Construção de uma redução distributiva de Bounded Halting (NBH) para SatMLS. Devido à complexidade da tradução completa de TM para MLS, o mapa de redução geral é axiomatizado (nbhToMlsMap), enquanto a condição de dominação é verificada para uma distribuição de suporte específica.
   • Completude: Prova de que SatMLS é NP-average completo, condicional à axioma de que todo problema distNP reduz-se a NBH.
   • Corolários de Dureza: Derivação de que SatMLS não está em AvP a menos que NEXP = EXP, usando a completude estabelecida e a hipótese de colapso.

Contribuições Principais

• Formalização de TR1995-711: A primeira formalização verificada por máquina dos resultados de complexidade de caso médio para MLS e EMLS.
• Biblioteca de AvCom em Lean 4: A criação de uma biblioteca personalizada (AvgCaseMls) implementando classes de Reischuk–Schindelhauer, reduções distributivas e distribuições classificáveis por rank, preenchendo uma lacuna no ecossistema Mathlib4, que atualmente foca em complexidade de pior caso.
• Verificação de Correção e Completude Parcial: Provas rigorosas de que o procedimento de decisão implementado é correto e completo para o fragmento específico de MLS sem literais de pertinência.
  verdade.
• Transparência Axiomática: Os autores documentam explicitamente "forks" (escolhas de design) e axiomas (ex: o mapa de redução geral de TM para MLS, o hipótese NEXP ≠ EXP) em DEFINITION_FORKS.md, distinguindo entre teoremas provados e andaimes necessários.

Resultos
O artigo reporta os seguintes resultados para seu plano de fases:

• Fases 1A–1D (Definições de AvCom): Todas as definições compilam sem sorry. A formalização de entradas, distribuições, funções de rank e classes de complexidade coincide com a literatura.
• Fases 2A–2D (MLS & Decisão): Sintaxe, semântica e o procedimento de decisão parcial são verificados. A correção é provada; a completude é provada apenas para o fragmento livre de pertinência.
• Fases 3A–3B (Codificação): Limites polinomiais de tamanho de codificação e o membro em NP para o verificador são verificados.
• Fases 4A–4C (Reduções & Completude): A redução de NBH para SatMLS é verificada módulo o mapa de tradução geral axiomatizado. A NP-average completude de SatMLS é provada módulo o axioma de que todos os problemas distNP reduzem a NBH.
• Fases 5A–5B (Dureza): A dureza condicional de não-AvP para SatMLS é derivada, contingente sobre o axioma NEXP ≠ EXP.

Significância e Alegações
O artigo não afirma ter "resolvido" a complexidade de caso médio de MLS de uma forma que mude a engenharia de software prática. Em vez disso, sua significância é histórica e metodológica:

1. Sobrevivência da Teoria: Ele testa se as alegações matemáticas do relatório de 1995 sobrevivem ao contato com um assistente de prova moderno. Os resultados indicam que a lógica central se mantém, desde que axiomas estruturais específicos (como a existência de uma redução universal para NBH) sejam aceitos.
2. Clarificação de Suposições: Ao formalizar o trabalho, os autores expõem as dependências precisas da prova original, como a dependência da hipótese NEXP ≠ EXP para resultados de dureza e a necessidade de propriedades específicas de redução distributiva.
3. Fundação para Trabalhos Futuros: O artigo argumenta que, embora a aplicação específica de AvCom a procedimentos de decisão de MLS tenha sido amplamente abandonada em favor de resolvedores SMT na década de 1990, o framework formal desenvolvido aqui fornece uma infraestrutura necessária para revisitar a análise de caso médio em outros domínios, como análise suavizada (smoothed analysis) ou criptografia pós-quântica, dentro do ecossistema Lean.

Os autores declaram explicitamente que não tratam sorry ou axiomas como sucesso; em vez disso, eles servem como "andaimes temporários" com tarefas para removê-los em trabalhos futuros. O artigo conclui que a visão do relatório de 1995 de usar a complexidade de caso médio para caracterizar a tratabilidade de problemas de verificação permanece matematicamente coerente, mesmo que o caminho prático para a implementação tenha mudado.