Please join us on Friday for a CSE 600 talk by CS Faculty, Stanley Bak. During this semester, please periodically check the CSE 600 schedule for the latest talk updates.

Title:  Formal Verification Methods for Cyber-Physical Systems and Neural Networks

Time: Friday 4/1, 2:40 PM

Location:  NCS 120

Abstract: Formal verification methods in Computer Science strive to prove properties about all possible executions of a system, and are an alternative development approach to testing when correctness is paramount. Traditionally these have been applied to hardware circuits, state-machine protocols, or software source code. Prof. Stanley Bak will discuss his research on extending formal verification approaches to more complex areas including cyber-physical systems and neural networks.


Speaker Bio: 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 received a PhD from the University of Illinois at Urbana-Champaign (UIUC) in 2013, and worked for four years in the Verification and Validation (V&V) group in the Aerospace Systems Directorate at the Air Force Research Laboratory (AFRL). He received the AFOSR Young Investigator Research Program (YIP) award in 2020.
























A new virtual seminar series on Games, Decisions, and Networks will start this Friday. The series aims at bringing together researchers working on foundations and applications of games theory, decision theory, and networks from computer science, control, economics and operation research. 





The advisory board for the series comprises Asu Ozdaglar (MIT), Christos Papadimitriou (Columbia), Drew Fudenberg (MIT), Eva Tardos (Cornell), Matthew O. Jackson (Stanford), Ramesh Johari (Stanford), and Tamer Başar (UIUC). 
The first talk will be given by Costantinos Daskalakis (MIT) on January 22nd at noon ET, titled Equilibrium Computation and the Foundations of Deep Learning. Upcoming speakers include


- Rakesh Vohra (Upenn)
- Sanjeev Goyal (Cambridge)
- Aaron Roth (Upenn)
- Aislinn Bohren (Upenn)
- Jason Marden (UCSB)

and more to be added!

You are cordially invited to attend the biweekly Brookhaven AI Mixer (BAM). BAM includes one short talk on AI research happening at BNL, followed by an open mixer over coffee and snacks for everyone to network and discuss all things AI. The first half hour will consist of presentations that will be available via ZOOM, and the second half hour will be for in person only networking.

Join us every other Tuesday at noon in CDSD's Training Room (building 725, 2nd floor) to learn about interesting AI methods and applications, engage with potential collaborators, prepare for pending FASST funding calls, and build a community of AI for Science at BNL.

AI for Neutrino Oscillation Fits

Abstract: Neutrino oscillation experiments face the problem of performing likelihood fits in a very highdimensional space to extract the oscillation parameters from measured spectra. The current strategy for this is to fix all but a few parameters, reducing the dimensionality of the fit to a manageable number, but this risks missing correlations between the parameters, which can impact the systematics of the measurement. This is an area where artificial intelligence and machine learning could make great improvements. I will discuss the problem, explain how it is currently dealt with, and sketch one possible way of implementing AI to solve it, using a sampling method combining Smolyak's algorithm, for efficient sampling using sparse grids, with an adaptive grid refinement to increase sampling in regions that are more likely to contain the global minimum.

Speaker: Steven Linden is a physicist in the Instrumentation Department at BNL working on neutrino and dark matter experiments. He got his PhD from Yale in 2010 doing analysis on the MiniBooNE experiment and then worked on various dark matter detectors (MiniCLEAN, Pico, SENSEI) at SNOLAB in Canada for nearly ten years before moving to BNL.

Location: CDS, Bldg. 725, Training Room

Join ZoomGov Meeting: https://bnl.zoomgov.com/j/1614473319?pwd=e4QSSgFHqDzHx870ixJpwuG3yqBere.1

Meeting ID: 161 447 3319
Passcode: 733283











