Towards Neuro-symbolic Causal Rule Synthesis, Verification, and Evaluation Grounded in Legal and Safety Principles

1. Declaração do Problema

O artigo aborda limitações críticas em sistemas baseados em regras utilizados em domínios críticos para a segurança (por exemplo, condução autónoma, controlo industrial):

• Fragilidade e Escalabilidade: Os sistemas tradicionais baseados em regras têm dificuldades na manutenção. Alterações menores nos requisitos frequentemente desencadeiam revisões em cascata através de regras interdependentes, criando um "gargalo de aquisição de conhecimento".
• Especificação Incorreta de Objetivos: Os sistemas de IA frequentemente otimizam objetivos estreitos e literais (hacking de recompensa) em vez da verdadeira intenção dos designers humanos. Isso ocorre porque os objetivos humanos são frequentemente vagos, dependentes do contexto e informais, enquanto a IA requer especificações precisas e formais.
• Falta de Rastreabilidade: Os métodos existentes frequentemente carecem de um vínculo claro e rastreável entre princípios humanos de alto nível (legais/de segurança) e as regras lógicas de baixo nível que governam o comportamento do sistema.

O desafio central é criar um sistema capaz de sintetizar, verificar e avaliar incrementalmente regras formais derivadas de objetivos e princípios em linguagem natural, garantindo que sejam mínimas, necessárias, suficientes e seguras.

2. Metodologia

Os autores propõem uma extensão a um Framework Causal Neuro-Simbólico (NeSy) anterior. A nova arquitetura introduz uma Camada de Síntese e Verificação de Nível Meta que se situa acima do ciclo de feedback padrão MAPE-K (Monitorizar-Analisar-Planear-Executar).

A. A Arquitetura Central

O sistema integra três espaços de representação:

1. Árvores de Abdução Simbólica (SAT): Lógica de primeira ordem (FOL) para codificar conhecimento de domínio e explicar violações.
2. Modelos Causais Estruturais (SCM): Para representar dependências e suportar raciocínio contrafactual.
3. Aprendizagem por Reforço Profunda (DRL): Para tomada de decisão operacional.

O novo Nível de Síntese e Verificação atua como um ciclo meta fechado, atualizando a teoria FOL governante do sistema com base na entrada humana e na deteção de anomalias.

B. O Pipeline de Síntese (Sintetizador de Objetivos/Regras)

Este pipeline utiliza Modelos de Linguagem de Grande Escala (LLMs) para transformar objetivos em linguagem natural em regras formais através de quatro etapas:

1. Decomposição em Causas: O LLM decompõe um objetivo de alto nível (efeito) em causas candidatas (condições/comportamentos) necessárias para o alcançar, restringido por princípios de segurança e legais.
2. Consolidação Semântica: O LLM identifica e funde causas sobrepostas ou redundantes para criar um conjunto único de condições, reduzindo a ambiguidade.
3. Tradução Simbólica: As causas em linguagem natural consolidadas são traduzidas em predicados e regras de Lógica de Primeira Ordem (FOL). O LLM fornece explicações para estas traduções para garantir o alinhamento semântico.
4. Avaliação de Necessidade e Suficiência: O sistema analisa combinações de causas para determinar:
   • Necessidade Individual: Uma causa específica é essencial por si só?
   • Conjuntos Mínimos Necessários: Qual é o menor conjunto de causas necessário para tornar o efeito impossível se removido?
   • Conjuntos Mínimos Suficientes: Quais combinações de causas garantem que o efeito ocorre?

C. O Pipeline de Verificação (Motor de Verificação de Regras)

Antes de as regras serem integradas na base de conhecimento, elas passam por uma verificação automatizada de três estágios:

1. Validação de Sintaxe e Esquema: Garante que as regras conformam-se à linguagem lógica e às ontologias de domínio.
2. Análise de Consistência Lógica: Verifica contradições contra a base de conhecimento FOL existente.
3. Verificação de Segurança e Invariantes: Verifica formalmente (utilizando solucionadores como o Z3) que as regras preservam propriedades críticas do sistema (por exemplo, evitamento de colisões).

