A Machine-Checked Cost Analysis of the BMSSP Recurrence in Isabelle/HOL With a Non-Vacuous Size-Parametric Runtime Witness

Resumo Técnico: Uma Análise de Custo Verificada por Máquina da Recorrência BMSSP

Enunciado do Problema
O artigo aborda a verificação formal da recorrência BMSSP (Bounded Multi-Source Shortest Path), o motor central do algoritmo determinístico de 2025 por Duan, Mao, Mao, Shu e Yin que quebra a duradoura barreira de ordenação $O(m + n \log n)$ para caminhos mínimos de fonte única (SSSP) direcionados. Embora o algoritmo original alcance um tempo de execução de $O(m \log^{2/3} n)$, formalizar sua correção e, crucialmente, sua análise de custo amortizado em um assistente de prova apresenta desafios significativos. Estes incluem a complexidade de argumentos de correção recursiva envolvendo conjuntos de fontes e intervalos de distância limitados, a delicadeza do cálculo amortizado sobre estruturas de dados de partição customizadas e o risco de teoremas assintóticos "vacuosos" — afirmações que são tecnicamente verdadeiras, mas sem sentido porque a família de entrada é limitada ou as execuções necessárias não existem.

Metodologia
Os autores apresentam uma formalização completa em Isabelle/HOL (Isabelle2025-2) estruturada em seis teorias distintas e em camadas para garantir a modularidade e a separação rigorosa de preocupações. O desenvolvimento importa apenas HOL e HOL-Library, sem axiomas externos, sorry ou oops.

1. Fundamentos Semânticos: Os autores definem grafos direcionados ponderados finitos, caminhadas simples e métricas de distância. Eles estabelecem lemas estruturais relativos a caminhadas mínimas únicas e desempate estrito, que formam a base para todos os argumentos subsequentes.
2. Correção Recursiva: Um modelo abstrato da recorrência BMSSP é formalizado, incluindo a rotina FindPivots, casos base e o loop de partição. Uma prova verificada por máquina estabelece que o algoritmo abstrato computa corretamente as distâncias mínimas para qualquer grafo bem formado.
3. Artefato Executável: O modelo abstrato é refinado em uma função executável (bmssp_distances) usando vértices e pesos de números naturais. Os autores provam bmssp_correct_strong, confirmando que a saída do executável corresponde à definição semântica de distâncias mínimas, verificada via avaliação em um exemplo específico de cinco vértices.
4. Modelo de Custo: Uma interface de partição abstrata (Insert, BatchPrepend, Pull) é definida com predicados de custo. Os autores provam um envelope de custo amortizado de $O(m \log^{2/3} n)$ para esta recorrência abstrata. Crucialmente, eles implementam uma estrutura de dados de partição por baldes (bucketed partition) que realiza fielmente o cronograma logarítmico do artigo, provando a escala decisiva de inserção de $O(\log(N/M))$ necessária para o ganho de velocidade.
5. Refinamentos Operacionais: Duas camadas operacionais são definidas:
   • Exact-Concrete (Exata-Concreta): Acopla a saída da recursão filha estritamente ao intervalo de fatia incremental.
   • Charged (Cobrada): Desacopla a saída, cobrando apenas a fatia incremental.
     Os autores verificam por máquina que a relação exact-concrete é não-total sobre as entradas pretendidas (especificamente em famílias de caminhos), forçando uma obstrução onde execuções completas não podem existir.
6. Camada Paramétrica de Tamanho: Os autores constroem uma família ilimitada de caminhos direcionados de peso unitário ($P_n$). Eles provam que a relação charged é total e que uma execução completa existe. Para garantir a totalidade sem alterar a classe assintótica, eles empregam um índice de cronograma "inflado" ($N = n \cdot n$), que garante que a capacidade do balde cubra o caminho enquanto preserva o fator $O(\log^{2/3} n)$.

Principais Contribuições

