💻 computer science

Embedding Formal Worst-Case Latency Proofs and Memory-Safety Certificates into the snn-mlir MLIR Lowering Pipeline for IEC 62304-Compliant Edge Deployment of Spiking Neural Networks

Este artigo introduz uma passagem de análise de pós-processamento de MLIR para o compilador snn-mlir que gera provas de latência de pior caso e certificados de segurança de memória verificáveis por máquina, permitindo, assim, a implantação de redes neurais de impulsos (spiking neural networks) em conformidade com a norma IEC 62304 Classe B para dispositivos médicos de borda de missão crítica, como detectores de convulsões.

Autores originais: Hassan Farooq

Publicado 2026-07-07

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Hassan Farooq

Artigo original sob licença CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você construiu um cérebro robótico muito inteligente e eficiente em energia (chamado de Rede Neural de Espículas ou SNN) projetado para ouvir as ondas cerebrais de um paciente e detectar convulsões antes que elas aconteçam. Este cérebro robótico é perfeito para dispositivos médicos minúsculos, alimentados por bateria, porque é rápido e consome pouquíssima energia.

No entanto, há um grande problema: ninguém confia nele ainda.

No mundo dos dispositivos médicos, você não pode apenas dizer: "Ele funciona na maioria das vezes". Você precisa de uma prova absoluta de que ele nunca será lento demais ou travará, mesmo no pior cenário possível. Se o cérebro robótico demorar muito para reagir, o paciente poderá estar em perigo. Atualmente, as ferramentas usadas para construir esses cérebros robóticos são como uma padaria que assa bolos deliciosos, mas se recusa a fornecer um certificado provando que a temperatura do forno estava segura ou que o bolo não queimará sua língua.

Este artigo apresenta um novo "inspetor de segurança" que corrige essa lacuna. Veja como funciona, usando analogias simples:

1. O Elo Perdido: O "Inspetor de Segurança"

Os autores criaram uma ferramenta de software especial (uma "passagem de pós-processamento") que atua como um inspetor de segurança super rigoroso.

O Jeito Antigo: Você constrói o cérebro robótico, transforma-o em código (C11) e torce para que seja rápido o suficiente.
O Novo Jeito: Após o código ser construído, este inspetor examina a planta (o grafo de fluxo de controle), calcula o tempo absolutamente mais lento que o robô poderia levar para pensar e escreve um certificado diretamente no código.

2. O Cálculo do "Pior Caso" (A Analogia do Engarrafamento)

Para provar que o cérebro robótico é seguro, o inspetor usa um método chamado IPET. Pense no processo de pensamento do robô como um carro dirigindo por uma cidade com muitos cruzamentos (loops e decisões).

Normalmente, o carro dirige rápido.
Mas o inspetor pergunta: "Qual é o pior engarrafamento que poderia acontecer? E se todas as luzes estiver de vermelho e todas as estradas estiverem bloqueadas?"
O inspetor resolve um quebra-cabeça matemático complexo (um "Programa Linear Inteiro") para encontrar esse engarrafamento de pior caso.
O Resultado: Eles descobriram que, mesmo no pior engarrafamento, o cérebro robótico leva apenas 100,6 microssegundos para tomar uma decisão.
A Margem de Segurança: O dispositivo médico precisa reagir dentro de 50 milissegundos (50.000 microssegundos). O cérebro robótico é 497 vezes mais rápido do que o prazo limite. É como terminar uma corrida de 100 metros em 0,2 segundos quando a regra diz que você tem 100 segundos para terminar. Você está seguro.

3. O "Livro de Provas" (Stubs de Lean4)

O artigo também menciona o Lean4, que é como um tabelião digital.

O inspetor não apenas escreve uma nota dizendo "É rápido". Ele escreve uma promessa matemática formal (uma "obrigação de prova") em uma linguagem especial que os computadores podem verificar.
Pense nisso como "espaços reservados" em um contrato. O artigo diz: "Escrevemos o contrato que diz 'Este código é seguro'. Um advogado (um especialista humano) poderia dar o aval posteriormente".
Esta é a primeira vez que um contrato formal desse tipo foi anexado a este tipo de código de cérebro robótico.

4. O Padrão Médico (IEC 62304)

Dispositivos médicos devem seguir um livro de regras estrito chamado IEC 62304. É como um checklist para construir um avião seguro.

