CISE Faculty Seminar: Dr. Sumit Jha

Details

Zoom Link: https://ufl.zoom.us/j/94143185671

Biography: Dr. Sumit Kumar Jha is Eminent Scholar Chair Professor of Computer Science at Florida International University. He earned his Ph.D. in Computer Science from Carnegie Mellon University and has held multiple summer faculty appointments with the Air Force Research Laboratory Information Directorate.

Dr. Jha currently serves as the lead PI on projects in excess of $11 million. Dr. Jha has led interdisciplinary, multi-institutional teams on projects funded by the National Science Foundation (NSF), Defense Advanced Research Projects Agency (DARPA), Department of Energy (DOE), and other federal agencies. His work has been published at premier venues, such as AAAI, DAC, DATE, ICCAD, ICLR, IJCAI, and NeurIPS. His research focuses on building high-assurance and efficient AI at both algorithmic and hardware levels. He has developed methods to make AI systems more transparent and resistant to threats by combining symbolic decision procedures, human expertise, foundation models, and deductive reasoning. Dr. Jha has also pioneered flow-based in-memory computing techniques for data-intensive applications, advancing a new paradigm for efficient and sustainable AI in his research funded by the NSF over the past 11 years.

Dr. Jha has been a PI on projects from DARPA GARD, DARPA ANSR, DARPA TIAMAT, NSF Software and Hardware Foundations (SHF), NSF Exploiting Parallelism and Scalability (XPS), NSF Scalable Parallelism in the Extreme (SPX), and NSF Formal Methods in the Field (FMitF), NGA Boosting Innovative GEOINT, NNSA/ORNL, ONR Science of AI, Department of Energy, AFRL, and the Royal Bank of Canada Innovation Lab. His work has earned multiple best paper awards and nominations at various forums (IEEE DATE, ACM/IEEE ICCAD, IEEE MILCOM, IEEE ICCABS), as well as the prestigious Air Force Office of Scientific Research Young Investigator Program (AFOSR YIP) Award. Dr. Jha aims to advance high-assurance and efficient AI systems that drive innovation across science, engineering, healthcare, and sustainable peace.

Title of the Talk: Formal Methods for High-assurance and Efficient AI

Abstract: Deployment of Artificial Intelligence (AI) in high-assurance settings demands formal guarantees, which remain challenging for the current generation of AI models, particularly deep neural networks. The limited scalability of the traditional formal verification methods has been further exacerbated by modern foundation models, such as large language models (LLMs). In this talk, we present scalable approaches to  (1) explain the decisions of AI agents in a human-interpretable manner drawing upon neural stochastic differential equations and path integrals, (2) communicate our ethics, domain knowledge, and feedback to AI agents informally and formally leveraging probabilistic temporal logics as formal specifications, and (3) enable human-in-the-loop auditing of the behavior of teams of LLM agents against regulatory and ethical guidelines through model checking, theorem proving and provably correct symbolic AI methods. Additionally, I will briefly discuss recent progress using Binary decision diagrams and other formal methods towards in-memory computing, demonstrating how algorithm-hardware co-design can reduce the soaring energy demands of foundation models. These innovations offer a blueprint for creating the next generation of AI that seamlessly fuses human expertise, ethical guidelines, domain rules, and data-driven intelligence while maintaining interpretability and efficiency.