Quantum Bayesian Networks: Compositionality and Typing via Linear Logic

1. Declaração do Problema

Contexto:
Redes Bayesianas (RBs) são o framework padrão para raciocínio probabilístico e inferência causal em sistemas clássicos. Elas dependem de um Grafo Acíclico Direcionado (DAG), onde os nós representam variáveis aleatórias e as arestas representam dependências condicionais. A semântica de uma RB é definida por uma distribuição de probabilidade conjunta fatorada em Tabelas de Probabilidade Condicional (TPCs). Uma força-chave das RBs clássicas é a composicionalidade: a capacidade de calcular distribuições marginais (inferência) realizando operações locais (produto e soma-fora) em fatores sem construir a distribuição conjunta completa.

A Lacuna:
Ao estender RBs para sistemas quânticos (Redes Bayesianas Quânticas ou RBQs), frameworks existentes (especificamente a abordagem baseada em instrumentos de Henson, Lal e Pusey [10]) enfrentam duas limitações críticas:

1. Falta de Composicionalidade: A definição padrão exige uma ordem de avaliação global, de cima para baixo. Não permite que a semântica de uma sub-rede seja computada independentemente e depois composta com outras. Isso impede o raciocínio modular.
2. Incompatibilidade de Operações: A inferência clássica depende do "compartilhamento" de variáveis (multiplicando fatores sobre variáveis compartilhadas). A mecânica quântica, governada pelo Teorema da Não-Clonagem, proíbe a duplicação de estados quânticos. Redes de tensores padrão lidam com dados quânticos, mas carecem do mecanismo para lidar eficientemente com a "soma-fora" (marginalização) de variáveis ocultas de uma maneira que preserve a eficiência dos algoritmos de inferência clássica.

Objetivo:
Os autores visam desenvolver um formalismo para RBQs que:

• Generalize RBs clássicas para incluir dados quânticos.
• Restaure a composicionalidade e a modularidade (permitindo que sub-redes sejam definidas e compostas independentemente).
• Garanta a tipagem para assegurar que composições resultem em DAGs válidos (sem ciclos).
• Mantenha compatibilidade com técnicas de inferência clássica existentes.

---

2. Metodologia

Os autores empregam uma abordagem dual combinando Semântica Denotacional (especificamente adaptando o trabalho de Selinger) e Teoria da Prova (Lógica Linear).

A. Fatores Quânticos (Q-fatores)

A inovação matemática central é a introdução de Fatores Quânticos (Q-fatores).

• Definição: Um Q-fator é uma função $\phi: \text{Val}(X) \to \mathcal{L}(\mathcal{H}_Q)^+$, mapeando atribuições de variáveis clássicas para operadores positivos em um espaço de Hilbert (registro quântico).
• Unificação: Esta definição unifica fatores clássicos (onde o espaço de Hilbert é unidimensional) e estados quânticos (onde o conjunto clássico é vazio).
• Operações: Os autores definem duas operações em Q-fatores:
  1. Produto ($\odot$): Combina dois Q-fatores. Crucialmente, para variáveis clássicas, comporta-se como a multiplicação padrão de fatores (compartilhando valores). Para registros quânticos, comporta-se como o produto tensorial, mas usa uma diferença simétrica ($Q_1 \Delta Q_2$) para o escopo do registro resultante, respeitando o Teorema da Não-Clonagem (qubits são consumidos/mergulhados, não duplicados).
  2. Soma-fora ($\sum$): Marginaliza variáveis.
     • Para variáveis clássicas: Soma sobre valores.
     • Para registros quânticos: Rastreamento parcial ($\text{tr}$).
• Fechamento: O conjunto de Q-fatores é fechado sob produto e soma-fora, permitindo computação modular de marginais.

B. TPCs Quânticas (Q-tpcs)

Para garantir que a semântica de uma rede resulte em uma distribuição de probabilidade válida (e não apenas em um operador positivo arbitrário), os autores definem TPCs Quânticas.

• Estas são Q-fatores satisfazendo condições específicas de normalização (análogas a matrizes estocásticas para variáveis clássicas e estados de Choi para canais quânticos).
• Uma RBQ é definida como um DAG onde cada nó está associado a uma Q-tcp.

C. Formalismo Gráfico Tipado (Lógica Linear)

Para abordar a modularidade e a prevenção de ciclos (propriedade DAG), os autores codificam RBQs em Redes de Prova da Lógica Linear Multiplicativa (MLL).

• Tipos: Variáveis clássicas e qubits são atribuídos polaridades (positivo/negativo).
  • Átomos negativos ($X^-, q^-$) representam entradas.
  • Átomos positivos ($X^+, q^+$) representam saídas.