Os autores mostraram que seu novo processo cria uma "trilha de papel" que cobre a maior parte do checklist (cerca de 75% dos requisitos principais).
Eles provaram que podem rastrear o código de volta até o design original, o que é um grande passo em direção à aprovação oficial para uso médico.

5. O Teste de Direção (Detecção de Convulsões)

Para provar que isso funciona, eles testaram em dados reais de dois pacientes com epilepsia (do conjunto de dados CHB-MIT).

O Resultado: O cérebro robótico identificou corretamente as convulsões 78,8% das vezes.
A Velocidade: Ele rodou tão rápido que teve uma margem de segurança enorme. Embora tenham testado em um computador padrão (não no minúsculo chip médico ainda), a matemática provou que ele seria seguro no chip minúsculo também.

Resumo do Que Foi Alcançado

O Problema: Tínhamos uma IA médica inteligente, mas não havia forma de provar que ela era rápida o suficiente para situações de vida ou morte.
A Solução: Uma nova ferramenta que calcula automaticamente a velocidade do "pior caso" e anexa um certificado de segurança formal ao código.
O Resultado: Eles construíram com sucesso um cérebro robótico de detecção de convulsões, provaram matematicamente que é 497 vezes mais rápido que o limite de segurança e criaram a documentação necessária para iniciar o processo de tornar este um dispositivo médico certificado.

Nota Importante: O artigo admite que este é um "primeiro rascunho" do processo de segurança. Eles ainda não construíram o dispositivo médico final e ainda não assinaram totalmente os contratos legais finais (os "provas de Lean4" são atualmente apenas o esboço do contrato). Mas eles construíram o roteiro e as ferramentas para chegar lá, o que nunca foi feito antes para este tipo específico de tecnologia.

Resumo Técnico: Incorporação de Provas de Latência de Pior Caso e Certificados de Segurança de Memória no Pipeline de Redução de snn-mlir MLIR

1. Declaração do Problema

As Redes Neurais de Espigões Neuromórficas (SNNs) oferecem computação temporal eficiente em termos de energia, adequada para dispositivos médicos de borda, como neuroestimuladores de circuito fechado para epilepsia. No entanto, sua implantação em ambientes de missão crítica é atualmente bloqueada por um "gap de ferramenta". Embora frameworks existentes como o snnTorch e compiladores como o snn-mlir possam gerar código C11 válido a partir de modelos treinados, eles falham em produzir evidências verificáveis por máquina de que as funções de inferência compiladas satisfazem limites de Tempo de Execução de Pior Caso (WCET) ou os requisitos de documentação da certificação IEC 62304 Classe B.

Os compiladores de SNN atuais não integram métodos de verificação formal (como a Técnica de Enumeração de Caminhos Implícitos, ou IPET) para provar que o código atende aos estritos limites de latência exigidos para hardware implantável. Sem essas provas, as SNNs não podem ser certificadas para uso médico sob normas como a IEC 62304, que exige rastreabilidade dos requisitos até a implementação verificada.

2. Metodologia

Os autores propõem uma passagem de análise de pós-processamento que opera na Representação Intermediária de Múltiplos Níveis (MLIR) emitida pelo compilador snn-mlir. O pipeline consiste nas seguintes etapas:

Treinamento e Exportação do Modelo: Uma SNN de três camadas feedforward de Leaky Integrate-and-Fire (LIF) foi treinada usando snnTorch no conjunto de dados de EEG de escalpo CHB-MIT (pacientes chb01 e chb02) para detecção de convulsões. O modelo foi exportado para o formato de Representação Intermediária Neuromórfica (NIR).
Compilação: O grafo NIR foi reduzido para código C11 usando snn-mlir (commit 89b65e0). O código foi compilado com GCC no nível de otimização -O0 para garantir uma correspondência estável e não otimizada entre a estrutura da fonte e as instruções emitidas, o que é necessário para a extração precisa do grafo de fluxo de controle (CFG).
Análise de WCET Formal (IPET): Uma passagem de pós-processamento em Python (certify.py) extrai o CFG de cada camada LIF compilada. Ela formula um Programa Linear Inteiro (ILP) de Técnica de Enumeração de Caminhos Implícitos (IPET) parametrizado pelo tempo de instrução do microcontrolador ARM Cortex-M4F. O ILP maximiza o fluxo de ciclos sujeito a restrições de conservação de fluxo e limites de retrocesso de laço (loop-back).
Anotação e Certificação: A passagem anota o código C11 resultante com comentários @wcet_bound e gera estatutos de obrigações de prova em Lean4. Esses estatutos declaram formalmente os limites de WCET como obrigações de prova, vinculando a saída do compilador a um assistente de prova.
Mapeamento IEC 62304: Os artefatos gerados (documentação de CFG, código fonte anotado, logs de teste) são mapeados para cláusulas específicas da IEC 62304 Classe B (Processo de Desenvolvimento de Software) para demonstrar conformidade com os requisitos de documentação e rastreabilidade.

