pibic/esbmc · fork maktheus/esbmc · verificação formal de controlador neural
UFAM · PIBIC/PROPESP · diretório pibic/
Um controlador neural quantizado, verificado sob hipóteses explícitas.
O ESBMC foi usado para provar, refutar ou declarar inconclusivo — nunca "seguro por omissão" — o comportamento de um controlador DDPG para o CartPole, comparando sua versão Float32 com a representação de ponto fixo Q8.8 que de fato roda no harness C.
10.000estados comparados
0,0778 Nerro médio F32 vs Q8.8
3,5 sprova Z3 do limite de força
Float32 — pêndulo contínuo
Q8.8 — pêndulo quantizado
⚠ pior estado medido: +6,43 N → −1,33 N
cena 3D ilustrativa · ângulos não são a série medida
01
O que este estudo se propôs a responder
Objetivo geral: avaliar como a quantização Q8.8, a estrutura do controlador DDPG e a verificação limitada de propriedades do CartPole influenciam a produção de evidências formais e reprodutíveis — e até onde esse fluxo pode ser reaproveitado em componentes de IA Generativa.
PQ1
Fidelidade
A representação Q8.8 preserva o comportamento Float32 no domínio operacional?
PQ2
Estrutura neural
Há neurônios mortos ou permanentemente saturados nos 48 neurônios ocultos?
PQ3
Segurança
Quais propriedades da malha fechada o ESBMC prova ou refuta, com qual contraexemplo?
PQ4
Limites
Que hipóteses, custo computacional e timeouts restringem a conclusão formal?
PQ5
Generalização
Quais etapas do fluxo valem para componentes de IA Generativa, só com execução verificável?
02
Desenho experimental — do checkpoint ao veredicto
Quatro etapas sequenciais, preservadas em evidencias/final_2026/ com manifesto de hashes SHA-256: identificar o artefato, comparar Float32 contra Q8.8, formalizar propriedades no ESBMC e reproduzir de forma independente os estados publicados como contraexemplo.
1
Artefatos
checkpoint, pesos exportados, histórico de treino
2
Preparo numérico
Float32 vs. Q8.8, 10.000 estados, seed 42
3
Grafo do controlador
4–24–24–1, ReLU + tanh aproximada
4
Harnesses C
domínio Q8.8, propriedades A, B, C, D
5
ESBMC + Z3
execução simbólica e BMC
6
Evidências
veredictos, contraexemplos, logs, hashes
7
Síntese
confirmado · refutado · inconclusivo
03
Float32 contra Q8.8 — 10.000 estados, uma inversão de sinal
Rodada canônica com numpy.random.RandomState(42). A média do erro é pequena; a cauda não — o pior estado observado inverte o sentido da força entre as duas representações.
10.000estados amostrados
0,0778 Nerro médio absoluto
0,2262 Npercentil 95
7,7589 Nerro máximo (77,6% da faixa ±10 N)
Ilustração gerada a partir das estatísticas publicadas (média, p95, p99, máximo) — não é a série bruta dos 10.000 estados. O ponto do pior estado medido está no valor real documentado: Float32 = +6,4308 N, Q8.8 = −1,3281 N.
4,5749%erro máx. da tanh aproximada (z=−281)Alegação anterior era <3% — não se sustenta.
Q8.8, escala 256representação verificadaHarness C e runtime web usam a mesma aritmética.
04
O que o ESBMC prova, refuta ou deixa em aberto
Três resultados de natureza distinta — e a distinção é o próprio achado metodológico do projeto.
SUCCESSFUL
Limite de força (Property C)
−2560 ≤ FQ ≤ 2560 (|F| ≤ 10 N) provado sobre todo o domínio simbólico Q8.8 declarado.
Z3 v4.8.9 · 3,5 s · Boolector → UNKNOWN (não compilado no binário Windows)
SUCCESSFULestado fixo
Segurança em 1 passo (Property B)
Estado histórico (−0,7539, −3,9219, −0,1836, −1,5234) reproduzido: θ₁ ultrapassa o limite inteiro −53 no modelo angular linearizado.
0,313 s · confirma reprodução, não prova insegurança universal
SUCCESSFULTIMEOUT
Correção direcional (Property A-direita)
Estado fixo reproduzido (z<0, contrariando z>0 esperado) em 0,609 s. Versão universal: Z3 atinge timeout em 12 s — inconclusivo, não "seguro".
A-esquerda histórica não tem estado completo — não é evidência reproduzível
05
Auditoria estrutural — 48 neurônios, sem bounds artificiais
Grafo completo recalculado: a camada 2 parte do vetor simbólico real da camada 1, sem independência indevida entre camadas. Barras somam 24 neurônios por camada; cinza = TIMEOUT, inconclusivo.
Ativação — camada 1
24/24
Ativação — camada 2
17/24 +7
Não saturação — camada 1
24/24
Não saturação — camada 2
22/24 +2
FAILED Saída z ≥ 0 — contraexemplo em (−2,−305,−27,−1184) Q8.8. Propriedade universal refutada.
TIMEOUT · 4 s Saída z ≤ 0 — tempo esgotado. Combinado com o resultado acima, a saída conjunta fica inconclusiva.
Conclusão: não há base para afirmar, sobre os 48 neurônios, que algum é universalmente morto ou saturado — a maioria tem contraexemplo, mas 9 casos seguem inconclusivos.
06
IC3/PDR — a tentativa de prova ilimitada, e onde ela trava
BMC prova "seguro até K passos"; o custo explode com K. IC3/PDR busca um invariante indutivo sem construir uma fórmula monolítica com K cópias da transição — mas frames e cláusulas ainda podem crescer. Pipeline em pibic/ic3/: pesos Q8.8 → Verilog (gen_transition_system.py) → validação diferencial amostral → AIGER via yosys → PDR/BMC via ABC, preservando stdout bruto, tempo e pico de RSS.
0,37 sPDR + batente — invariante provado ∀t
909 sparede BMC sintético, K=4 (383 MB)
901,4 sator real · ABC BMC, 5 frames, sem veredito
1802,4 sator real · ABC PDR, não convergiu
Aviso de escopo — dois controladores diferentes
O gráfico abaixo mistura dois modelos: um sintético (24 neurônios, 1 camada, seed 7, soma-depois-divide), usado só para caracterizar a parede do BMC em geral, e o ator real do projeto (2 camadas de 24, 745 parâmetros, divisão por termo com truncamento). São controladores diferentes — a cor do rótulo indica qual é qual.
Escala logarítmica, de 0,3 s a 1802 s (~4 ordens de magnitude). Verde = modelo sintético · âmbar = ator real (745 parâmetros) · a barra com borda clara é a única prova universal desta raia.
PROVADO ∀t
ABC PDR, modelo sintético + batente
Com um limite artificial (batente) adicionado ao modelo sintético, o PDR encontra um invariante indutivo em 0,37 s — contra 500 s sem convergir sem o batente.
Invariante: 4 cláusulas, 8 literais, 3 dos 65 bits de estado — th[13] ⟺ th[14] ⟺ th[15], convergiu em F[2]
5 frames, sem veredito
ABC BMC, ator real DDPG (745 parâmetros)
745 parâmetros, forward coincidente em 12/12 amostras com a referência Python. Síntese yosys: 904.242 portas AND, 65 latches, nível 689.
bmc3 -F 60 -T 900 · 901,4 s · pico 503 MB
não convergiu
ABC PDR, ator real DDPG (745 parâmetros)
Mesma síntese do ator real. TIMEOUT é indeciso, nunca "seguro" — nenhuma das duas execuções decide |θ| ≤ 53 Q8.8 (12°) a partir de |estado| ≤ 5.
pdr -v -T 1800 · 1802,4 s · pico 708 MB
A semelhança entre esta parede e a parede do BMC do ESBMC (K=4, 909 s) é hipótese sugestiva, não causalidade demonstrada — modelos, propriedades, representações e solvers diferem.
Lacuna de evidência, registrada em vez de apagada
O stdout bruto da execução histórica do PDR sobre o ator real nunca existiu: a execução ocorreu antes de run_pdr.sh passar a preservar a saída do ABC, e um filtro por palavras-chave descartou o resto. Restaram apenas tempo e pico de memória. Corrigido no commit ad995812 — a saída bruta agora é sempre salva.
O que fica como limite documentado
E03
Curva K=8/K=16 é pesquisa futura — no modelo real o BMC não passa de 5 frames em 901 s; medir K maiores só faz sentido no sintético.
E04
PDR evita a fórmula monolítica com K transições, mas frames e cláusulas ainda podem crescer; AIGER bit-blasta os 4 inteiros de estado em bits soltos, perdendo estrutura de palavra.
E07
Rota mais promissora: exportar BTOR2 (yosys write_btor, já disponível) e usar um motor word-level (AVR, Pono ou btormc) — nenhum instalado nesta máquina.
"Não é 'use IC3 e o problema acaba': é a parede do BMC medida no sistema real, a prova de que IC3/PDR pode ser ordens de magnitude mais rápido quando o invariante é pequeno — e a mesma barreira reaparecendo no ator real para os dois métodos."
07
A auditoria que motivou tudo isso
O problema não era código ruim — era evidência quebrada. A auditoria de 2026-08-17 encontrou um artigo que afirmava resultados que os arquivos do repositório não sustentavam, e em alguns casos contradiziam. Cinco agentes de auditoria read-only trabalharam em paralelo, um por área, com posse exclusiva de arquivos — três retornaram; dois se perderam sem notificação, e aquelas áreas foram marcadas como "não auditado", nunca como "ok".
Até os próprios auditores erraram: afirmaram que não existia pasta .github/ no repositório. Existem 13 workflows ali, um deles nunca executado. A disciplina corretiva foi simples de enunciar e trabalhosa de aplicar — cada afirmação carrega a procedência da sua evidência: verificada por execução direta, ou apenas relatada sem confirmação.
A armadilha do timeout
O artigo alegava que o PID mantém T < 150°C por 10 passos. Uma primeira medição com limite de 200 s deu timeout — quase descartada como "sem evidência". Reexecutada com folga: SUCCESSFUL em 217 s, dezessete segundos além do primeiro limite. A afirmação era verdadeira. Ler timeout como "seguro" inventa uma prova; lê-lo como "sem evidência" pode destruir uma prova legítima — tratar ausência de sinal como sinal é o mesmo erro nos dois sentidos.
Estado do backlog (KANBAN.md)
Tarefas totais52
Concluídas36
P0 fechados (diagnóstico + correção)11
P0 ainda abertos0
P1/P2 restantes16
Afirmações verificadas vs. não confirmadas46 / 6
Suíte de testes, antes21 falhas em 0,12 s
Suíte de testes, depois44 testes coletados
Branches de correção do relatório (claude/*)
2026-06-19analyze-pibic-codelimpeza de 505 arquivos legados
2026-08-25pibic-ufam-relatorio-finalrelatório + PDF reprodutível
2026-08-30pibit-final-report-localizemais recente · não mesclada
08
Conclusão: verificabilidade parcial, não certificação
01
Fidelidade quantitativa. Erro médio 0,0778 N, p95 0,2262 N, p99 1,0927 N, máximo 7,7589 N em 10.000 estados; o pior estado inverte o sinal da ação.
02
Estrutura ainda condicional. O dado legado "24 vivos, 0 mortos, 0 saturados" é indicação histórica, não prova — continha bounds artificiais corrigidos nesta rodada.
03
Prova formal delimitada. |F| ≤ 10 N é SUCCESSFUL com Z3 em 3,5 s — prova do harness e domínio codificados, não do Float32 nem da dinâmica não linear completa.
04
Reprodução sem refutação universal nova. Estados fixos publicados foram confirmados; a refutação universal histórica carece de um novo log preservado.
05
Direcional inconclusivo. TIMEOUT em 12 s com Z3, UNKNOWN com Boolector indisponível — nenhum dos dois é prova nem refutação.
06
Contribuição tecnológica. Fluxo rastreável peso → Q8.8 → harness C → propriedade ESBMC → veredicto → contraexemplo reproduzido no simulador.
"Há evidência reprodutível de limites e falhas concretas, mas não há prova de segurança global do controlador." — a frase que resume por que este relatório troca certeza por rastreabilidade.