A Profile-Separation Framework for Quantitative Convergence of No-U-Turn Samplers

Resumo Técnico: Um Framework de Separação de Perfil para a Convergência Quantitativa de Amostradores No-U-Turn

Enunciado do Problema
O Hamiltoniano Monte Carlo (HMC) gera propostas distantes através da simulação de trajetórias hamiltonianas, mas sua eficiência depende criticamente do tempo de integração. Trajetórias muito curtas resultam em pouco movimento, enquanto trajetórias muito longas retratam regiões já visitadas, desperdiçando computação. O amostrador No-U-Turn (NUTS) aborda isso construindo adaptativamente uma órbita de leapfrog e encerrando-a quando diagnósticos de extremidade indicam um "U-turn" (vetores de momento apontando de volta para o início). Embora o NUTS seja central para o sucesso prático de sistemas de programação probabilística (ex: Stan, PyMC), sua regra de parada recursiva e dependente do estado historicamente obstruiu o desenvolvimento de uma teoria de mistura quantitativa. Limites não assintóticos existentes para o NUTS basearam-se amplamente em estruturas alvo Gaussianas, onde os diagnósticos aleatórios de U-turn se concentram em torno de uma função seno determinística. Estender esses resultados para alvos fortemente log-côncavos gerais permanece um desafio significativo devido à dependência conjunta da transição com o refrescamento do momento, decisões de duplicação aleatórias, erros numéricos de energia e a regra de seleção específica.

Metodologia
Este artigo introduz um Framework de Separação de Perfil para estabelecer a convergência quantitativa para variantes multinomiais e progressivas-viesadas do NUTS em alvos $(m, L)$-fortemente log-côncavos que satisfazem a regularidade de Hessian de Frobenius. A metodologia central envolve o desacoplamento do mecanismo de parada adaptativo da análise de mistura através das seguintes etapas:

1. Perfil de U-Turn Estacionário: O autor define um objeto populacional determinístico, o perfil estacionário $u(t) = \mathbb{E}[V_0^\top (X_t - X_0)]$, que representa a média de equilíbrio dos diagnósticos de extremidade usados pelo NUTS. Para alvos gerais, isso substitui as funções seno Gaussianas explícitas.
2. Separação de Perfil: Uma condição suficiente é introduzida onde uma profundidade específica $k^*$ é "separada de perfil". Isso exige que o perfil $u(t)$ seja uniformemente positivo em todas as durações diádicas pré-terminais e uniformemente negativo na duração terminal candidata, com uma margem de ordem $d/\sqrt{m}$.
3. Estabilidade de Diagnóstico Intrínseco: O framework quantifica o desvio entre os diagnósticos numéricos práticos (baseados em leapfrog) e o perfil populacional exato. Isso envolve limitar:
   • A concentração dos diagnósticos escalares exatos em torno de $u(t)$.
   • O erro numérico de leapfrog nesses diagnósticos.
   • A falha de janelas de energia uniformes.
   • A falha de positividade em intervalos muito curtos.
4. Certificação de Profundidade Terminal: Sob a suposição de que a margem de separação de perfil excede os erros estocásticos e numéricos combinados, o autor prova que, em um evento de alta probabilidade, cada realização das decisões de duplicação aleatória termina na mesma cardinalidade $K^*$ via um U-turn genuíno, estritamente antes do limite de profundidade máxima.
5. Transferência de Profundidade-Terminal-para-Condutância: Uma vez que uma profundidade terminal e uma janela de energia comuns são certificadas, mostra-se que a transição NUTS contém uma mistura explícita de propostas de leapfrog de índice fixo. O autor utiliza a simetria de ponto inicial da duplicação aleatória e identidades de detalhe de equilíbrio para construir operadores positivos (projeções ortogonais para multinomial, esqueletos de dois passos para progressivo-viesado) que permitem a aplicação da isoperimetria de Cheeger para derivar limites de condutância restritos.

Contribuições Principais