Abstract:
Quantifying similarity is a central notion in science and data analysis, pervading everything from phylogenetic trees to the foundation of clustering. Unfortunately, despite being examined and applied for decades, traditional similarity and distance metrics have fundamental drawbacks. The key problem is that all of them are only defined over pairs of objects, so they scale quadratically when one tries to compare N objects. The present explosion in the amount of data available to us requires new ways to process information, and while some current algorithms can handle millions of points, we need alternatives applicable to billions. This is what motivated us to develop a new framework that can compare any number of objects at the same time. With this, we achieve an unprecedented linear scaling when comparing multiple objects. Here we will discuss the main properties of this formalism, along with its applications in drug design and to the analysis of Molecular Dynamics (MD) simulations. Our indices have proven to be incredibly versatile when applied to chemical space exploration and visualization, allowing us to rigorously quantify the chemical diversity of very large molecular libraries. This has led to the creation of several algorithms to sample important regions in chemical space, including a more efficient way of identifying the prevalence of activity cliffs. Additionally, our indices provide a convenient route to sample complex MD trajectories, allowing to identify representative structures very efficiently. Moreover, we can also cluster biological ensembles in a more robust way than with standard algorithms, which has led to our group's work on MDANCE, a very flexible and efficient open-source clustering module. Drop by if you want to know how we clustered one billion molecules!


Speaker:
Assistant Professor, Department of Chemistry and Quantum Theory Project
University of Florida, Gainesville
Website: https://quintana.chem.ufl.edu/

Location:
Laufer Center Lecture Hall 101
Language shared online through social media or messaging reflects people's thoughts and emotions. Processing this data with Natural Language Processing (NLP) and machine learning can reveal mental health and psychological traits. For example, analyzing Facebook posts enables me to predict depression before it is clinically diagnosed and highlight particular symptoms. At the population level, billions of geo-tagged Tweets can be used to monitor health risk patterns, including depression and anxiety trends across communities. Beyond assessment, I'm using Large Language Models (LLMs) to improve mental health care, including training therapists and assisting with Cognitive Behavioral Therapy. These applications of NLP and Al may lead to earlier and more effective interventions and improved access for underserved populations. Speaker: Johannes Eichstaedt, Ph.D. Assistant Professor, Psychology & Human-Centered Al, Stanford University

Abstract: Recent progress in Large Language Models (LLMs) has transformed text and code generation, yet models still falter on scientific reasoning where correctness, constraints, and physical consequences are critical. This talk explores how formal LLM reasoning can advance symbolic scientific modeling. First, our PDE-Controller formalizes informal PDEs (Partial Differential Equations), synthesizes solver-ready code, and plans subgoals to tackle nonconvex control via interactions with external solvers. Second, our Lean Finder accelerates scientific formalization via a semantics-aware search engine for Lean/Mathlib that retrieves relevant theorems, outperforming GPT models and gaining significant traction in the AI-for-math community. Through these efforts, we aim to design a semantics-first LLM that autoformalizes informal scientific problems into machine-checked specifications and synthesizes solver-ready code. This closes the loop between formal analysis and LLM reasoning, ultimately surpassing human heuristics for scientific discovery.

Bio: Dr. Wuyang Chen is a tenure-track Assistant Professor in Computing Science at Simon Fraser University. He is also a visiting research scientist at Microsoft. Previously, he was a postdoctoral researcher in Statistics at the University of California, Berkeley, advised by Professor Michael Mahoney. He obtained his Ph.D. in Electrical and Computer Engineering from the University of Texas at Austin in 2023, advised by Professor Atlas Wang. Dr. Chen's research focuses on integrating AI methods with physical knowledge, scientific machine learning, and theoretical understanding of deep networks. Dr. Chen has published papers at CVPR, ECCV, ICLR, ICML, NeurIPS, and other top conferences. Dr. Chen's research has been recognized by the US NSF newsletter, two Doctoral Dissertation Awards from INNS and iSchools, AAAI New Faculty Highlights, and NVIDIA Academic Grant Award. Dr. Chen also hosted and co-organized many conference workshops at NeurIPS, ICLR, CVPR.

Location: NCS 120

You are cordially invited to attend the biweekly Brookhaven AI Mixer (BAM). BAM includes one short talk on AI research happening at BNL, followed by an open mixer over coffee and snacks for everyone to network and discuss all things AI. The first half hour will consist of presentations that will be available via ZOOM, and the second half hour will be for in person only networking.

Join us every other Tuesday at noon in CDSD's Training Room (building 725, 2nd floor) to learn about interesting AI methods and applications, engage with potential collaborators, prepare for pending FASST funding calls, and build a community of AI for Science at BNL.

HPCortex - a new, general-purpose machine learning library for HPC

