Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

O artigo apresenta o Elenchus, um sistema de diálogo que utiliza a interação entre um especialista humano e um modelo de linguagem para construir bases de conhecimento baseadas em semântica inferencialista, mapeando os estados dialéticos para a lógica NMMS e demonstrando sua eficácia na eliciação e verificação formal das tensões de design da ontologia PROV-O.

O essencial

Imagine que você é um especialista em um assunto complexo, como a construção de uma cidade ou a criação de um novo tipo de lei. Tradicionalmente, para transformar seu conhecimento em um "manual" ou "banco de dados" que computadores possam usar, você teria que sentar com um engenheiro de conhecimento e tentar explicar tudo, palavra por palavra, como se estivesse transcrevendo um livro mental que já existe na sua cabeça. O problema é que, muitas vezes, nem nós sabemos exatamente o que pensamos até tentarmos explicar.

O artigo "Elenchus" propõe uma maneira totalmente nova e mais inteligente de fazer isso. Vamos usar uma analogia para entender:

A Metáfora do "Advogado e o Detetive"

Imagine que você é um Advogado (o especialista humano) e você tem um Detetive (uma Inteligência Artificial, um LLM) como seu oponente.

1. O Objetivo: O objetivo não é o Detetive adivinhar o que você sabe. O objetivo é que vocês dois joguem um jogo de "perguntas e respostas" para descobrir o que realmente faz sentido no seu conhecimento.
2. O Jogo (Diálogo):
   • Você começa dizendo: "Eu acredito que X é verdade".
   • O Detetive olha para o que você disse e pergunta: "E se X for verdade, isso significa que Y também é verdade? Mas você disse que Y é falso. Isso não é uma contradição?"
   • Aqui está a mágica: O Detetive não está tentando te vencer ou te humilhar. Ele é um parceiro de teste. Ele aponta onde suas ideias podem estar "batendo de frente" (incoerentes).
3. A Resolução:
   • Você, como o especialista, tem o poder final. Você pode dizer: "Ah, você tem razão, eu mudei de ideia sobre X" (retração).
   • Ou: "Não, eu não disse que Y é falso, eu disse que Z é falso" (refinamento).
   • Ou: "Não, isso não é uma contradição, você entendeu errado" (contestação).

O Que é o "Elenchus"?

O Elenchus é o nome desse sistema. Ele é como uma máquina de polir ideias.

• Antes: A gente achava que o conhecimento era como um baú fechado na cabeça do especialista. O trabalho era apenas abrir o baú e tirar as coisas.
• Agora (Elenchus): O conhecimento é como uma argamassa que só endurece quando você a mistura e a aperta. O conhecimento só se torna claro e útil enquanto você discute e defende suas ideias contra as perguntas do Detetive.

O Resultado: O "Mapa de Conflitos"

Ao final da conversa, o sistema não gera apenas uma lista de fatos. Ele gera um Mapa de Relações Lógicas (chamado de "Base Material").

Pense nisso como um mapa de trânsito:

• Ele mostra quais ruas (ideias) você pode pegar juntas sem bater o carro.
• Ele mostra quais ruas são proibidas de serem usadas ao mesmo tempo (incoerências).
• O mais legal é que o sistema sabe exatamente por que cada regra existe, porque ele registrou cada vez que você disse "Ok, concordo que essas duas coisas não podem andar juntas".

Por que isso é importante? (O Caso da PROV-O)

Os autores testaram isso com um especialista que ajudou a criar uma norma internacional chamada PROV-O (usada para rastrear a origem de dados na internet).

• Eles pegaram apenas um texto curto de 350 palavras dessa norma.
• O especialista e o Detetive (IA) tiveram uma conversa.
• O sistema conseguiu extrair as decisões de design complexas que os criadores originais levaram anos e milhares de e-mails para definir.
• O sistema descobriu que certas regras não funcionam em cadeia (se A leva a B e B leva a C, não significa que A leva a C automaticamente) e que adicionar mais informações pode, às vezes, invalidar uma regra anterior.

