Resumo Técnico: IA Neuro-Simbólica para o Direito Penal Coreano

1. Declaração do Problema

O sistema de justiça criminal coreano depende fortemente de processos sumários (guyaksik) para agilizar um alto volume de infrações menores, particularmente delitos de trânsito, como condução sob influência de álcool (DUI) simples, direção sem habilitação e acidentes de trânsito leves. Embora este mecanismo melhore o rendimento judicial, ele impõe uma carga administrativa significativa aos promotores, que devem processar manualmente documentos jurídicos não estruturados (ex: registros de bafômetro, relatórios policiais, registros de interrogatório) em resultados estatutários determinísticos.

Avanços recentes em Grandes Modelos de Linguagem (LLMs) demonstraram capacidades robustas na extração semântica de textos jurídicos densos. No entanto, a implantação de LLMs puros para a Predição de Julgamento Jurídico (LJP) apresenta limitações fundamentais:

• Natureza Probabilística: Os LLMs geram texto com base em probabilidade, o que é inadequado para o raciocínio estritamente aritmético e baseado em regras exigido para o cálculo de multas estatutárias.
• Risco de Alucinação: Em contextos jurídicos, onde a responsabilidade exige determinismo completo, os LLMs frequentemente produzem "alucinações" ao serem confrontados com restrições matemáticas complexas ou limiares estatutários específicos.
• Falta de Verificação Formal: Arquiteturas puramente neurais não podem provar matematicamente a validade de um resultado de sentença, tornando-as insuficientes para aplicação judicial direta, onde erros estocásticos são intoleráveis.

2. Metodologia

Os autores propõem uma estrutura Neuro-Simbólica que faz a ponte entre fatos jurídicos não estruturados e a verificação formal. A arquitetura particiona estritamente as tarefas entre a compreensão semântica neural e o raciocínio lógico simbólico, organizada em um pipeline de cinco módulos:

Módulo 1: Ingestão de Dados Brutos

O sistema ingere documentos probatórios heterogêneos e com layouts complexos (declarações circunstanciais de DUI, resultados de bafômetro, registros de interrogatório e relatórios de acidentes). Ele emprega um protocolo de ingestão consciente de layout híbrido, utilizando OCR baseado em regras customizadas e segmentação de texto por codificador bidirecional para isolar seções narrativas de índices tabulares e metadados, convertendo-os em fluxos de texto limpos.

Módulo 2: Extração por LLM

Um LLM atua como um parser semântico para extrair elementos centrais do caso (tipos de crime, variáveis contínuas como a Concentração de Álcool no Sangue [BAC], e variáveis categóricas discretas).

• Restrição: O LLM é estruturalmente restringido para mapear cada fator extraído diretamente à sua fonte textual exata ("Texto de Referência") para reforçar o silogismo jurídico e o embasamento.
• Saída: As entidades extraídas são populadas em um esquema JSON intermediário, que serve como a ponte entre a extração probabilística e a lógica determinística.

Módulo 3: Verificação Human-in-the-Loop (HITL)

Para garantir a conformidade legal e o devido processo, uma fase de verificação obrigatória é introduzida antes de qualquer cálculo.

• Interface: Uma UI de tela dividida exibe a saída JSON estruturada ao lado do documento original com o texto de referência destacado.
• Mecanismo: Todas as variáveis extraídas assumem por padrão is_valid_by_human = false. Um profissional do direito deve verificar explicitamente cada fator para alterná-lo para true.
• Proveniência de Dados: Apenas os parâmetros explicitamente validados por um humano são encaminhados ao solver, garantindo que o sistema atue como uma ferramenta de suporte à decisão, e não como um decisor autônomo.

Módulo 4: Tradução Lógica e Solver Z3 SMT

Este é o núcleo da ponte neuro-simbólica. Os campos JSON validados são mapeados para variáveis de estado formais (flags Booleanas e restrições Inteiras) dentro do solver de Teoria de Satisfatibilidade Modulo Teorias (SMT) Z3.

