Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

Este artigo apresenta o Delta1, um pipeline neuro-simbólico que integra um gerador de teoremas determinístico baseado na Contradição Padrão Triangular Completa (FTSC) com Modelos de Linguagem de Grande Escala (LLMs) para produzir raciocínio explicável, auditável e alinhado a domínios específicos, como saúde e conformidade regulatória.

O essencial

Imagine que você tem um engenheiro de lógica extremamente rigoroso e um contador de histórias muito talentoso trabalhando juntos. É assim que funciona o sistema ∆1–LLM descrito neste artigo.

Aqui está a explicação simples, usando analogias do dia a dia:

1. O Problema: A Confusão entre "Cérebro" e "Bússola"

Hoje, temos duas ferramentas poderosas, mas elas têm defeitos opostos:

• Os Grandes Modelos de Linguagem (LLMs): São como contadores de histórias incríveis. Eles escrevem textos bonitos, parecem inteligentes e entendem o contexto. Mas, às vezes, eles "alucinam" (inventam fatos) e não têm certeza absoluta se o que dizem é logicamente verdadeiro. É como um amigo que conta uma história emocionante, mas você não sabe se ela é 100% real.
• A Lógica Simbólica (Sistemas Tradicionais): São como engenheiros de precisão. Eles seguem regras matemáticas estritas. Se algo é verdadeiro, eles provam. Se é falso, eles mostram o erro. O problema é que eles são "mudos" e difíceis de entender. Eles podem dizer "Erro 404: Inconsistência", mas não explicam por que isso aconteceu em uma linguagem que um humano comum entenda.

O mundo precisa de algo que tenha a precisão do engenheiro e a clareza do contador de histórias.

2. A Solução: A Dupla Dinâmica (∆1 + LLM)

Os autores criaram uma equipe onde cada um faz o que faz de melhor:

O Engenheiro: ∆1 (O Gerador de Teoremas)

Pense no ∆1 como um arquiteto de labirintos.

• Ele pega regras do mundo real (como leis, regras médicas ou contratos) e as transforma em blocos de construção lógicos.
• Em vez de tentar adivinhar ou procurar aleatoriamente por erros (como um detetive perdido), ele constrói o erro de propósito, de forma matemática e garantida.
• Ele usa uma técnica chamada "Contradição Padrão Triangular Completa" (FTSC). Imagine que você tem várias peças de um quebra-cabeça. O ∆1 organiza essas peças de todas as formas possíveis para ver exatamente onde elas não encaixam.
• O Grande Truque: Ele não apenas diz "tem um erro". Ele diz: "Se você tirar esta peça específica (A), o resto funciona. Mas se você tentar colocar A de volta, o castelo desmorona." Ele encontra o mínimo de erros necessários para causar o problema. É como dizer: "O problema não é o castelo todo, é apenas esta única pedra solta."

O Contador de Histórias: O LLM (A Tradutora)

Agora, imagine que o LLM é o tradutor que pega o relatório técnico do arquiteto e o transforma em uma história para o cliente.

• O ∆1 entrega uma lista fria de símbolos: "A + B + C = Contradição".
• O LLM pega isso e diz: "Olha, a regra de 'Privacidade' e a regra de 'Transparência' estão brigando. Se você prometer privacidade total, não pode ser totalmente transparente. Precisamos ajustar uma delas."
• Ele transforma a lógica fria em conselhos acionáveis, como um médico explicando um diagnóstico ou um advogado sugerindo como mudar uma cláusula de contrato.

3. Como Funciona na Prática? (Exemplos)

O artigo mostra como isso funciona em situações reais:

• Na Medicina:

  • Cenário: Um paciente tem infecção, febre e alto nível de glóbulos brancos. O sistema diz que precisa de antibióticos. Mas e se a regra de "antibiótico" entrar em conflito com outra regra de segurança?
  • Ação do ∆1: Ele descobre matematicamente que, com todas as regras atuais, é impossível tratar o paciente sem violar uma regra. Ele isola a regra exata que causa o conflito.
  • Ação do LLM: Explica ao médico: "A regra de dar antibióticos automaticamente entra em conflito com a necessidade de confirmar o tipo de infecção. Sugiro adicionar uma etapa de confirmação antes de prescrever."

• Em Contratos e Leis:

  • Cenário: Uma empresa tem regras de "Fornecimento Exclusivo" e "Rescisão Sem Justa Causa".
  • Ação do ∆1: Mostra que essas duas regras são como tentar segurar um balão de água e um balão de ar ao mesmo tempo; eles se anulam.
  • Ação do LLM: Diz ao advogado: "Você não pode ter exclusividade total e ainda permitir que o cliente cancele o contrato a qualquer momento sem motivo. Isso cria uma contradição. Vamos ajustar o contrato para que a rescisão só ocorra em casos específicos."

