DSA Thrust seminar “Efficient, Trusted, and Practical Automated Reasoning”  

Automated reasoning lies at the intersection of AI and formal methods, serving as a foundation for verifying hardware, accelerating software development, and securing large-scale cloud systems. Over decades, real-world applications have transformed automated reasoning into a core technology, yet scalability and reliability remain fundamental challenges due to computational complexity and subtle correctness flaws.

In this talk, I present research aimed at advancing efficient and trusted automated reasoning from both theoretical and practical perspectives, while extending its impact to emerging domains. First, I introduce a randomized approximate counting algorithm that balances estimation error and solves 23% of instances that were previously out of reach for the state of the art. Second, I present the first formally certified approximate counter that ensures provably reliable model counts via a static proof in Isabelle/HOL and dynamic per-run validation, establishing a new approach to verifying randomized algorithms. Finally, I show how automated reasoning benefits emerging domains: in machine learning, we developed an efficient certified verifier for binarized neural networks that achieves a 218× speedup over existing methods, enabling the first practical certified neural network verification.