Resumo em uma Frase

O Elenchus transforma a criação de conhecimento de uma "entrevista de extração de dados" (onde o especialista é um livro aberto) em uma "sessão de debate" (onde o especialista e a IA trabalham juntos para forjar um conhecimento sólido, testado e sem contradições).

É como se, em vez de pedir para um arquiteto desenhar a casa inteira de uma vez, você e um assistente de IA fossem construindo a casa tijolo por tijolo, e toda vez que um tijolo parecesse instável, vocês o ajustassem antes de colocar o próximo. No final, você tem uma casa (banco de conhecimento) que é estruturalmente perfeita e você sabe exatamente por que cada parede está onde está.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues", apresentado em português.

1. O Problema: A "Gargalo" de Aquisição de Conhecimento

O artigo aborda o problema persistente da engenharia de conhecimento, especificamente a dificuldade de formalizar conhecimento expresso em linguagem natural por especialistas.

• Crítica às abordagens tradicionais: O autor argumenta que os métodos atuais (sistemas especialistas, ontologias, grafos de conhecimento) partem de uma premissa equivocada: tratam o conhecimento do especialista como um conteúdo interno determinista que precisa apenas ser "extraído" ou transcrito.
• A visão alternativa: O conhecimento não é pré-formado; ele é constituído através de práticas de expressão e negociação. Portanto, a engenharia de conhecimento deve ser reimaginada como explicitação (tornar explícito) das relações inferenciais implícitas na prática do especialista, e não como extração de fatos.

2. Metodologia: O Protocolo Dialético Elenchus

O sistema Elenchus é um protocolo de diálogo bilateral entre um especialista humano (o "Respondente") e um Modelo de Linguagem (LLM) atuando como oponente ("Proponente/Cético").

• Fundamento Semântico: Baseia-se na Semântica Inferencialista (Brandom, Hlobil), onde o significado de uma sentença é definido pelo seu papel inferencial (o que dela se segue, o que a segue e com o que é incompatível), e não por condições de verdade.
• Mecanismo de Interação:
  1. O especialista estabelece uma posição bilateral: um conjunto de compromissos (afirmações) e negações.
  2. O LLM atua como um oráculo derivável defeasível. Ele analisa a posição do especialista e propõe tensões (alegações de incoerência entre compromissos e negações).
  3. O especialista resolve as tensões de três formas:
     • Retratação: Remove um compromisso ou negação.
     • Refinamento: Ajusta a proposição para dissolver o conflito.
     • Contestação: Rejeita a alegação de incoerência feita pelo LLM.
• Controle de Qualidade: O LLM não é a fonte de verdade, mas um parceiro dialético. Se o LLM propõe uma tensão falsa (alucinação), o especialista a contesta. Apenas as tensões aceitas pelo especialista entram na base de conhecimento final. Isso contém estruturalmente a não confiabilidade do LLM.

3. Contribuições Técnicas Principais

A. Mapeamento para Bases Materiais (NMMS)

A contribuição teórica central é o mapeamento dos estados dialéticos do Elenchus para Bases Materiais na lógica NonMonotonic MultiSuccedent (NMMS) de Hlobil e Brandom.

• Estrutura da Base Material ($B_S$): É definida como um par $\langle L_B, \vdash_B \rangle$, onde $L_B$ é a linguagem atômica e $\vdash_B$ é a relação de consequência base.
• Condição de Contenção (Containment): A relação de consequência satisfaz a condição de que afirmar e negar a mesma sentença é incoerente.
• Composição da Relação de Consequência: A relação $\vdash_B$ é a união de dois componentes:
  1. $I$ (Implicações Materiais): Pares de sequentes derivados de tensões aceitas durante o diálogo (incoerências descobertas).
  2. $Cont$ (Contenção): Pares que representam a norma pragmática de consistência bilateral (afirmar e negar o mesmo é incoerente), que é um pressuposto do diálogo.
• Explicitação: A construção da base torna explícitas tanto as incoerências descobertas quanto as normas pragmáticas que sustentam o diálogo.

