Hyperscale Verification in Microsoft Azure talk by Nikolaj Bjorner

Abstract: Cloud providers are increasingly embracing network verification for managing complex datacenter network infrastructure. Microsoft's Azure cloud infrastructure integrates the SecGuru tool, which leverages the Z3 Satisfiability Modulo Theories solver, for checking network access
control lists. It also integrates a verifier that uses both custom verification algorithms and Z3 that checks correctness of forwarding tables in Azure data-centers. These tools assure that the network is configured to preserve desired intent over hundreds of thousands of network devices. We describe our experiences building and running SecGuru for network verification in Azure.

Finally we mention recent advances in Z3, including a distributed version of Z3 that scales with Azure's elastic cloud. It integrates recent advances in lookahead and distributed SAT solving for Z3's
engines for SMT. A different recent advance includes integration of DNNs to learn variable branching strategies for high-performance SAT solvers, including MiniSAT, Glucose and Z3's SAT solver.

Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014, and test of time award at ETAPS 2018. Together with Leonardo de Moura received the CADE 2019 Herbrand award for contributions to SMT and applications. Previously, he developed the DFSR, Distributed File System - Replication, and Remote Differential
Compression protocols, RDC, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup, and program synthesis and transformation systems at the Kestrel Institute. He received his Master's and PhD degrees in computer science from Stanford University.
AI for Conservation: AI and Humans Combating Extinction Together by Daniel I. Rubenstein of Princeton University

ABSTRACT: The state of our planet is not good. We have lost more than 60% of the world's wildlife. Stopping the decline remains a challenge, especially since acquiring appropriate knowledge is expensive, time consuming and risky. Visual observations following the fates of a few individuals was the currency of the realm. But GPS technology and now machine learning provide a non-invasive scalable alternative. Photographs, taken by field scientists, tourists, automated cameras and incidental photographers, are the most abundant source of data on wildlife today. Wildbook, a project of tech for conservation coordinated by a non-profit Wild Me, is an autonomous computational system that starts from massive collections of images and, by detecting various species of animals and identifying individuals, combined with sophisticated data management, turns them into high-resolution information databases, enabling scientific inquiry, conservation and citizen science.

BIO: Dan Rubenstein is the Class of 1877 Professor of Zoology. He is currently Director of Princeton's Environmental Studies Program and is former Chair of Princeton University's Department of Ecology and Evolutionary Biology and Director of Princeton's Program in African Studies. He is a behavioral ecologist who studies how environmental variation and individual differences shape social behavior, social structure, sex
roles and the dynamics of populations. He has special interests in all species of wild horses, zebras and asses, and has done field work on them throughout the world identifying rules governing decision-making, the emergence of complex behavioral patterns and how these understandings influence their management
and conservation. In Kenya he also works with pastoral communities to develop and assess impacts of various grazing strategies on rangeland quality, wildlife use and livelihoods. He has also developed a scout program for gathering data on Grevy's zebras and created curricular modules for local schools to raise awareness about the plight of this endangered species. He engages people as 'Citizen Scientists' and has recently extended his work to measuring the effects of environmental change, including issues pertaining to the global commons
and changes wrought by management and by global warming, on behavior.
18th Annual Engineering Ball Flowerfield, St. James, NY Thursday April, 2nd, 7:00 to 10:00 pm Pick up your tickets in 231 Engineering (Monday - Friday, 10:00 am to 4 pm) Presenting Partner: L3Harris
Predicting Subjective Attributes in Visual Data - Zijun Wei

ABSTRACT: Recent progress in deep neural networks has revolutionized many computer vision tasks such as image classification, detection and segmentation. However, in addition to excelling in tasks that predict well-defined objective information, human-centered artificial intelligence systems should also be able to model subjective attributes, as defined by human perceptual behavior, that goes beyond the pure physical content of visual data. Example subjective tasks are the prediction of spatial or temporal regions that are interesting to humans (e.g., attract attention or are visually pleasing) and the recognition of subjective attributes (e.g., visually elicited sentiments). Better models for these tasks will improve the human-computer interaction experience in various applications. This thesis investigates several approaches to address the challenges in predicting those subjective attributes in visual data over a diverse set of tasks. I first present a novel framework for real-time automatic photo composition. The framework consists of a cost-effective data collection workflow, an efficient model training pipeline and a lightweight module to account for personalized preferences. Then I develop a novel and general algorithm to detect interesting segments in sequential data, which can be naturally applied to video summarization tasks. Furthermore, I propose methods that learn to represent sentiments elicited by images, in an unsupervised manner, using linguistic features extracted from large scale Web data. To conclude this thesis, I introduce a human-vision-inspired image classification algorithm that also predicts spatial visual attention even though no attention data was used for training it.  
Making sense of Twitter @ Bloomberg presented by Daniel Preotiuc-Pietro

ABSTRACT: The Bloomberg Terminal has provided ways for investors and journalists to sift through and understand the immense volume of tweets and discover financially-relevant content ever since the SEC approved the use of Twitter for company disclosures back in 2013.

