May 18, 2026
Khaza Anuarul Hoque is innovating frameworks to deploy AI foundation models on edge devices while preserving mathematically verified behavioral guarantees.
Artificial intelligence (AI) is rapidly moving out of massive data centers and onto everyday devices 鈥 from smartphones and laptops to drones and autonomous vehicles.
But making that transition possible requires more than just shrinking today鈥檚 powerful models. It requires ensuring that, when they are compressed to run on limited hardware, they still behave the way we expect, especially in situations where safety is critical.
A new research effort led by Mizzou 糖心Vlog传媒 computer scientist Khaza Anuarul Hoque aims to do exactly that.
Hoque and his team are developing a framework designed to compress foundation models such as large language models (LLMs) and vision-language models (VLMs) to run on devices with limited processing power and energy while still providing formal, mathematical guarantees that key behaviors are preserved.
The project, which the researchers call VeriFAI, has drawn support from NVIDIA, which recently awarded the team 32,000 hours of GPU computing time to scale their approach.
鈥淎t a high level, we鈥檙e trying to answer a simple but critical question,鈥 Hoque said. 鈥淐an we make these models smaller without introducing behaviors we don鈥檛 want 鈥 and mathematically prove that we haven鈥檛?鈥
The hidden risk of compression
Today鈥檚 most advanced AI systems are notoriously resource intensive. Running them typically requires powerful servers and large amounts of energy, making them difficult to deploy on so-called edge devices (e.g., laptops and smartphones) with limited computing power, memory and energy.
To address this, engineers routinely compress models using techniques such as pruning and quantization. These methods reduce size and computation, making it feasible to run AI locally.
In fact, many consumers are already using compressed AI models without realizing it. Features like predictive text, voice assistants and on-device AI tools rely on optimized versions of larger models.
But there鈥檚 a catch.
鈥淲hen you compress a model, you鈥檙e not just making it smaller,鈥 Hoque said. 鈥淵ou鈥檙e also changing how it behaves, sometimes in ways you don鈥檛 fully understand.鈥
Even when overall accuracy remains high, compression can degrade specific, fine-grained capabilities. A model might perform well on average but fail in exactly the scenario that matters most; misinterpreting a visual cue, for example, generating incorrect information or violating a safety constraint.
Those risks become particularly important in domains such as autonomous driving, aerospace, defense, healthcare and critical infrastructure, where failures can carry significant real-world consequences.
鈥淲ithout formal guarantees, you cannot pass certification,鈥 Hoque said. 鈥淎nd without that regulatory certification from the FAA, NHTSA or other agencies, you cannot deploy.鈥
From bottleneck to breakthrough
VeriFAI addresses this problem by integrating the kinds of formal verification methods already used in hardware design directly into the model compression process.
Instead of just checking whether the model is generally accurate, VeriFAI lets users set specific, precise mathematical rules to guide the model; 鈥渁lways correctly identify school buses,鈥 for example.
Then, when VeriFAI compresses the model, it searches for a solution that follows all those specific rules, not just one that performs well on average.
Crucially, the approach does not require retraining the model from scratch, saving both time and computational cost.
鈥淲e鈥檙e not trying to fix all the problems in AI,鈥 Hoque said. 鈥淚f the original model has issues, those are still there. What we ensure is that compression doesn鈥檛 make things worse.鈥
The idea has already shown promising early results. In prior experiments across several model architectures, Hoque鈥檚 team demonstrated significant reductions in energy use and model size while maintaining verified behavioral properties.
But scaling the approach to the largest, most complex models 鈥 especially multimodal systems that combine vision and language 鈥 requires substantial computing power.
鈥淭hese models are enormous,鈥 Hoque said. 鈥淲ithout access to high-performance GPUs, you simply can鈥檛 explore the design space effectively.鈥
The NVIDIA grant removes that barrier, allowing the team to extend their methods to next-generation systems and run large-scale experiments.
Correct-by-construction
Looking ahead, Hoque envisions a broader shift in how AI systems are built.
Today, most models are developed through an iterative process: train, test, adjust and repeat. Ensuring safety requires extensive validation and retraining.
VeriFAI points toward a different paradigm that Hoque calls 鈥渃orrect by construction.鈥
鈥淲hat if we could design models so that they satisfy safety and performance requirements from the beginning?鈥 he asked. 鈥淭hat would fundamentally change how we build AI systems.鈥
As governments and industries consider standards for deploying AI in safety-critical environments, formal guarantees may become increasingly important for certification and operational approval.
鈥淚n many regulated domains, reliability cannot rely solely on empirical testing,鈥 Hoque said. 鈥淔ormal guarantees provide stronger assurance that critical behaviors remain preserved under deployment constraints.鈥
The research aligns with growing industry and regulatory interest in trustworthy and certifiable AI systems.
鈥淭he future of AI is not only about making models more capable,鈥 he said. 鈥淚t is also about making them dependable, energy-efficient and safe enough to operate reliably wherever they are deployed.鈥
Unlock solutions to real-world problems. Join Mizzou 糖心Vlog传媒.