• Primeira Formalização Mecanizada: Esta é a primeira formalização verificada por máquina da recorrência BMSSP e de sua análise de tempo de execução.
• Testemunha de Tamanho-Paramétrica Não-Vacua: O artigo fornece um teorema totalmente incondicional testemunhando que, sobre a família ilimitada de caminhos direcionados de peso unitário, o tempo de execução cobrado é $O(|V| \cdot (\ln |V|)^{2/3})$. Este resultado é não-vacuo porque os autores provam explicitamente (via um "livro-razão de não-vacuidade") que a família cresce sem limites, uma execução completa provavelmente existe e o regime operacional é realizado.
• Diagnóstico Formal de uma Obstrução de Acoplamento: Os autores identificam e provam formalmente um defeito em uma relação de custo ingênua e estritamente acoplada (o modelo exact-concrete). Eles demonstram que essa relação força o algoritmo a realizar no máximo um passo em famílias de caminhos, tornando qualquer limite paramétrico de tamanho baseado nela vacuo. Esta obstrução é registrada como um lema verificado por máquina, e o resultado principal é derivado usando a relação desacoplada charged para contorná-la.
• Verificação Executável: O desenvolvimento inclui uma função de distância mínima executável com uma prova de correção que é validada pela avaliação de código dentro do processo de construção (build).

Resultos
O teorema principal, path_nonvac_runtime_bigo_card_V_unconditional, afirma que:
$$(\lambda n. \text{real}(\text{path\_nonvac\_time } n)) \in O(\lambda n. \text{real}(\text{card}(\text{path\_k\_V } n)) \cdot (\ln(\text{real}(\text{card}(\text{path\_k\_V } n) + 2))^{2/3})$$
Este limite é:

• Incondicional: Não carreia hipóteses relativas à existência de execução ou propriedades de grafo além da definição da família de caminhos.
• Paramétrico de Tamanho: A variável assintótica é o verdadeiro tamanho do grafo ($|V|$), não um parâmetro fixo.
• Não-Vacuo: Ele limita o custo de uma execução de menor custo que é provada existir.

O artigo também estabelece o limite $O(m \log^{2/3} n)$ para o modelo de custo abstrato realizado pela estrutura concreta de baldes, confirmando a escala de inserção de $O(\log(N/M))$.

Significância e Escopo
Os autores enquadram explicitamente a significância deste trabalho como uma formalização rigorosa da correção da recorrência BMSSP e de sua análise de tempo de execução cobrada, em vez de uma verificação completa de ponta a ponta da implementação SSSP de Duan–Mao–Mao–Shu–Yin.

• O que é Reivindicado: O artigo reivindica ter verificado a correção da lógica da recorrência e a validade da análise de custo de operação cobrada, incluindo um limite assintótico não-vacuo para uma família específica ilimitada.
• O que Não é Reivindicado: Os autores não reivindicam ter verificado a complexidade de passo de máquina do código SML exportado, nem reivindicam um limite universal para todos os grafos ou para todas as execuções. Eles declaram explicitamente que o limite paramétrico de tamanho limita a execução de menor custo de uma família específica, pois um limite universal é falso para esta família.
• Contribuição Metodológica: O artigo destaca a importância da "não-vacuidade" como uma obrigação de prova de primeira classe na complexidade mecanizada. Demonstra que teoremas assintóticos podem ser logicamente válidos, mas vazios se a família de entrada for limitada ou se as execuções não existirem. O "livro-razão de não-vacuidade" (provando crescimento, existência de execução e realização de regime) é apresentado como um modelo reutilizável para futuras formalizações de argumentos de complexidade recursiva.

Em resumo, o trabalho fornece uma base de alta confiabilidade e verificada por máquina para a recorrência BMSSP, separando rigorosamente a correção funcional da análise de custo e navegando cuidadosamente pelos obstáculos da formalização de complexidade amortizada para garantir que os limites assintóticos resultantes sejam significativos.