1. Certificado de Parada Independente do Alvo: O artigo abstrai o mecanismo de perfil determinístico das análises Gaussianas para a "separação de perfil", uma condição aplicável a alvos fortemente log-côncavos gerais. Isso fornece um certificado intrínseco que transfere sinais para cada órbita completa e subárvore recursiva inspecionada pela árvore de leapfrog prática.
2. Teorema de Profundidade-Terminal-para-Condutância: Um novo teorema estabelece que, uma vez certificada uma profundidade terminal comum, a transição NUTS adaptativa pode ser limitada por estimativas de movimento de tempo fixo. Isso separa o problema da trajetória (provar onde a trajetória para) do problema de mistura (provar que o kernel cruza cortes).
3. Operadores Positivos para Kernels Não-Preguiçosos: O autor demonstra que os kernels originais multinomiais e progressivos-viesados (sem lazificação artificial) possuem propriedades espectrais positivas. O re-enraizamento multinomial é mostrado como uma projeção ortogonal, enquanto o esqueleto de dois passos do kernel progressivo-viesado é positivo semidefinido, permitindo argumentos de condutância sem modificar o amostrador.
4. Análise Geral de Trajetória e Numérica: O trabalho fornece identidades de equilíbrio para perfis não lineares, desigualdades de deslocamento de média-quadrado e limites universais de positividade inicial. Estabelece a concentração de diagnósticos exatos e comparações determinísticas de leapfrog-para-fluxo sem exigir limites sobre o Jacobiano completo do Hamiltoniano.
5. Rotas de Verificação: O artigo oferece rotas de verificação específicas para o certificado intrínseco, incluindo representações espectrais para produtos não lineares, limites perturbativos para alvos quase isotrópicos e condições para adaptação métrica para remover anisotropia linear.

Resultados
O teorema principal (Teorema 3.7) fornece limites de transição incondicionais para mistura de warm-start. Seja $T^*$ o comprimento da trajetória física selecionada e $a^* = \sqrt{m}T^*$. O número de transições $n$ necessário para atingir erro de variação total $\epsilon$ é limitado por:

• NUTS Multinomial: $\tilde{O}\left( (1 + a^{*2}\kappa^2(1+\gamma)^{4/3}) \log(M/\epsilon) \right)$
• NUTS Progressivo-Viesado: $\tilde{O}\left( (1 + a^{*4}\kappa^3(1+\gamma)^2) \log(M/\epsilon) \right)$

onde $\kappa = L/m$ é o número de condição e $\gamma$ relaciona-se com a regularidade de Hessian.

Em relação ao trabalho computacional, o artigo distingue entre transições certificadas e não certificadas. No evento de certificação, o custo é proporcional à profundidade $K^*$ selecionada. Sem restrições adicionais sobre o limite de profundidade máxima, o limite de trabalho determinístico incondicional é proporcional ao limite máximo $K_{cap}$. No entanto, o autor fornece limites refinados esperados e de alta probabilidade que interpolam entre $K^*$ e $K_{cap}$, recuperando a ordem determinística $K^* n$ quando o limite é comparável à profundidade certificada.

Para alvos Gaussianos, o framework recupera a dependência de dimensão $\tilde{O}(d^{1/4})$ e caracteriza explicitamente os regimes "acelerados" e "presos" identificados na literatura anterior específica de Gaussianas, mostrando que a separação de perfil recupera a dicotomia de duas escalas.

Significância e Alegações
O artigo alega fornecer a primeira teoria de mistura quantitativa para o NUTS prático em alvos fortemente log-côncavos gerais que não depende de estrutura Gaussiana ou modificações artificiais (como lazificação ou correções de Metropolis). A principal contribuição é uma redução de trajetória-para-mistura, demonstrando que o mecanismo de parada adaptativo do NUTS prático comporta-se de forma suficientemente previsível para que as estimativas de tempo fixo de HMC se tornem úteis, desde que o perfil estacionário esteja separado de zero pela soma dos erros estocásticos e numéricos.

O autor enfatiza que os resultados são globais e incondicionais em relação aos limites de transição, enquanto o trabalho computacional é contabilizado separadamente para refletir a realidade de que transições não certificadas (executando até o limite) permanecem como parte da cadeia de Markov. O framework valida o uso de métricas pós-warmup fixas para remover anisotropia linear e fornece uma base rigorosa para o sucesso empírico do NUTS em cenários de alta dimensão e não Gaussianos. O artigo não afirma que a separação de perfil é necessária para uma mistura rápida, mas sim que é uma condição suficiente que unifica a análise de HMC adaptativo através de uma ampla classe de alvos.