In the first part of the talk, I will showcase how tweets impact financial markets and how Bloomberg is using Natural Language Processing methods to identify financially relevant tweets that move the markets. Our processing pipeline feeds directly to clients, journalists in the newsroom and powers several news analytic products offered by the company including trending companies and consumer sentiment for publicly traded equities.

However, understanding user pragmatic intent in individual tweets would allow us to gain deeper insights and enable new applications. I will present several recent research studies focused on understanding intent including identifying complaints and the roles with which vulgarity is used in social media and how these can help improve applications such as sentiment analysis and hate speech detection.

BIO: Daniel Preotiuc-Pietro is a Senior Research Engineer and Team Lead at Bloomberg LP, where he works on analyzing and building models for real-world large scale social media and news mining and information extraction. His research interests are focused on understanding the social and temporal aspects of text, especially from social media, with applications in domains such as Social Psychology, Law, Political Science and Journalism. Several of his research studies were featured in popular press including the Washington Post, BBC, New Scientist, Scientific American or FiveThirtyEight. He is a co-organizer of the Natural Legal Language Processing workshop series. Prior to joining Bloomberg LP, Daniel was a postdoctoral researcher at the University of Pennsylvania with the interdisciplinary World Well Being Project and obtained his PhD in Natural Language Processing and Machine Learning at the University of Sheffield, UK.
Abstract: This dissertation addresses the methodological disconnect between Natural Language Processing (NLP) and human-centric analysis by shifting the unit of analysis from document to human behavior in two broad respects: (i) time-ordering: modeling documents as sequential person-indexed behavioral observations, and (ii) person-level semantics: evaluation and explainability of models by their latent structure of psychological constructs rather than just its predictive accuracy against narrow proxy measures. First, we consider the most basic implication of language as a person's behaviors when measuring their psychological constructs: relationship between language sample size and model's predictive performance. We empirically show that the state-of-the-art transformers are often over-parameterized for typical NLP dataset sizes and can be reduced in dimensionality without performance loss. Establishing the author as the unit of analysis naturally allows us to treat their behavior as a time-ordered sequence. Second, we introduce a longitudinal evaluation framework that establishes ecologically valid evaluation settings, namely, cross-sectional and prospective generalization, and separates error measurement of the model into within-person dynamics and between-person differences. We demonstrate that traditional NLP evaluations based on random document splits can yield reversed conclusions under ecologically valid generalization settings. To address this, we develop models that capture the trajectory of mental states (e.g., mood shifts) rather than static traits. Third, moving into person-level semantics, we evaluate the latent structure of large language models using a novel machine behavior analytic framework. We find that while GPT-4 achieves high predictive correlation with self-reports, its latent symptoms structure diverges from clinical understanding. Finally, we propose a method for modeling multidimensional behaviors, embedding concurrent behavioral signals alongside language to predict future states. Taken together, this work suggests that operationalizing language as behavior advances NLP methods into a rigorous instrument for valid psychological inquiry.

Speaker: Adithya Ganesan

Location: Join Zoom Meeting (ID: 99021939129, Passcode: 569493)
Abstract: Modern decision-making increasingly relies on complex data, imperfect models, and limited domain expertise--yet decisions must still be made with confidence and accountability. This talk presents a research perspective on visual analytics as a bridge between data, models, and human judgment. Through three case studies spanning public-health risk analysis, multivariate scientific visualization, and causal model auditing with large language models, I will show how interactive visualization can reveal structure in high-dimensional data, support reasoning under uncertainty, and help humans critically assess both statistical and AI-generated explanations. Together, these examples illustrate how visual analytics enables users not only to explore data, but to form, challenge, and refine beliefs that underpin scientific and societal decisions.

Bio: Klaus Mueller received his Ph.D. in Computer Science from The Ohio State University in 1998. He is a Professor in the Department of Computer Science at Stony Brook University and a Senior Scientist at the Computational Science Initiative at Brookhaven National Laboratory. He currently serves as the Acting Chair of the Department of Technology and Society at Stony Brook. From 2012 to 2015, he was the Founding Chair of the Computer Science Department at SUNY Korea, where he also served as Vice President for Academic Affairs and Finance for two years.
His research interests span visual analytics, explainable AI, machine learning and data science, human-centered responsible AI, fairness, belief modeling and personalized communication, virtual and augmented reality, and computational and medical imaging. Dr. Mueller received the U.S. National Science Foundation Early Career Award in 2001, the SUNY Chancellor's Award for Excellence in Scholarship and Creative Activity in 2011, and the Meritorious Service Certificate and Golden Core Award of the IEEE Computer Society in 2016. In 2018, he was inducted into the U.S. National Academy of Inventors.
To date, he has authored more than 300 peer-reviewed journal and conference papers, which have been cited over 15,000 times. He is a frequent speaker at international conferences, has organized or participated in 18 tutorials, chaired the IEEE Visualization Conference in 2009, served as elected Chair of the IEEE Technical Committee on Visualization and Computer Graphics (VGTC) from 2012-2015, and was Editor-in-Chief of IEEE Transactions on Visualization and Computer Graphics from 2019-2022. He is a Fellow of the IEEE.