4. Por que isso é revolucionário?

A grande inovação aqui é a "Explicabilidade por Construção".

• Antes: As IAs tentavam adivinhar a resposta e depois inventavam uma desculpa para parecerem inteligentes. Era como um aluno que chuta a resposta na prova e depois tenta explicar a lógica de trás dela.
• Agora (∆1 + LLM): O sistema constrói a resposta correta e a explicação ao mesmo tempo. A explicação não é um "pós-processamento"; ela é parte da estrutura da prova.
  • É como se o arquiteto (∆1) não apenas desenhasse o prédio, mas também entregasse um manual de instruções escrito pelo contador de histórias (LLM) que explica exatamente onde estão as vigas e por que o prédio não vai cair.

Resumo Final

Este trabalho é como criar uma ponte segura entre a matemática dura e a linguagem humana.

1. O ∆1 garante que a lógica seja perfeita, sem erros e sem "alucinações".
2. O LLM garante que a lógica seja compreensível, útil e conversável.

Juntos, eles permitem que máquinas não apenas "pensem" logicamente, mas que expliquem seu pensamento de forma que humanos possam confiar, auditar e corrigir. É um passo gigante para uma Inteligência Artificial que não é apenas inteligente, mas também confiável e transparente.

Resumo técnico

Resumo Técnico: ∆1–LLM

1. O Problema

O campo da inteligência artificial enfrenta uma dicotomia fundamental entre duas abordagens de raciocínio:

• Abordagens Simbólicas (Lógica): Oferecem rigor formal, garantias de correção (sonoridade) e estrutura de inferência transparente, mas carecem de expressividade linguística e dificuldade em gerar explicações naturais para humanos.
• Abordagens Neurais (LLMs): Oferecem fluência linguística, adaptabilidade e capacidade de gerar explicações coerentes, mas carecem de garantias de correção, sendo propensas a alucinações e raciocínio estocástico (não verificável).

A lacuna atual reside na falta de sistemas que unam a sonoridade formal da lógica com a interpretabilidade dos Grandes Modelos de Linguagem (LLMs) de forma intrínseca, e não apenas post-hoc (após a geração). Sistemas existentes de prova automática (ATPs) frequentemente produzem rastros de prova opacos ou espaços de busca infinitos e não estruturados.

2. Metodologia: A Arquitetura ∆1 + LLM

O artigo propõe um pipeline end-to-end de "explicabilidade por construção" (explainability-by-construction), integrando um gerador de teoremas determinístico com uma camada de interpretação neural.

A. O Gerador de Teoremas Automáticos ∆1 (Lado Simbólico)

• Base Teórica: Baseia-se na estrutura formal da Contradição Padrão Triangular Completa (FTSC - Full Triangular Standard Contradiction).
• Mecanismo: Dado um conjunto de $n$ literais de entrada (predicados atômicos) que não contêm pares complementares, o ∆1 constrói deterministicamente um conjunto de cláusulas $S$ que forma uma contradição.
• Geração de Teoremas: Para cada cláusula $C$ no conjunto $S$, o sistema gera um teorema na forma $S \setminus \{C\} \vdash \neg C$. Isso significa que, ao remover uma cláusula, o conjunto restante torna-se satisfiável, provando que a cláusula removida é a fonte mínima de inconsistência.
• Garantias:
  • Determinismo: Não utiliza busca estocástica, backtracking ou solvers SAT externos.
  • Sonoridade e Minimalidade: Garante que os conjuntos de cláusulas são minimamente insatisfiáveis (MUS) por construção.
  • Complexidade: A geração de um único conjunto FTSC ocorre em tempo $O(n^3)$. A enumeração de todas as permutações de literais resulta em $n!$ teoremas não redundantes.
  • Rastro de Prova Transparente: Cada teorema possui um rastro de derivação explícito e reproduzível.

B. A Camada de Interpretação (Lado Neural - LLM)

• Função: O LLM atua como uma camada de "ponte semântica".
• Entrada: Recebe os predicados atômicos extraídos de texto natural (via LLM front-end) e, posteriormente, os teoremas e rastros de prova gerados pelo ∆1.
• Saída:
  1. Verbalização: Transforma a lógica formal (ex: $S \setminus \{D_i\} \vdash \neg D_i$) em explicações em linguagem natural coerentes.
  2. Ranking: Classifica os teoremas com base na saliência contextual ou novidade.
  3. Remediação: Sugere correções práticas para resolver as inconsistências identificadas (ex: adicionar critérios de qualificação, ajustar prazos, revisar cláusulas).

