An automated method for neural network quantization refinement
| Primeiro coorientador dc.contributor.advisor-co1 | Lima Filho, Eddie Batista de | |
| Currículo Lattes do primeiro coorientador dc.contributor.advisor-co1Lattes | http://lattes.cnpq.br/7827981023232761 | eng |
| Primeiro orientador dc.contributor.advisor1 | Cordeiro, Lucas Carvalho | |
| Currículo Lattes do primeiro orientador dc.contributor.advisor1Lattes | http://lattes.cnpq.br/5005832876603012 | eng |
| Primeiro membro da banca dc.contributor.referee1 | Rosa, Thierson Couto | |
| Segundo membro da banca dc.contributor.referee2 | Becker, Leandro Buss | |
| Terceiro membro da banca dc.contributor.referee3 | Barreto, Raimundo da Silva | |
| Autor dc.creator | Matos Júnior, João Batista Pereira | |
| Currículo Lattes do autor dc.creator.Lattes | http://lattes.cnpq.br/6143153274833914 | eng |
| ORCID do autor dc.creator.orcid | https://orcid.org/0000-0001-8380-6058 | eng |
| Data de defesa/publicação dc.date.issued | 2025-02-18 | |
| Resumo / Abstract dc.description.abstract | No campo em rápida evolução da inteligência artificial, redes neurais profundas (DNNs) tornaram-se essenciais em diversas aplicações, desde veículos autônomos até sistemas de saúde. No entanto, o aumento no tamanho e na complexidade dessas redes apresenta desafios significativos para sua implementação em ambientes com restrições de recursos e críticos para segurança, devido às altas demandas computacionais e de memória. Esta dissertação aborda o problema crítico da quantização de redes neurais, cujo objetivo é reduzir a precisão dos parâmetros das redes para aumentar a eficiência sem comprometer seu comportamento funcional. A principal contribuição é o desenvolvimento do arcabouço Quantização Guiada por Contraexemplos para Redes Neurais (CEG4N), que integra a Verificação Formal de Equivalência (FEV)—uma técnica que rigorosamente verifica se dois modelos apresentam comportamento idêntico—ao processo de quantização. Metodologicamente, o CEG4N emprega um ciclo iterativo de otimização que utiliza ferramentas de verificação formal para detectar e corrigir sistematicamente discrepâncias entre os modelos original e quantizado, garantindo assim sua equivalência funcional (FE). Avaliações experimentais realizadas em benchmarks como Iris, Seeds, MNIST e CIFAR-10 demonstram que o CEG4N mantém efetivamente a precisão e integridade comportamental dos modelos, superando métodos tradicionais de quantização como quantização por seguimento de caminho guloso (GPFQ), especialmente em redes menores e esparsas. Embora a escalabilidade para modelos maiores permaneça um desafio devido ao alto custo computacional associado aos métodos de verificação formal, o arcabouço proposto avança significativamente na robustez e confiabilidade das redes neurais quantizadas. Além disso, esta pesquisa ressalta a importância da integração da verificação formal com a quantização para equilibrar de maneira ótima eficiência e precisão. Em última análise, estas contribuições facilitam a implementação de redes neurais em ambientes com rigorosas restrições de recursos e confiabilidade, promovendo sistemas de inteligência artificial mais seguros e eficientes. | por |
| Resumo (português) dc.description.resumo | In the rapidly evolving field of artificial intelligence, deep neural networks (DNNs) have become integral to numerous applications, from autonomous vehicles to healthcare systems. However, the increasing size and complexity of DNNs pose significant challenges for deployment in resource-constrained and safety-critical environments due to high computational and memory demands. This dissertation addresses the critical problem of neural network quantization, which aims to reduce the precision of network parameters to enhance efficiency while preserving functional behavior. The primary contribution is the development of the Counterexample-Guided Quantization for Neural Networks (CEG4N) framework, which integrates formal equivalence verification (FEV)—a technique that rigorously verifies that two models exhibit identical behavior—into the quantization process. Methodologically, CEG4N employs an iterative optimization loop that leverages formal verification tools to systematically detect and correct discrepancies between the original and quantized models, thus ensuring their functional equivalence (FE). Experimental evaluations conducted on benchmark datasets, including Iris, Seeds, MNIST, and CIFAR-10, demonstrate that CEG4N effectively maintains model accuracy and behavioral integrity, outperforming traditional quantization methods such as the greedy path following quantization (GPFQ), particularly in smaller and sparse networks. While scalability to larger models remains challenging due to increased computational overhead associated with formal verification methods, the proposed framework significantly advances the robustness and reliability of quantized neural networks. Moreover, this research underscores the importance of integrating formal verification into quantization to optimally balance efficiency and accuracy. Ultimately, these contributions facilitate the deployment of neural networks in environments with stringent resource and reliability constraints, promoting safer and more efficient artificial intelligence systems. | eng |
| Agência de fomento / Financiador dc.description.sponsorship | FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas | eng |
| Agência de fomento / Financiador dc.description.sponsorship | CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior | eng |
| Formato dc.format | application/pdf | * |
| Referência (citação) dc.identifier.citation | MATOS JÚNIOR, João Batista Pereira. An automated method for neural network quantization refinement. 2025. 130 f. Tese (Doutorado em Informática) - Universidade Federal do Amazonas, Manaus, 2025. | eng |
| Endereço permanente (URI) dc.identifier.uri | https://tede.ufam.edu.br/handle/tede/10912 | |
| Idioma dc.language | eng | eng |
| Instituição / Editora dc.publisher | Universidade Federal do Amazonas | eng |
| País dc.publisher.country | Brasil | eng |
| Faculdade, Instituto ou Departamento dc.publisher.department | Instituto de Computação | eng |
| Sigla da instituição dc.publisher.initials | UFAM | eng |
| Programa de Pós-Graduação dc.publisher.program | Programa de Pós-graduação em Informática | eng |
| Tipo de acesso dc.rights | Acesso Aberto | |
| Licença (endereço) dc.rights.uri | https://creativecommons.org/licenses/by-nc-nd/4.0/ | |
| Palavras-chave dc.subject | Redes neurais | por |
| Palavras-chave dc.subject | Quantização | por |
| Palavras-chave dc.subject | Verificação formal de equivalência | por |
| Palavras-chave dc.subject | Equivalência funcional | por |
| Palavras-chave dc.subject | Sistemas críticos para segurança | por |
| Palavras-chave dc.subject | Ambientes com recursos limitados | por |
| Palavras-chave dc.subject | Neural networks | eng |
| Palavras-chave dc.subject | Quantization | eng |
| Palavras-chave dc.subject | Formal equivalence verification | eng |
| Palavras-chave dc.subject | Functional equivalence | eng |
| Palavras-chave dc.subject | Safety critical systems | eng |
| Palavras-chave dc.subject | Resource-constrained environments | eng |
| Área de conhecimento (CNPq) dc.subject.cnpq | CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO: METODOLOGIA E TECNICAS DA COMPUTACAO: ENGENHARIA DE SOFTWARE | eng |
| Área de conhecimento (CNPq) dc.subject.cnpq | CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO: METODOLOGIA E TECNICAS DA COMPUTACAO: SISTEMAS DE INFORMACAO | eng |
| Termo controlado dc.subject.other | Redes neurais (Computação) | por |
| Termo controlado dc.subject.other | Computação natural | por |
| Termo controlado dc.subject.other | Computação quântica | por |
| Miniatura (endereço) dc.thumbnail.url | https://tede.ufam.edu.br/retrieve/84482/TESE_Jo%c3%a3oMatosJ%c3%banior_PPGI.pdf.jpg | * |
| Título dc.title | An automated method for neural network quantization refinement | eng |
| Título alternativo dc.title.alternative | Um método automatizado para refinamento de quantização de redes neurais | por |
| Tipo de documento dc.type | Tese | eng |