• Caixas: Nós na RBQ são representados como "caixas" na rede de prova, contendo uma Q-tcp.
• Polaridade e DAGs: A polaridade das fórmulas induz uma orientação nas arestas do grafo. Os autores provam que uma rede de prova "polarizada" corresponde exatamente a um DAG.
• Composição: Duas redes de prova podem ser compostas via Regra de Corte se seus tipos forem duais (por exemplo, $A$ e $A^\perp$). Esta disciplina de tipagem garante estaticamente que o grafo resultante é um DAG válido.

---

3. Contribuições Principais

1. Definição de Fatores Quânticos (Q-fatores):

   • Um novo objeto matemático que generaliza fatores clássicos e redes de tensores.
   • Resolve a tensão entre o compartilhamento de variáveis clássicas e a não-clonagem quântica, definindo uma operação de produto que lida com o compartilhamento clássico e a fusão quântica (via diferença simétrica de registros).

2. Semântica Composicional para RBQs:

   • O artigo reformula RBQs de modo que a semântica de toda a rede seja o produto da semântica de suas sub-redes ($\llbracket B \rrbracket = \llbracket B_1 \rrbracket \odot \llbracket B_2 \rrbracket$).
   • Isso permite inferência modular: pode-se calcular a marginal de um subcomponente somando variáveis ocultas localmente, uma característica ausente em definições anteriores baseadas em instrumentos.

3. Disciplina de Tipagem via Lógica Linear:

   • Os autores mapeiam RBQs para redes de prova MLL.
   • Provam que a tipagem garante modularidade: compor duas redes de prova bem tipadas (via corte) sempre produz uma rede de prova válida (e, portanto, um DAG válido), prevenindo a formação de ciclos causais.
   • Isso fornece uma verificação estática para a validade estrutural de modelos causais quânticos.

4. Provas de Equivalência:

   • A definição baseada em Q-fatores é provada equivalente à definição baseada em instrumentos em [10].
   • A semântica de uma RBQ é mostrada como idêntica à semântica de sua rede de prova quântica correspondente.

---

4. Resultados

• Equivalência Teórica: O artigo estabelece que o novo formalismo de Q-fatores é matematicamente equivalente às RBQs baseadas em instrumentos existentes, mas oferece propriedades estruturais superiores (composicionalidade).
• Preservação de Limites Clássicos:
  • Se todos os nós forem clássicos, o produto de Q-fatores reduz-se à multiplicação padrão de fatores, e o framework colapsa para Redes Bayesianas padrão.
  • Se todos os nós forem quânticos, o framework comporta-se como Redes de Tensores.
• Invariância da Semântica: A semântica de uma rede de prova é invariante sob redução (eliminação de corte). Isso significa que a ordem de computação (etapas de redução) não altera a distribuição de probabilidade final, garantindo a robustez do processo de inferência.
• Modularidade: O sistema de tipagem previne com sucesso a construção de grafos cíclicos (por exemplo, o exemplo na Fig. 4 onde $N_0$ e $N_2$ não podem ser compostos porque seus tipos são incompatíveis, enquanto $N_0$ e $N_1$ compõem-se em um DAG válido).

---

5. Significado

• Ponte entre Inferência e Causalidade: O trabalho integra com sucesso a perspectiva de modelagem causal (RBQs) com a perspectiva de inferência eficiente (algoritmos baseados em fatores). Modelos causais quânticos anteriores frequentemente lutavam para suportar a marginalização eficiente de variáveis ocultas.
• Potencial Algorítmico: Ao estabelecer que Q-fatores são fechados sob produto e soma-fora, o artigo abre caminho para adaptar algoritmos clássicos de inferência eficiente (como Eliminação de Variáveis ou Propagação de Crenças) ao domínio quântico.
• Rigor Fundacional: O uso da Lógica Linear fornece uma fundação rigorosa, baseada em teoria dos tipos, para estruturas causais quânticas. Avança além de definições ad hoc para um sistema onde propriedades estruturais (como aciclicidade) são garantidas pelo sistema de tipos.
• Aplicações Futuras: Este framework é essencial para:
  • Criptografia Independente de Dispositivos: Analisar protocolos onde a confiança em dispositivos é minimizada.
  • Aprendizado de Máquina Quântico: Desenvolver modelos que possam raciocinar sobre dados mistos clássico-quânticos.
  • Fundamentos da Física: Fornecer uma linguagem formal para discutir não-localidade e emaranhamento dentro de um framework de inferência causal.

Em resumo, o artigo resolve o "problema de composicionalidade" em Redes Bayesianas Quânticas introduzindo Q-fatores e um sistema de tipagem de Lógica Linear, permitindo raciocínio modular, eficiente e estruturalmente sólido sobre sistemas causais mistos clássico-quânticos.