Abstract: I will introduce HPCortex, a lightweight, C++, MPI-native machine-learning library for heterogeneous HPC systems. It implements many common architecture patterns including transformers, graph neural networks, and convolutional networks, and delivers performance portability across NVIDIA, AMD, and Intel GPUs while depending only on MPI and standard compiler/BLAS stacks. I will illustrate its capabilities via a surrogate model for the RHIC AGS Booster digital twin, a simple GNN for a coupled spring system, and a compact language model, then outline the roadmap.

Biography: Christopher is a research scientist and head of the Scientific Computing Applications Group in the Computational Science Department at Brookhaven National Laboratory. Previously he was an assistant staff scientist in the Physics Dept. at Columbia University, and held physics postdoctoral research positions at both Brookhaven and Columbia. He earned his Ph.D in Theoretical Physics from the University of Edinburgh, UK.
His scientific background is in lattice QCD and high performance computing, but since joining Brookhaven in 2020 his research interests have expanded to include machine learning, applied mathematics and performance analysis, with a particular emphasis on building tools to support scientific research on HPC systems.

Location: CDS, Bldg. 725, Training Room

Join ZoomGov Meeting: https://bnl.zoomgov.com/j/1604143373?pwd=hHT2yaIjahBIQ6tieURFqs8Pwex9gU.1

Meeting ID: 160 414 3373
Passcode: 277410

Abstract: Humans perceive the world around them by recognizing global patterns and structures such as object parts, branches, their spatial arrangement, and so on. Most deep learning models, however, take a fundamentally local approach. They process images pixel-by-pixel rather than focusing on structures as a whole. While these models indeed perform well on many tasks, the local (pixel-level) versus global (structure-level) disconnect makes them harder to interpret and control.

Topology, in a general sense, is a mathematical language for describing structure. It delineates how different parts of an image relate to one another, capturing both individual structures and their overall layout. Preserving topology enforces structural correctness and, by extension, semantic validity.

In this thesis, we investigate how topological constraints can be used to bridge the gap between local and global understanding. We use topology to inform the design of deep learning models that are explicitly structure-aware. Our thesis focuses on dense prediction tasks, which include image segmentation, uncertainty estimation, and generative modeling. First, we introduce a topological interaction module for semantic segmentation that encodes containment and exclusion constraints directly into the learning process. This preserves anatomical hierarchies and improves multi-class consistency. Next, since segmentation models can never be truly perfect, we address the need for reliable uncertainty estimation to identify error-prone regions. Unlike conventional pixel-wise uncertainty maps, which tend to be noisy and difficult to interpret, we propose reasoning at the level of structural units--branches and connections--which are more visually discernible and actionable. Finally, we leverage topology for generative modeling. We propose a topology-guided diffusion framework that can be controlled using structural attributes like object count and connectivity.

Together, these contributions establish a unified approach to topology-informed, structure-preserving dense prediction models. By integrating topological reasoning with deep networks, this thesis advances models that are not only accurate, but also structurally consistent, interpretable, and controllable. The results from this thesis have been published in ECCV, NeurIPS, and ICLR.

Speaker: Saumya Gupta

Location: New Computer Science (NCS) 120


Zoom: https://stonybrook.zoom.us/j/93643318604?pwd=kv8DagpbayzizivU29UCYItnlzlYRM.1&jst=2
AI Institute Seminar Title: A Geometric Understanding of Deep Learning Abstract: This work introduces an optimal transportation (OT) view of generative adversarial networks (GANs). Natural datasets have intrinsic patterns, which can be summarized as the manifold distribution principle: the distribution of a class of data is close to a low-dimensional manifold. GANs mainly accomplish two tasks: manifold learning and probability distribution transformation. The latter can be carried out using the classical OT method. From the OT perspective, the generator computes the OT map, while the discriminator computes the Wasserstein distance between the generated data distribution and the real data distribution; both can be reduced to a convex geometric optimization process. Furthermore, OT theory discovers the intrinsic collaborative--instead of competitive--relation between the generator and the discriminator, and the fundamental reason for mode collapse. We also propose a novel generative model, which uses an autoencoder (AE) for manifold learning and OT map for probability distribution transformation. This AE-OT model improves the theoretical rigor and transparency, as well as the computational stability and efficiency; in particular, it eliminates the mode collapse. The experimental results validate our hypothesis, and demonstrate the advantages of our proposed model.