Fluxo de Trabalho:

1. Extração de Predicados: LLM converte texto natural em predicados lógicos ($L = \{x_1, ..., x_n\}$).
2. Geração Determinística: ∆1 constrói o FTSC e gera todos os teoremas minimais.
3. Construção de Rastro: ∆1 gera a sequência de derivação explícita.
4. Explicação e Ação: LLM traduz os teoremas em razões naturais e recomendações de ação.

3. Contribuições Principais

• Pipeline de Integração Neuro-Simbólica: Uma arquitetura que acopla a geração determinística de teoremas do ∆1 com as capacidades interpretativas dos LLMs, garantindo que a explicação seja fundamentada em uma prova lógica verificável.
• Justificativa Teórica e Validação Empírica: Demonstra que o sistema entrega tanto a sonoridade formal quanto a interpretabilidade em nível humano em domínios de alto risco (saúde, conformidade, contratos).
• Explicabilidade por Construção: Diferente de métodos post-hoc, a interpretabilidade é inerente ao processo de geração. Cada explicação é ancorada em um rastro de prova determinístico, eliminando a necessidade de verificação externa.
• Novo Paradigma de Descoberta: Apresenta o ∆1 como um "gerador de universo de teoremas" que cobre o espaço de conflitos de raciocínio mínimos de forma completa e não redundante, servindo como um benchmark para consistência simbólica-neural.

4. Resultados e Estudos de Caso

O framework foi testado em diversos domínios, demonstrando sua capacidade de identificar contradições mínimas e fornecer orientações acionáveis:

• Raciocínio Médico:
  • Cenário: Regras sobre infecção, contagem de leucócitos, febre e uso de antibióticos.
  • Resultado: O sistema identificou que a imposição simultânea de todas as condições criava uma contradição global. O LLM explicou que a prescrição automática de antibióticos sem confirmação de critérios (como teste ou gravidade) era a fonte de inconsistência, sugerindo a adição de critérios de qualificação.
• Gestão de Conformidade e Regulatória:
  • Cenário: Conflitos entre políticas de privacidade (GDPR) e transparência, ou entre leis de diferentes jurisdições (ex: GDPR vs. HIPAA).
  • Resultado: Identificação de que "DataPortability" (portabilidade de dados) era o predicado minimamente inconsistente frente às restrições de retenção e divulgação. O sistema sugeriu ajustes nos limites de retenção para restaurar a satisfabilidade.
• Governança de Contratos:
  • Cenário: Contratos complexos com cláusulas de fornecimento exclusivo, prazos de entrega e penalidades.
  • Resultado: Detecção de que cláusulas de "rescisão sem justa causa" contradiziam a lógica de fornecimento exclusivo e penalidades. O sistema sugeriu condicionar a rescisão a causas justas ou introduzir períodos de cura.

Desempenho:

• O sistema opera de forma determinística e reproduzível.
• Para entradas pequenas ($n=4$ ou $5$), o tempo de processamento é trivial, mas a estrutura garante completude lógica.
• A combinação permite que especialistas humanos rastreiem o raciocínio desde a extração do predicado até a explicação final.

5. Significado e Impacto

• Avanço na IA Explicável (XAI): O trabalho move a IA de "prova automática" para "compreensão automática de teoremas". Ele resolve o problema da "caixa preta" ao garantir que a explicação não é uma alucinação do modelo de linguagem, mas uma tradução fiel de uma prova lógica formal.
• Fundação para Sistemas Confiáveis: Oferece uma base para sistemas de decisão em áreas críticas (saúde, direito, finanças) onde a auditoria e a correção lógica são obrigatórias.
• Benchmarking: O conjunto de teoremas gerados pelo ∆1 serve como um "TPTP para explicabilidade", permitindo avaliar a consistência lógica de outros sistemas neuro-simbólicos.
• Futuro: Abre caminho para agentes de descoberta de teoremas auto-reflexivos que alternam entre geração, prova e explicação, aproximando-se do raciocínio humano iterativo.

Em suma, o ∆1–LLM representa um marco na convergência entre lógica, linguagem e aprendizado, estabelecendo que a rigorosidade formal e a inteligibilidade humana podem coexistir e se reforçar mutuamente através de uma arquitetura de construção determinística.