Apenas as regras que passam em todos os estágios são comprometidas na base de conhecimento, orientando a adaptação futura.

3. Contribuições Principais

• Ciclo de Síntese de Nível Meta: Uma arquitetura inovadora que trata a manutenção de regras como um processo incremental e rastreável, afastando-se de bases de regras monolíticas em direção a conjuntos de regras modulares ligados a objetivos.
• Abdução Causal Guiada por LLM: Demonstrar como os LLMs podem ser restringidos para realizar raciocínio abdutivo estruturado (geração de causas a partir de efeitos) e raciocínio dedutivo (avaliação de necessidade/suficiência) fundamentado em domínios legais e de segurança específicos.
• Formalização de Conjuntos "Necessários e Suficientes": Um método sistemático para derivar conjuntos de regras mínimas que garantem objetivos de segurança, abordando a questão da sobre-especificação ou sub-especificação em objetivos de IA.
• Rastreabilidade: Cada regra sintetizada está explicitamente ligada de volta ao seu objetivo humano originário e princípio legal, melhorando a auditabilidade e a explicabilidade.

4. Resultados (Prova de Conceito)

Os autores avaliaram a abordagem utilizando uma implementação de Prova de Conceito em dois cenários de condução autónoma, utilizando o GPT-4o Mini da OpenAI e um conjunto curado de regulamentos de trânsito alemães e princípios de segurança física.

• Cenário 1: Fusão em Tráfego Intenso
  • O sistema decompôs com sucesso o objetivo em 4 causas consolidadas únicas.
  • Identificou que, embora algumas causas não fossem individualmente necessárias, eram essenciais dentro de conjuntos mínimos necessários específicos.
  • Derivou um único Conjunto Mínimo Suficiente contendo todas as quatro causas, garantindo uma fusão segura.
• Cenário 2: Manutenção de Velocidade Constante numa Autoestrada
  • O sistema identificou 6 causas únicas, estreitando-as para 3 condições individualmente necessárias (controlo, limites de velocidade, atrito).
  • Gerou dois Conjuntos Mínimos Suficientes distintos, mostrando que diferentes combinações de condições (por exemplo, presença de obstáculos vs. alterações no tráfego) poderiam satisfazer o objetivo.
• Tradução Simbólica: O LLM mapeou com sucesso condições complexas em linguagem natural (por exemplo, "distância suficiente") em regras FOL precisas (por exemplo, ∀x(sd_front(x) ∧ sd_rear(x) ← ¬dense(x))).

Resultado: O pipeline derivou com sucesso conjuntos de regras mínimos, necessários e suficientes a partir de objetivos de alto nível, formalizando-os como restrições lógicas sem alucinar comportamentos inseguros.

5. Significado e Trabalho Futuro

• Preenchimento da Lacuna: O trabalho preenche a lacuna entre a intenção humana vaga e a verificação formal rigorosa, oferecendo um caminho para mitigar o "hacking de recompensa" e a especificação incorreta de objetivos em IA.
• Escalabilidade: Ao localizar alterações de regras em módulos específicos ligados a objetivos, a abordagem reduz o fardo de manutenção e o risco de falhas em cascata em grandes conjuntos de regras.
• Garantia de Segurança: A integração de um motor de verificação garante que apenas regras logicamente consistentes e que preservam a segurança sejam implementadas, algo crucial para sistemas críticos para a segurança.

Limitações e Direções Futuras:

• A abordagem atual depende de um conjunto pré-definido de regulamentos; o trabalho futuro visa expandir a cobertura de domínio.
• O LLM atua como uma "caixa preta" e a sensibilidade aos prompts permanece um desafio.
• Planos futuros incluem a integração de solucionadores automatizados para detetar conflitos entre regras novas e existentes e a incorporação de raciocínio probabilístico para lidar com incerteza de forma mais robusta.

Em conclusão, este artigo apresenta uma estrutura robusta para Síntese Causal Neuro-Simbólica de Regras, demonstrando que a combinação de LLMs com lógica formal e raciocínio causal pode criar sistemas de IA adaptativos, explicáveis e seguros, fundamentados em princípios legais e de segurança humanos.