3. Principais Contribuições

O artigo reivindica quatro contribuições primárias:

Formulação de WCET para SNNs: Os autores formulam a análise de WCET para funções de inferência LIF compiladas por snn-mlir como um ILP de IPET parametrizado pelo tempo de instrução do ARM Cortex-M4F.
Passagem de Pós-Processamento Automatizada: Implementação de uma passagem em Python que automatiza a extração de CFG, resolução de ILP, anotação de WCET e geração de estatutos de Lean4 sem exigir modificações no código-fonte C++ do compilador subjacente.
Validação de Ponta a Ponta: Validação do pipeline em uma tarefa de detecção de convulsões clinicamente relevante, demonstrando que a inferência C11 compilada corresponde ao modelo de referência em Python enquanto adere a restrições de análise estática.
Pacote de Artefatos IEC 62304: Provisão de um pacote de artefatos mapeados cobrindo categorias de processo de desenvolvimento de software da IEC 62304 Classe B, representando um caminho da um modelo treinado para documentação regulatória compatível.

4. Resultados

Desempenho do Modelo: A SNN treinada alcançou uma acurácia balanceada de 78,8% (IC 95%: 74,5–83,2%) no conjunto de teste reservado, excedendo o limiar de credibilidade de 75%. A sensibilidade foi de 68,6% e a especificidade de 89,1%.
Corretude da Compilação: A função de inferência C11 compilada mostrou uma divergência negligível em relação à referência Python do snnTorch (divergência máxima $\approx 1 \times 10^{-5}$ ), atribuída a diferenças de precisão de ponto flutuante em vez de viés sistemático.
Limites de WCET:
- A análise IPET gerou um limite uniforme por camada de 5.634 ciclos.
- O limite da rede certificada para a rede de três camadas é de 16.902 ciclos (100,6 µs a 168 MHz).
- Este limite fornece uma margem de 497× abaixo do prazo de tempo real rígido de 50 ms para neuroestimulação.
- O tempo de execução medido foi de 8.627 ciclos (51,4 µs), bem dentro do limite certificado.
Cobertura de Artefatos: O pacote gerado cobre totalmente cinco das oito categorias de processo de desenvolvimento de software da IEC 62304 §5.x e parcialmente cobre duas outras, resultando em uma pontuação de 6,0/8,0 para o processo de desenvolvimento. Ele cobre totalmente o gerenciamento de configuração (§8.0), mas observa a falta de uma análise formal de gerenciamento de risco de software (§7.1).

5. Significância e Alegações

Os autores posicionam este trabalho como o primeiro caminho publicamente documentado de um modelo snnTorch treinado para um pacote de documentação IEC 62304 Classe B para uma função de inferência SNN.

Novidade: O trabalho preenche a lacuna entre as saídas de compiladores neuromórficos e padrões de verificação formal, aplicando especificamente IPET a SNNs e gerando obrigações de prova em Lean4.
Modéstia e Limitações: Os autores declaram explicitamente que os estatutos de Lean4 são especificações, não provas verificadas; a descarga dessas provas é deixada para colaboradores futuros. Os limites de WCET são derivados de builds não otimizadas (-O0) e aplicados como uma aproximação cross-arquitetura (host x86_64 com modelos de tempo ARM) em vez de através de compilação cruzada nativa para ARM. A análise de gerenciamento de risco (§7.1) não foi realizada, e o estudo é limitado a dois pacientes do conjunto de dados CHB-MIT.
Conclusão: O pipeline estabelece uma base reprodutível para trabalhos futuros visando a implantação de borda neuromórfica totalmente verificada, demonstrando que as SNNs podem ser compiladas em código C11 com limites de latência verificáveis por máquina, adequados para a certificação de dispositivos médicos de missão crítica.