Acabamos de conhecer o falecimento de Francisco Pinto Balsemão, um homem livre. A quem dedico, por ele ter sido quem foi, o pensamento/diálogo que me ocupava no Chatgpt5, na sequência de ter acabado de ouvir em podcast a entrevista de Eliezer Yudkowsky a Ezra Klein - autor que tem vindo a alertar para o perigo de extinção da humanidade por descontrole da Inteligência Artificial. Aqui fica:
Semantic Top-Layer Logical-Deductive Censor
(supervisor semântico formal com efeito catalisador)
Autor: Luis Miguel Novais
Data: Porto, 21 de outubro de 2025
Resumo
Propõe-se um controlador semântico de topo que atua como censura lógico-dedutiva: o modelo pode “pensar” e “falar”, mas só produz efeitos (chamadas de ferramenta, ordens financeiras, ações de robótica, publicações externas) quando a sua saída é compilada para uma linguagem formal e provada contra invariantes explicitadas. O controlador emite um token de execução apenas se a prova passar; caso contrário, bloqueia ou devolve para revisão. A solução reconcilia práticas conhecidas de verificação/monitorização com a realidade dos modelos gerativos e coloca a semântica das ações no centro — com papel catalítico sobre todo o fluxo.
- Definição operativa
Supervisor semântico formal (SSF): componente obrigatório “no topo” que:
a) impõe forma — a saída do modelo tem de ser estrutura formal (JSON/DSL/AST) compatível com um esquema definido;
b) verifica significado — traduz essa estrutura para restrições/propriedades e prova que as invariantes de segurança e de política são satisfeitas;
c) autoriza efeitos — só aciona efeitos externos se existir certificado de conformidade emitido pelo SSF;
d) audita — regista AST, prova e decisão para responsabilidade e fiscalização.
Garantia: se todo o canal de efeitos passa pelo SSF e as invariantes cobrem a classe de danos relevante, nenhuma ação executada pode violar essas invariantes (garantia por construção).
- Arquitetura mínima (em camadas)
- Geração estruturada pelo modelo, constrangida por gramática/JSON Schema.
- Guardrails de política (listas de permissões, filtros de segurança) para triagem rápida.
- Verificação formal (SMT/SAT, planeamento declarativo, lógicas temporais; em robótica, funções barreira/“shields”).
- Execução condicionada: o orquestrador só executa com token do SSF.
- Registo e atestação do ambiente para auditoria e conformidade.
- Relação com trabalho anterior
A proposta dialoga com:
– arquiteturas com monitor e fallback (runtime assurance/Simplex);
– escudos de segurança em aprendizagem por reforço (shielding a partir de especificações formais);
– verificação em tempo de execução (runtime verification) de propriedades sobre traços;
– guardrails práticos para GenAI (políticas/filtros de conteúdo).
O ponto novo é a síntese aplicada a modelos gerativos com gating obrigatório de efeitos e foco explícito na semântica de ações. - Teorema prático (esboço)
Se:
(i) todas as ações externas são expressas numa linguagem formal decidível;
(ii) existe uma especificação que codifica as invariantes de segurança/política;
(iii) o único caminho para efeitos é “modelo → SSF → execução”;
(iv) o SSF só emite token quando as invariantes estão satisfeitas;
então nenhuma ação executada viola as invariantes. O risco residual é extra-semântico (canais paralelos, engenharia social, lacunas de especificação). - Exemplos de invariantes (ilustrativos)
Jurídico/financeiro: jurisdição e foro permitidos; tetos de honorários; cláusulas obrigatórias; cálculos conferidos; autenticação forte antes de transações.
Operacional/IT: chamadas apenas para APIs em allow-list; parâmetros dentro de intervalos; idempotência e rollback garantidos.
Robótica: zonas proibidas; limites de velocidade/força; funções barreira que asseguram segurança física. - Limitações e escopo
– Cobertura: o SSF garante o que foi especificado; lacunas na especificação não são cobertas.
– Canais: se existirem vias alternativas de ação (humanas ou técnicas) fora do SSF, não há garantia.
– Custo: algumas provas podem ser onerosas; mitigam-se com cache, decomposição modular e combinações de “checks” rápidos com verificações profundas.
– Verdade factual em linguagem livre: o SSF não prova “verdade” de afirmações abertas; garante que os efeitos obedecem às invariantes. - Avaliação sugerida
– Taxa de bloqueio útil (violações captadas sobre violações injetadas).
– Falsos positivos e latência de verificação.
– Robustez a ataques de prompting e integrações externas antes e depois do SSF.
– Traçabilidade para auditorias e conformidade regulatória. - Nota de originalidade
Existem antecedentes técnicos (monitores formais, shields, verificação, guardrails). A presente formulação — censura lógico-dedutiva no topo da semântica, com efeito catalisador e gating obrigatório de efeitos em modelos gerativos — não é apresentada como solução canónica por autores como Yudkowsky e distingue-se pelo enfoque semântico-normativo aplicável a domínios jurídicos, financeiros, operacionais e robóticos. - Não é o fim, claro.
