Avaliação de Código de Inteligência Artificial: teste de estresse de inferência e verificação formal para robustez

Abstract

This work investigates how to reduce the gap between satisfactory results in controlled settings and the trustworthy behavior of artificial intelligence (AI) systems in real-world contexts. To address this challenge, it proposes a three-layer methodological architecture. In the first layer, the Smart Inference Pipeline (SIP) structures empirical robustness testing through synthetic perturbations to data, labels, and hyperparameters. On this foundation, the Smart Inference Pipeline with Verification (SIP-V) adds formal certification to the experimental workflow using Satisfiability Modulo Theories (SMT) solvers, making analyses more auditable and reproducible. Finally, SIP-Q extends this architecture by introducing controlled quantization, enabling an integrated assessment of the trade-off between computational efficiency and predictive stability. Taken together, SIP, SIP-V, and SIP-Q establish a unified inference pipeline for reliability assessment, capable of supporting development decisions with greater transparency, traceability, and safety. The experimental results indicate that SIP consistently exposes latent fragilities, with measurable degradation across all evaluated configurations and average F1-score drops exceeding 50% in 13 of the 25 evaluated pairs, primarily due to perturbations in input data. In SIP-V, formal verification analyzed 274 queries, detected all invalid perturbations, and highlighted the contrast between CVC5, which was faster, and Z3, which was more suitable for in-depth audits. In SIP-Q, quantization preserved average performance in most configurations, enabling efficiency gains of up to 8×, although models sensitive to numerical thresholds exhibited degradation under low-precision settings.