• Modelagem de Axiomas: As Diretrizes de Sentença de 2026 para Infrações de Trânsito são formalizadas como axiomas matemáticos. Por exemplo, os limiares de BAC são modelados como restrições condicionais (ex: $0.08 \le BAC < 0.20 \implies Crime\_Category = 3$).
• Derivação de Zona: O solver avalia arrays Booleanos de fatores atenuantes e agravantes, somando-os para determinar a zona de sentença (Básica, Atenuada ou Agravada).
• Lógica de Prisão Obrigatória: O solver verifica restrições lógicas compostas (ex: se condenações anteriores $\ge 3$ ou se os fatores agravantes forem dominantes) para sobrepor os cálculos de multa com recomendações de prisão obrigatória.
• Verificação de Satisfatibilidade: Antes de emitir um resultado, o Z3 realiza um check de SAT para garantir que não existam contradições lógicas (ex: um caso não pode ser simultaneamente "Atenuado" e "Agravado"). Se um estado UNSAT for detectado, o pipeline retorna à interface HITL para resolução de conflitos.

Módulo 5: Visualização e Geração de Documentos

As saídas determinísticas do solver Z3 são traduzidas em artefatos acionáveis:

• Visualização da Árvore de Sentença: O sistema renderiza o caminho de decisão lógica (da categorização de BAC até a multa final) em uma árvore visual, fornecendo uma trilha de auditoria interpretável.
• Redação de Documentos: Usando prompts rigidamente estruturados, um LLM gera documentos legalmente conformes (Relatórios de Investigação Policial, Pareceres de Encaminhamento e Pedidos de Denúncia Sumária). Crucialmente, os valores das multas são injetados literalmente da saída do solver Z3, impedindo que o LLM recalcule ou alucine números.

3. Principais Contribuições

O artigo delineia três contribuições primárias:

1. Design de Pipeline Neuro-Simbólico: Uma estrutura que transforma registros policiais e de acusação não estruturados em resultados jurídicos determinísticos, isolando especificamente o LLM para extração semântica para mitigar riscos de alucinação durante o cálculo de multas.
2. Verificação Human-in-the-Loop (HITL): Um esquema transparente que ancora as variáveis jurídicas extraídas aos textos de referência de origem, garantindo supervisão humana e interpretabilidade, mantendo a autoridade jurídica final com o promotor.
3. Estrutura de Lógica Jurídica Formal: A construção de uma estrutura lógica usando o solver SMT Z3 para computar faixas de sentença precisas alinhadas com as Diretrizes de Sentença de 2026, substituindo a geração probabilística por prova matemática.

4. Resultados e Alegações

O artigo não apresenta métricas de desempenho empírico (ex: porcentagens de precisão em um conjunto de teste), pois o estudo foca na formulação teórica e no mapeamento lógico da arquitetura. Em vez disso, os autores alegam o seguinte com base no design:

• Determinismo: Ao delegar os cálculos estatutários para um provador de teoremas, o sistema garante que os resultados das sentenças estejam livres dos erros estocásticos inerentes aos LLMs.
• Robustez: O mecanismo de check de SAT garante que as contradições lógicas sejam detectadas e resolvidas antes que um veredito seja gerado, evitando resultados jurídicos inválidos.
• Responsabilidade: A integração HITL garante que o sistema permaneça uma ferramenta de assistência verificável, abordando as preocupações de transparência inerentes aos modelos de IA de "caixa preta".

5. Significância

Os autores posicionam este trabalho como uma evolução necessária na Predição de Julgamento Jurídico para ambientes de alto risco. Ao reconhecer que os LLMs são insuficientes para aritmética e adesão estrita a regras, o artigo propõe uma abordagem híbrida que aproveita as forças semânticas das redes neurais enquanto confia na lógica simbólica para as restrições "rígidas" da lei.

A significância reside no seu potencial para aliviar o gargalo administrativo dos casos de acusação menores na Coreia sem comprometer a integridade judicial. A estrutura oferece um caminho para automatizar a redação de denúncias sumárias (yaksik-gongsojang) garantindo que cada resultado matemático esteja fundamentado em fatos formalmente verificados e validados por humanos. Os autores observam que, embora o foco atual seja em infrações de trânsito, a arquitetura é projetada para ser escalável para outros crimes menores (ex: agressão simples, difamação, furto menor) que terminam em processos sumários.