B. Extensão Lógica via Cálculo de Sequentes

A partir da base material que satisfaz a Contenção, o cálculo de sequentes NMMS permite a elaboração de um vocabulário lógico (conectivos como $\to, \land, \lor, \neg$) com três propriedades garantidas:

1. Supraclassicalidade: Todos os sequentes classicamente válidos são válidos.
2. Conservatividade: A introdução de vocabulário lógico não cria novas consequências no nível base (preserva a estrutura subestrutural).
3. Explicitação: Qualquer relação de consequência material na base pode ser expressa explicitamente usando o vocabulário lógico.

C. Implementação e Rastreabilidade

• O sistema é implementado como um agente Claude Code que utiliza repositórios GitHub para armazenamento persistente do estado dialético (compromissos, desafios, tensões).
• Cada implicação material no resultado final é totalmente rastreável até uma fala específica no diálogo, oferecendo uma proveniência clara que falta em bases extraídas de corpora estatísticos.

4. Resultados: Estudo de Caso com PROV-O

O método foi aplicado à ontologia de proveniência W3C PROV-O (seção 3.1), utilizando apenas a especificação em prosa (350 palavras) como entrada.

• Processo: Um especialista do domínio (ex-editor do PROV) interagiu com o LLM. O diálogo gerou 19 compromissos finais e 9 implicações materiais aceitas após a resolução de 7 desafios.
• Validação com pyNMMS: O autor utilizou o reasoner automatizado pyNMMS para verificar as propriedades estruturais da base gerada:
  • Não-transitividade: Confirmado que a cadeia de entidades não é transitiva (ex: Entidade $\vdash$ Individação e Individação $\vdash$ Termos Expandidos, mas Entidade $\nvdash$ Termos Expandidos). Isso corresponde ao requisito de design de manter um "núcleo" separado das extensões.
  • Não-monotonicidade: Adicionar contexto (ex: detalhes de cadeias de proveniência) pode derrotar inferências simples. Isso modela a transição de "proveniência desleixada" (scruffy) para "proveniência adequada" (proper).
  • Independência: As resoluções de design para diferentes desafios (ex: fluxo de dados vs. fluxo de processos vs. responsabilidade) são inferencialmente independentes, sem vazamento de inferências entre visões.
  • Correspondência com Racional de Design: As propriedades estruturais da base gerada pelo diálogo correspondem exatamente a decisões de design documentadas em uma análise retrospectiva de 8.820 e-mails e 666 issues do grupo de trabalho original.

5. Significado e Impacto

• Reconceitualização da Engenharia de Conhecimento: O trabalho propõe mudar o paradigma de "extração de conteúdo" para "explicitação dialética". A base de conhecimento é o registro estruturado do que foi articulado e defendido, não uma cópia do que o especialista "sabe" internamente.
• Uso Seguro de LLMs: O Elenchus transforma o problema de alucinação dos LLMs em uma característica do protocolo. O LLM propõe hipóteses de incoerência, mas o especialista humano mantém a autoridade final. Erros do LLM são filtrados pela contestação, custando apenas um turno de diálogo, sem corromper a base final.
• Integração End-to-End: Demonstra um fluxo de trabalho completo que vai de uma conversa em linguagem natural até uma base formal verificável logicamente, com propriedades estruturais (não-transitividade, não-monotonicidade) que refletem nuances de domínio que lógicas clássicas ou abordagens puramente estatísticas frequentemente perdem.
• Rastreabilidade Total: Oferece uma solução para a "caixa preta" da engenharia de ontologias, onde cada regra pode ser rastreada até um momento específico de negociação dialética.

Em suma, o Elenchus demonstra que é possível construir bases de conhecimento formalmente rigorosas e semanticamente ricas através de um processo dialético assistido por IA, onde a estrutura lógica emerge da negociação de compromissos e incoerências, alinhando-se com a filosofia inferencialista e resolvendo problemas práticos de engenharia de ontologias.