SpecGuard usa lógica temporal para detectar jailbreaks que só aparecem ao longo de várias mensagens
O SpecGuard propõe monitorar diálogos inteiros com LLMs, e não mensagens isoladas, convertendo observações em linguagem natural em fatos verificáveis e checando-os contra especificações formais de comportamento proibido escritas em lógica temporal linear. O framework não exige treinar um classificador e supera guard models de código aberto mantendo taxa controlada de falsos positivos, além de produzir um rastro de decisão auditável.
A maioria dos guard models atuais classifica cada mensagem ou par pergunta-resposta isoladamente, atribuindo um score de risco pontual. O problema é que muitos jailbreaks multi-turno são desenhados justamente para nunca ter uma única mensagem obviamente maliciosa — a intenção perigosa só emerge quando se olha a sequência completa de turnos, o que os autores descrevem como tratar segurança de diálogo como uma propriedade de traço em vez de uma propriedade pontual.
O SpecGuard primeiro usa um contrato fixo de proposições atômicas para traduzir cada observação em linguagem natural — o que o usuário pediu, o que o assistente respondeu — em fatos estruturados, com proveniência e evidência associadas. Padrões de interação proibidos são então escritos como fórmulas de Lógica Temporal Linear (LTL), do tipo "nunca X depois de Y, a menos que Z tenha ocorrido antes", e cada fórmula é compilada em um autômato finito simbólico que consome o traço do diálogo turno a turno, tanto em tempo real, bloqueando antes da resposta, quanto retrospectivamente, em auditoria pós-hoc.
Como o framework não aprende parâmetros a partir de dados rotulados, ele não sofre do mesmo tipo de overfitting a padrões de ataque vistos em treinamento que afeta guard models convencionais, e cada decisão vem acompanhada de um "witness" replicável — a especificação disparada, os fatos que a sustentam e os turnos relevantes — o que facilita auditoria e depuração de falsos positivos e negativos. A limitação natural é que a cobertura depende de quão bem o conjunto de especificações LTL antecipa os padrões de ataque possíveis; formas novas de manipulação multi-turno que não se encaixem em nenhuma especificação existente passam despercebidas até que alguém escreva uma regra específica para elas.