Location: NCS 120
Face Editing with Machine Learning presented by Zhixin Shu

ABSTRACT: The face is the most informative feature of humans and has been a long-standing research topic in Computer Vision and Graphics. Images of faces are also ubiquitous in photography and social media, and people have devoted significant resources to capturing and editing face images. Face editing can be broadly viewed as the encoding, manipulation and the decoding of some representations for face images. The challenges are that we want to manipulate an image in a controllable way and generate results that are both desirable and as realistic as possible. This thesis explores different Machine Learning-based face-editing approaches. I discuss the role of machine learning for achieving desirable edits by learning both the physical aspects as well as the statistical manifold of human faces. In my work for eye-editing, I discuss the importance of understanding multiple physical elements of a face image, such as shape, illumination, pose, etc. In a deep-learning-based approach, I introduce image formation domain knowledge to the construction and training of a neural network. This network provides transparent access to the disentangled representations of the aforementioned physical properties. With this network, we can achieve various face editing tasks in forms of representation manipulation. After that, I introduce Deforming Autoencoders, a network that learns to disentangle shape and appearance in an unsupervised manner. This disentanglement is beneficial for the learning of some other factors of variations, such as illumination and facial expression. In an extension of Deforming Autoencoders, we incorporate non-rigid structure-from-motion to learn a 3D morphable model for faces that only requires an image set for training. At last, I describe an image-to-image network for 3D face reconstruction, which also utilizes structure-from-motion in deep learning. With real face images in training, this network not only reconstructs 3D faces more accurately than prior art but also has better generalization ability in real-life testing cases.
Talk by Zhenhua Liu to be followed by AI Institute updates


Abstract: Decision making with uncertainty has been studied in multiple communities extensively. Recently, online optimization has gained popularity partially because of its promising performance guarantees by incorporating predictions. In this talk, I will provide an overview of our work on algorithm designs for online optimization and its applications. Then, I will talk about our recent work in ACM Sigmetrics 2019 on choosing predictions and control algorithms simultaneously and dynamically. Finally, I will discuss some ongoing efforts and collaboration opportunities.

Bio: Zhenhua Liu is currently an assistant professor in the Department of Applied Mathematics and Statistics at Stony Brook University. He is also affiliated with the Department of Computer Science, the AI Institute and the Smart Energy Technology Cluster. He received his PhD degree in Computer Science from California Institute of Technology. His current research interests include cloud computing, online optimization and learning, smart grid, market design and distributed control. His research combines rigorous analysis and system design, and goes from theory, to prototype, and eventually to industry to make real impacts.
Abstract: Language offers a uniquely powerful lens for understanding the mind: one that can access latent psychological realities often missed by traditional measurement tools. However, as language models expand their ability to capture semantics through context length, expansion into deeper levels of semantics is less explored, especially with respect to understanding cognitive patterns of authors. This dissertation proposes that we can uncover deeper cognitive and affective patterns that reflect more accurate underlying mental states by analyzing language at higher levels of discourse semantics and by modeling latent states.


First, the dissertation focuses on uncovering cognitive styles or thinking patterns manifesting in language. We demonstrate that modeling language at deeper semantic levels such as discourse relations, can unveil latent psychological states and traits, including cognitive styles that influence both mental health and behavior. Introducing a novel blend of transfer and active learning, we efficiently curated a new set of linguistic data on cognitive styles like dissonance. This approach allows for more precise measurement when dealing with rare-classes and low-resource tasks. As a second contribution, effective validation methods are introduced to language-based assessments of the underlying cognitive styles. Controlled behavioral experiments and online studies show that cognitive styles detected through linguistic signals reliably predict real-world behaviors such as decision-making and engagement with extremist communities, both at the individual and community levels, sometimes months in advance

The research further moves beyond traditional measurement tools like questionnaires and expert judgments, which rely on Classical Test Theory, by establishing that language-based assessments more closely approximate true psychological states. The mechanisms by which these assessments outperform standard tools are explained, highlighting their predictive power for behaviors linked to underlying traits. Finally, a more sophisticated approach is explored by modeling psychological outcomes with Item Response Theory (IRT), an improvement over Classical Test Theory. Adaptive language-based assessments are introduced, showing that targeted, adaptive testing based on latent IRT scores can efficiently and accurately capture multiple psychological dimensions.

Taken together, these contributions argue for a shift towards language-based psychological assessments. By integrating deeper discourse-level semantics with measurement theory, this dissertation charts a path towards truer scores of mental states: ones that are more precise, and reflective of the complexity of human cognition and emotions.

Speaker: Vasudha Varadarajan

https://stonybrook.zoom.us/j/99180374682?pwd=w2zZTkQsfunrBZhHgEweR54NjKabZ2.1&jst=2