An automated method for neural network quantization refinement
Carregando...
Data
Orientador(es)
Coorientador(es)
Lima Filho, Eddie Batista de
Membros da banca
Rosa, Thierson Couto
Becker, Leandro Buss
Barreto, Raimundo da Silva
Becker, Leandro Buss
Barreto, Raimundo da Silva
Pós-Graduação
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal do Amazonas
Tipo
Direito de acesso
DOI
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.
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.
Descrição
Palavras-chave
Redes neurais , Quantização , Verificação formal de equivalência , Equivalência funcional , Sistemas críticos para segurança , Ambientes com recursos limitados , Neural networks , Quantization , Formal equivalence verification , Functional equivalence , Safety critical systems , Resource-constrained environments
Termo controlado
Redes neurais (Computação); Computação natural; Computação quântica
Objetivos de Desenvolvimento Sustentável (ODS)
Citação
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.
Coleções
Avaliação
Revisão
Suplementado Por
Referenciado Por
Licença Creative Commons
Exceto quando indicado de outra forma, a licença deste item é descrita como Acesso Aberto