Search and Metavariable Coupling

by Leni Aniva, 05 Nov 2024

Search is the underlying theme of many difficult computational tasks. Search algorithms have achieved incredible success in the fields of board games, planning, and SMT. Can we extend the same idea to proving mathematical theorems? We’ll use an example to motivate. Read More

Towards Efficient Verification of Quantized Neural Networks

by Pei Huang, 15 May 2024

Deep neural networks (DNNs) have demonstrated striking and steadily improving capabilities across a wide range of tasks. Ongoing improvements to neural networks are typically achieved through a significant expansion in their scale. This escalation, however, frequently leads to substantial increases in computational cost, memory bandwidth requirements, and energy consumption, which make DNNs difficult to deploy on embedded systems with limited hardware resources. A promising approach for mitigating this difficulty is neural network quantization. Read More

Reconstructing cvc5 proofs in Isabelle/HOL- Part I: Communication between Isabelle and cvc5

by Hanna Lachnitt, 15 Mar 2024

If you have used the cvc5 SMT solver before you know that it can solve many complicated problems fast, especially for the theories it supports! But can other programs profit from cvc5’s efficiency too? And if so, how can cvc5 effectively communicate with these external tools? Could we use their feedback to increase our trust in cvc5’s result even more? Read More

Adding a New Theory to cvc5

by Alex Ozdemir, 26 Jan 2024

cvc5 is an SMT solver with support for many theories: integers, reals, bit-vectors, algebraic datatypes, separation logic, sets, bags, and more. This means that is can find satisfying solutions for formulas involving these kinds of objects. In this post, I explain the process of adding a new theory to cvc5: the theory of prime-order finite fields. Read More

VeriX: Towards Verified Explainability of Deep Neural Networks

by Min Wu, 15 Jan 2024

Broad deployment of artificial intelligence (AI) systems in safety-critical domains, such as autonomous driving and healthcare, necessitates the development of approaches for trustworthy AI. One key ingredient for trustworthiness is explainability: the ability for an AI system to communicate the reasons for its behavior in terms that humans can understand. Read More

Partitioning Strategies for Distributed SMT Solving

by Amalee Wilson, 15 Dec 2023

Partitioning is a divide-and-conquer approach where a difficult problem is split into hopefully easier subproblems that can be solved in parallel. This strategy is notoriously difficult to get right with SMT problems. We found that while it’s no panacea, partitioning can be used to diversify solving and reliably improve performance in a portfolio. Read More