Topic: AI Seminar: Stanley Bak
Time: Monday Nov 1, 2021 12:00 PM Eastern Time (US and Canada)

Join Zoom Meeting
https://stonybrook.zoom.us/j/91227496273?pwd=M3EyUDlzK3Vzd2pDOGpDU1ZjN0k1UT09

Abstract: The field of formal verification has traditionally looked at proving properties about finite state machines or software programs. The surge in deep learning has been accompanied by a surge of progress in trying to apply mathematical and algorithmic techniques to prove things about the function being computed by a neural network.

This talk formalizes the neural network verification problem and describes technical methods for neural network verification based on reachability analysis. Improvements to analysis efficiency will be given, as well as research directions for further exploration. We also include an objective comparison performed this last summer trying to evaluate the best existing verification methods in terms of speed and network size. The competition was performed on common hardware and involved the participation of twelve international teams (the tool authors) on a common set of benchmarks. 

Biography: Stanley Bak is an assistant professor in the Department of Computer Science at Stony Brook University investigating the verification of autonomy, cyber-physical systems, and neural networks. He strives to develop practical formal methods that are both scalable and useful, which demands developing new theory, programming efficient tools and building experimental systems.
Stanley Bak received a Bachelor's degree in Computer Science from Rensselaer Polytechnic Institute (RPI) in 2007 (summa cum laude), and a Master's degree in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2009. He completed his PhD from the Department of Computer Science at UIUC in 2013. He received the Founders Award of Excellence for his undergraduate research at RPI in 2004, the Debra and Ira Cohen Graduate Fellowship from UIUC twice, in 2008 and 2009, and was awarded the Science, Mathematics and Research for Transformation (SMART) Scholarship from 2009 to 2013. From 2013 to 2018, Stanley was a Research Computer Scientist at the US Air Force Research Lab (AFRL), both in the Information Directorate in Rome, NY, and in the Aerospace Systems Directorate in Dayton, OH. He helped run Safe Sky Analytics, a research consulting company investigating verification and autonomous systems, and performed teaching at Georgetown University before joining Stony Brook University as an assistant professor in Fall 2020.
Abstract: Molecular learning has become an emerging field of AI, driving breakthroughs in drug discovery, protein design, and materials design. For high-stakes scientific tasks, however, predictive accuracy alone is not sufficient: models must also be interpretable and trustworthy. Our work aims to study molecular learning under a unified explainability perspective across two major model families: Graph Neural Networks (GNNs) and Large Language Models (LLMs).

GNNs are natural choices for molecular graphs and achieve strong performance on many molecular tasks. To enhance explainability, many GNN explanation methods have been proposed and work well for 2D GNNs. However, 3D GNNs introduce two key challenges: producing chemically meaningful substructures and reducing fidelity loss caused by dense geometric graphs. To address these challenges, I present two methods. 3DGraphX decomposes dense 3D graphs into chemically meaningful 3D motifs, enabling compact explanations that align with chemical intuition. EDMA introduces an energy-based discrete mask approximation approach to reduce the discrepancy between the soft mask optimized during training and the hard mask used for explanation, improving explanation fidelity.

LLMs present different characteristics and challenges compared with GNNs. LLMs can provide a certain level of explanation through step-by-step reasoning, and their natural-language outputs are easy for humans to understand and interpret. However, because LLMs are trained for general-purpose tasks, their performance on scientific tasks often lags behind specialized GNNs. To improve performance, existing methods guide LLMs by providing suggestions through brief feedback, retrieval-augmented generation (RAG), or planner agents. However, these approaches face several limitations, such as vague guidance, introduced bias problems, and high computational cost. To fill the gap, I propose RL-Guider, a lightweight reinforcement-learning agent that converts evaluation feedback into input-specific guidance for molecular optimization. RL-Guider improves over time by accumulating historical experience and transfers efficiently across different LLMs while preserving interpretability.

Together, these efforts aim to provide explanations that are scientifically meaningful and faithful, while also preserving or improving performance on molecular tasks to better meet real scientific needs.

Speaker: Xufeng Liu

Location: New Computer Science-1-Room 115
Join us for the New York State Innovation Summit on October 28-29, 2024 in Syracuse, NY. This multi-day is event for NYS organizations that want to showcase and discover new and emerging technologies that support innovation and drive business growth. The event serves as an opportunity to foster collaboration; introduce industry to experts that can assist growth, strengthen our statewide innovation ecosystem and showcase promising early stage companies. Whether you're a startup, an economic developer, or an established manufacturer, the NYS Innovation Summit is for you. The 2024 New York State Innovation Summit will showcase companies and researchers at the forefront of emerging technologies and new advancements in production capabilities. This event celebrates New York State leadership in technology-led economic growth with experts in biotechnology, new materials, energy innovation, and artificial intelligence that will explore current technology convergence opportunities, ways to accelerate commercialization, and issues of manufacturing sustainability.
Postmortem Program Analysis from a Conventional Program Analysis Method to an AI-assisted Approach

Abstract: Despite the best efforts of developers, software inevitably contains flaws that may be leveraged as security vulnerabilities. Modern operating systems integrate various security mechanisms to prevent software faults from being exploited. To bypass these defenses and hijack program execution, an attacker needs to constantly mutate an exploit and make many attempts. While in their attempts, the exploit triggers a security vulnerability and makes the running process abnormally terminate.

After a program has crashed and abnormally terminated, it typically leaves behind a snapshot of its crashing state in the form of a core dump. While a core dump carries a large amount of information, which has long been used for software debugging, it barely serves as informative debugging aids in locating software faults, particularly memory corruption vulnerabilities. As such, previous research mainly seeks fully reproducible execution tracing to identify software vulnerabilities in crashes. However, such techniques are usually impractical for complex programs. Even for simple programs, the overhead of fully reproducible tracing may only be acceptable at the time of in-house testing.

In this talk, I will discuss how we tackle this issue by bridging program analysis with artificial intelligence (AI). More specifically, I will first talk about the history of postmortem program analysis, characterizing and disclosing their limitations. Second, I will introduce how we design a new reverse-execution approach for postmortem program analysis. Third, I will discuss how we integrate AI into our reverse-execution method to escalate its analysis efficiency and accuracy. Last but not least, as part of this talk, I will demonstrate the effectiveness of this AI-assisted postmortem program analysis framework by using massive amounts of real-world programs.

Bio: Dr. Xinyu Xing is an Assistant Professor at Pennsylvania State University. His research interests include exploring, designing and developing new program analysis and AI techniques to automate vulnerability discovery, failure reproduction, vulnerability diagnosis (and triage), exploit and security patch generation. His past research has been featured by many mainstream media and received the best paper awards from ACM CCS and ACSAC. Going beyond academic research, he also actively participates and hosts many world-class cybersecurity competitions (such as HITB and XCTF). As the founder of JD-OMEGA, his team has been selected for DEFCON/GeekPwn AI challenge grand final at Las Vegas. Currently, his research is mainly supported by NSF, ONR, NSA and industry partners.
The coach who led Team USA to four Math Olympiad gold medals shares his blueprint for staying irreplaceable in an AI-driven world.

As artificial intelligence transforms our world, what skills will remain uniquely human? How can we prepare for careers in an automated future?

Join Carnegie Mellon mathematics professor Po-Shen Loh for insights on navigating the AI revolution by embracing our humanity.

Dr. Loh brings a distinctive perspective shaped by his dual expertise: serving as national coach of the USA Mathematical Olympiad team (which has won four gold medals under his leadership) and developing innovative solutions for real-world challenges from pandemic response to educational technology.

Through his nationwide speaking tour that reached 250 audiences across 100 cities, he has refined a practical framework for thriving alongside AI.

In this presentation, Dr. Loh will explore how creative problem-solving, judgment, and communication become more valuable as automation grows -- and how students and professionals can build those strengths now.

The session includes real-world examples, guidance for education and careers, and a Q&A.

Speaker: Po-Shen Loh is a social entrepreneur and inventor, working across the spectrum of mathematics, education, and healthcare.

A math professor at Carnegie Mellon University, he also served a decade-long term as the national coach of the USA International Mathematical Olympiad (IMO) team, taking the team to gold on numerous occasions.

He has pioneered numerous innovations and has been featured in or co-created YouTube videos with more than 25 million views.

Location: Wang Center Theater

The series is offered by Stony Brook University's Institute for Creative Problem Solving in collaboration with the National Museum of Mathematics (MoMath) and Brookhaven National Laboratory.

The event is free but space is limited. Please register to reserve your space.

This virtual presentation series is designed to inform the Stony Brook University research community about the Research Funding Landscape of key topic areas. Our Strategic Research Initiatives team will provide insight into the rapidly shifting funding environment using policy briefs, budgetary priorities, and relevant legislation. We will highlight federal and state priorities in the current and upcoming years to help Stony Brook researchers develop strategies for pursuing funding in a rapidly shifting environment. This series is moderated by Mónica Bugallo, Interim Vice President for Research & Innovation.

Join us for the third in the series, focused on the artificial intelligence landscape:


Translating the Funding Landscape for Stony Brook Researchers: Artificial Intelligence
Presented by Catherine Chen, Ph.D., Research Development Associate
Faculty Respondent: Assistant Professor Nav Nidhi Rajput, Department of Materials Science and Chemical Engineering
Wednesday, April 22, 2026 at 2 pm to 3 pm

Registration is Required

Abstract: Current Chain-of-Thought (CoT) verification methods predict reasoning correctness based on outputs (black-box) or activations (gray-box), but offer limited insight into \textit{why} a computation fails. We introduce a white-box method: \textbf{Circuit-based Reasoning Verification (CRV)}. We hypothesize that attribution graphs of correct CoT steps, viewed as \textit{execution traces} of the model's latent reasoning circuits, possess distinct structural fingerprints from those of incorrect steps. By training a classifier on structural features of these graphs, we show that these traces contain a powerful signal of reasoning errors. Our white-box approach yields novel scientific insights unattainable by other methods. (1) We demonstrate that structural signatures of error are highly predictive, establishing the viability of verifying reasoning directly via its computational graph. (2) We find these signatures to be highly domain-specific, revealing that failures in different reasoning tasks manifest as distinct computational patterns. (3) We provide evidence that these signatures are not merely correlational; by using our analysis to guide targeted interventions on individual transcoder features, we successfully correct the model's faulty reasoning. Our work shows that, by scrutinizing a model's computational process, we can move from simple error detection to a deeper, causal understanding of LLM reasoning.

Speaker: Xianjun Yang

Location: Old Computer Science Building - CS2311