- talks - lists.cs.princeton.edu

Nikhil Pimpalkhare will present his FPO "Predictable Inter-Procedural Program Analysis via Almost-Commuting Transition Systems" on Thursday, 6/4/2026 at 1pm in the Common Area of 194 Nassau Street.
by Gradinfo 28 May '26

28 May '26

Nikhil Pimpalkhare will present his FPO " Predictable Inter-Procedural Program Analysis via Almost-Commuting Transition Systems" on Thursday, 6/4/2026 at 1pm in the Common Area of 194 Nassau Street. The members of his committee are as follows: Readers: Professors Zachary Kincaid (adviser), Thomas Reps Examiners: Aarti Gupta, and Mae Milano, Zachary Kincaid All are welcome to attend. Abstract follows below. Program analysis aims to automatically compute properties of programs from their source code. Since the problems that arise are frequently undecidable, the field has largely focused on developing sound analyses that over-approximate the true properties of a program. Modern program analyzers leverage complex heuristics to make these over-approximations as tight as possible, but these heuristics cause brittle performance: minor updates to codebases can cause large unintended swings in analysis precision. To help tool users anticipate analysis outcomes, a recent line of work has focused on developing analyses that are robust, and in particular \textit{monotone}: if a program is a refinement of another, its analysis should be at least as precise. Monotonicity is a meta-property of the analysis technique; it gives tool users a way to reason about how certain code changes, like refactoring a loop or deleting a variable, will affect their analysis results, without requiring knowledge of the tool's internal mechanisms. However, development on monotone program analysis had been largely confined to the intra-procedural setting (to analyzing procedures without procedure calls). This thesis develops a framework for designing monotone inter-procedural program analysis. The key idea is to connect context-free reachability results for abstract machines to program analysis via abstract interpretation: we compute the best abstraction of a program within a given model---its reflection---then exactly characterize the input-output behavior of that abstraction. We instantiate this recipe with vector addition systems with resets (VASR), a numerical computational model, establishing techniques to compute the VASR reflection of a program and the context-free reachability relation of VASR. We extend these results to Lossy VASR, a more expressive variant, producing a program analysis tool which is competitive with the state-of-the-art in verification capabilities while providing formal robustness guarantees. We further investigate Semi-Linear VASR, showing that their reachability relation can be computed in polynomial time despite exponential abstraction size. Finally, we unify the reachability results across all three classes under almost-commuting transition systems, (ACTS), algebraically characterizing properties that make these context-free reachability problems tractable. ACTS define a rich frontier of abstraction domains for monotone inter-procedural program analysis.

1 0

Gon Buzaglo will present his General Exam "Online Control using Spectral Filtering" on Tuesday, June 2, 2026 at 11:00 AM in CS 402.
by CS Grad Department 26 May '26

26 May '26

Gon Buzaglo will present his General Exam "Online Control using Spectral Filtering" on Thursday, May 28, 2026 at 11:30 AM in CS 402. Committee Members: Elad Hazan (advisor), Mark Braverman, Clarence Rowley, Bartolomeo Stellato Abstract: We introduce a new algorithmic framework for controlling linear dynamical systems in adversarial environments. Our method achieves efficient online control with regret guarantees while improving the running-time dependence on the stability margin from polynomial to polylogarithmic. The approach is based on a novel convex relaxation that approximates linear control policies using a universal basis derived from the eigenstructure of a Hankel matrix, a technique which may be of independent interest. This yields a computationally efficient algorithm that matches the performance of prior online control methods while exponentially accelerating their runtime dependence on the stability margin. To demonstrate the generality of our approximation framework, we derive results for partial observation of the state and bandit feedback of the costs. Reading List: https://drive.google.com/file/d/1y6Bk6Bd0rduVU1kwgGVvk_0DdTxo857E/view?usp=… Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

2 1

Jonah Langlieb will present his General Exam "Use GPU-based First Order Methods to speed up Benders Decomposed Capacity Expansion Optimization Models" on Thursday, May 28, 2026 at 10:00 AM in CS 302.
by CS Grad Department 25 May '26

25 May '26

Jonah Langlieb will present his General Exam "Use GPU-based First Order Methods to speed up Benders Decomposed Capacity Expansion Optimization Models" on Thursday, May 28, 2026 at 10:00 AM in CS 302. Committee Members: Jesse Jenkins (advisor), Felix Heide, Jonathan Mayer, Bartolomeo Stellato Abstract: Use GPU-based First Order Methods to speed up Capacity Expansion Optimization Models Electricity grid expansion is rapidly emerging as one of the most critical infrastructure bottlenecks in the United States, driven by rapid data center growth, increasing cross-sector electrification, and world-wide climate goals. To guide an estimated $479 billion in annual global electricity infrastructure investments [1], system planners, policymakers, and researchers use capacity expansion models (CEMs) to evaluate future grid pathways. These models are formulated as large-scale mixed-integer linear programs (MILPs) and are central to balancing complex trade-offs across grid reliability, cost, and emissions. However, despite advances such as parallel CPU-based Benders decomposition, current approaches still encounter computational limits that restrict the scope of policy analysis, particularly when co-optimizing generation and transmission at realistic spatial and temporal scales. This work explores how recent advances in GPU computing and GPU-native first-order methods, particularly cuPDLPx [2], can be leveraged to address these challenges. We show that Benders-decomposed CEMs exhibit structural properties such as repeated linear subproblems, shared sparsity patterns, and limited communication, that are well suited to GPU acceleration. We develop and evaluate approaches that apply GPU-accelerated first-order methods to subproblems, the master problem, and the monolithic relaxation, leveraging warm starts and parallelism. By integrating domain knowledge of energy systems, algorithmic structure, and low-level systems engineering, this work provides a scalable foundation for, and opens new avenues toward, generation/transmission co-optimization and higher resolution planning models. Reading List: https://docs.google.com/document/d/1jCdk9Cdbaa0qwe-vyOhXJGr-GbhN3NJDry2eS5d… Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0

Seminar with Caroline Trippel *19, Stanford University | Friday, May 29th @ 12:15pm | J-323
by Emily C. Lawrence 22 May '26

22 May '26

Speaker: Caroline Trippel *19, Stanford University Day: Friday, May 29, 2026 Time: 12:15pm Location: J323 Engineering Quadrangle Hosts: Sharad Malik and Aarti Gupta Title: Specification and Formal Verification of Hardware-Software Contracts for High-Assurance Computer Architectures Abstract: The complexity of modern computer systems gives rise to two critical computer architecture challenges: traditional instruction set architectures lack the detail needed to capture how hardware may undermine software assurance—correctness, security, reliability; and verification is a major and growing hardware design bottleneck, with critical bugs escaping to silicon in >85% of hardware projects despite verification consuming >50% of design effort, per a 2024 Siemens EDA study. To address these challenges, our work develops hardware-software (HW-SW) contracts to support software assurance and automated approaches and tools to rigorously verify hardware implementations against them. This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs. I will present three different tools built on this unified approach for side-channel security, memory consistency, and cache coherence verification of processor implementations. I will also briefly highlight our contracts work, which prompted Intel to update their Software Security Guidance and is informing industrial discussions on retrofitting the Arm ISA to better support performant constant-time code in the Spectre era of microarchitectural side-channel attacks. Bio: Caroline Trippel is an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University, where she leads the High Assurance Computer Architectures Lab. A central theme of her work is leveraging formal methods, especially automated reasoning, techniques to design and verify hardware systems. Trippel's research has been recognized with IEEE Top Picks and Best Paper Award distinctions, a Sloan Research Fellowship, an NSF CAREER Award, the inaugural Google ML and Systems Junior Faculty Award, the Intel Rising Star Faculty Award, an Intel Outstanding Researcher Award, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering.

1 0

Abhishek Panigrahi will present his FPO "Understanding Optimization, Distillation, And Transfer: A Theoretical Study of Deep Learning" on Thursday, May 28, 2026 at 2:00 PM in CS 302.
by CS Grad Department 21 May '26

21 May '26

Abhishek Panigrahi will present his FPO "Understanding Optimization, Distillation, And Transfer: A Theoretical Study of Deep Learning" on Thursday, May 28, 2026 at 2:00 PM in CS 302. The members of Abhishek’s committee are as follows: Examiners: Sanjeev Arora (Adviser), Elad Hazan, Karthik Narasimhan Readers: Danqi Chen, Surbhi Goel (UPENN) A copy of his thesis is available upon request. Please email gradinfo(a)cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend his talk. Abstract follows below: Modern deep learning systems are trained through increasingly complex pipelines involving large-scale data, multiple stages of training, and a growing number of design choices. While such systems have achieved remarkable empirical success, our theoretical understanding of how these choices shape the capabilities of the final model remains limited. This thesis develops theoretical studies on three fundamental questions underlying modern training pipelines: how optimization choices affect learning dynamics, how capabilities can be effectively transferred across models, and how learned capabilities generalize across tasks and modalities. First, the thesis analyzes the role of the learning rate in driving the Edge of Stability phenomenon, where training dynamics differ from the predictions of classical optimization theory. It also introduces and studies Context-Enhanced learning, a learning framework in which access to privileged contextual information during training can substantially accelerate training, even when that information is difficult to recover from the model’s outputs after training. Second, the thesis investigates how existing trained models can be used to more effectively train new models through knowledge distillation. Stronger teachers do not necessarily produce stronger students; rather, the quality of transfer depends critically on both the choice of teacher and the form of supervision. The results establish design principles for distillation from two complementary perspectives: selecting teachers by analyzing the student’s own gradients, and adapting supervision by identifying the student’s missing skills. Together, these principles enable efficient and reliable teacher selection using only 1% of the training compute, and yield improvements of at least 7% in settings where standard fine-tuning and reinforcement learning methods struggle to improve the student model. Finally, the thesis studies the transferability of learned capabilities beyond training. It develops methods for localizing the skills required for a task within a model and shows that such localized skills can improve generalization to out-of-distribution tasks. At the same time, it demonstrates that standard training pipelines are often insufficient for transferring capabilities to new modalities, and studies the importance of data composition in enabling reliable cross-modal transfer. Together, these results contribute to a more principled understanding of modern deep learning pipelines, with the broader goal of moving from empirical trial-and-error toward a science of training design.

1 0

Liv d'Aliberti will present their General Exam "Learning Machine Behavior: Measuring Exploration, Stability, and Alignment in Learned Agents" on Tuesday, May 26, 2026 at 1:00 PM in Sherrerd 306
by CS Grad Department 21 May '26

21 May '26

Liv d'Aliberti will present their General Exam "Learning Machine Behavior: Measuring Exploration, Stability, and Alignment in Learned Agents" on Tuesday, May 26, 2026 at 1:00 PM in Sherrerd 306. Committee Members: Manoel Horta Ribeiro (advisor), Peter Henderson, Tom Griffiths Abstract: Modern AI systems increasingly behave less like static predictors and more like learned agents: they reason over multiple steps, explore alternative responses, adapt through feedback, and participate in human institutions. As these systems become more capable and socially consequential, evaluation must move beyond average benchmark performance. We need tools for asking behavioral questions: which behaviors are actually present? Are they stable across prompts, samples, and training runs? Do they reflect a genuine learned capability, or an artifact of prompting, sampling, optimization, or interpretation? This talk centers on “The Illusion of Insight in Reasoning Models,” which studies whether large reasoning models exhibit intrinsic “Aha!” moments. Rather than treating insight as self-evident from a reasoning trace, I frame it as a behavioral construct that must be operationalized, measured, and tested. The goal is not to deny that reasoning models exhibit interesting behavior, but to separate robust behavioral evidence from compelling anthropomorphic stories. This perspective draws on cognitive science and statistical evaluation: claims about model cognition require construct validity, robustness checks, and careful alternatives to surface-level interpretation. I then connect this measurement problem to broader questions in Reinforcement Learning (RL) and alignment. Ongoing work on behavior-consistent RL asks whether agents with similar returns actually learn similar behaviors across random seeds, while work on exploration in Large Language Model (LLM) fine-tuning asks whether diversity should enter learning at the level of tokens, prompts, or candidate solutions. Together, these projects point toward a science of learned machine behavior: one that rigorously tests behavioral claims, identifies when evaluation artifacts masquerade as capabilities, and designs learning algorithms whose behavior is more reliable, interpretable, and aligned with human interests. Reading List: https://docs.google.com/document/d/1mSkrxB-SvCrvIhsne3VDMqYFxf3lMbCkg8z8QM3… Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0

Haoyu Zhao will present his FPO "Data-Centric Foundations of Compositional Generalization in Large Language Models" on Friday, May 29, 2026 at 1:00 PM in CS 402.
by CS Grad Department 21 May '26

21 May '26

Haoyu Zhao will present his FPO "Data-Centric Foundations of Compositional Generalization in Large Language Models" on Friday, May 29, 2026 at 1:00 PM in CS 402. The members of Haoyu’s committee are as follows: Examiners: Sanjeev Arora (Adviser) Elad Hazan, Chi Jin, Readers: Karthik Narasimhan, Danqi Chen A copy of his thesis is available upon request. Please email gradinfo(a)cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend the talk. Abstract follows below: Large language models (LLMs) exhibit remarkable capabilities in language understanding, reasoning, and code generation, yet they often remain brittle when tasks require systematic composition of learned components. This dissertation argues that such strengths and weaknesses are shaped not only by model architecture or scale, but fundamentally by the structure of the data distributions through which models are trained and evaluated. We develop a data-centric perspective on compositional generalization through two complementary settings. First, we study how compositional structure can emerge in language models from appropriately structured data. In the setting of masked language modeling, we show that transformers trained on synthetically generated data can approximate classical parsing procedures such as the Inside–Outside algorithm, providing both theoretical and empirical evidence that latent hierarchical structure can arise without explicit supervision. We then extend this perspective to higher-level behavior through controlled skill composition tasks, showing that the ability to combine multiple skills is not automatic, but depends critically on the diversity and structure of compositional examples seen during training. Second, we study compositional reasoning under formal constraints, where correctness must be exact rather than approximate. We introduce Ineq-Comp, a benchmark for inequality theorem proving that systematically varies compositional structure through simple, human-intuitive transformations. Despite strong performance on standard problems, state-of-the-art provers degrade substantially on these variants, revealing a persistent gap between solving familiar patterns and composing known reasoning steps in formally verified settings. We then present a scalable theorem-proving pipeline that integrates synthetic data generation, scaffolded decomposition, and verifier-guided self-correction, showing that carefully designed data pipelines can substantially improve formal reasoning performance. Taken together, these results support a central thesis: compositional generalization in large language models is fundamentally shaped by the structure of their effective data distribution. By viewing pretraining corpora, synthetic supervision, benchmarks, and verifier feedback as different ways of organizing that distribution, this dissertation provides both a conceptual framework and practical guidance for designing language models with stronger compositional reasoning abilities.

1 0

Varun Nagaraj Rao will present his FPO "Toward Human-Centered, Evidence-Based Policy on AI's Labor Impacts" on Wednesday, May 27, 2026 at 10:00 AM in Sherrerd Hall 306 (CITP Conference Room) and Zoom.
by CS Grad Department 21 May '26

21 May '26

Varun Nagaraj Rao will present his FPO "Toward Human-Centered, Evidence-Based Policy on AI's Labor Impacts" on Wednesday, May 27, 2026 at 10:00 AM in Sherrerd Hall 306 (CITP Conference Room) and Zoom. Location: Zoom link: https://princeton.zoom.us/j/96896715417?pwd=nls0CXVf7w6pfpbG0QbfnDU8OiDWPi.… The members of Varun’s committee are as follows: Examiners: Andrés Monroy-Hernández (Adviser), Arvind Narayanan, Peter Henderson Readers: Manoel Horta Ribeiro, Solon Barocas (Microsoft Research) A copy of his thesis is available upon request. Please email gradinfo(a)cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend his talk. Abstract follows below: Public discussion of AI and labor often centers on future job loss, obscuring how AI and associated algorithmic systems are transforming work today. For policymakers, labor organizers, and civil society groups, a key challenge is understanding how these systems currently shape workers’ pay, opportunities, and ability to contest decisions, and how to gather evidence for oversight and intervention. However, such evidence is hard to obtain. The systems managing work are often opaque, firm-controlled, and rapidly changing, and workers’ experiences are often embedded in unstructured sources. As a result, workers lack visibility into how these systems operate, and access to the data needed to challenge consequential decisions, and understand their impacts. In this dissertation, I show how worker-centered evidence about these impacts can be generated and help address these information and power asymmetries, in three ways. First, I develop a LLM-based sensemaking method to extract worker concerns from large-scale unstructured text and evaluate whether it can support policy research. Second, I study opaque AI and algorithmic decisions in social media job advertising and rideshare work to understand how they shape pay and opportunity. Third, I develop systems with labor organizations to generate quantitative evidence for legislation and appeals under state policy. Taken together, this dissertation shows how to generate policy-relevant, human-centered evidence about AI’s labor impacts and translate it into forms that inform policy and support workers.

1 0

Wentao Guo will present his General Exam "Accelerating MoE with IO-aware and tile-aware optimizations" on Friday, May 22, 2026 at 12:30 PM in CS 401 and via zoom.
by CS Grad Department 20 May '26

20 May '26

Wentao Guo will present his General Exam "Accelerating MoE with IO-aware and tile-aware optimizations" on Friday, May 22, 2026 at 12:30 PM in CS 401 and via zoom. Zoom link: https://princeton.zoom.us/j/9317908194 Committee Members: Tri Dao (advisor), Ravi Netravali, Kai Li Abstract: Mixture-of-Experts (MoE) models have emerged as the dominant architecture for scaling language models without proportional increases in training compute. Recent frontier MoE models exhibit a clear trend toward fine-grained experts (smaller intermediate dimension) and higher sparsity (more total experts at constant activated count), which improve model quality per FLOP but introduce significant hardware inefficiencies. Activation memory grows linearly with expert granularity, arithmetic intensity drops as experts become smaller and sparser, and grouped GEMM kernels waste compute on tile-size padding when each expert receives few tokens. These costs compound on modern GPUs, where memory bandwidth rather than tensor-core throughput often determines kernel runtime. In this talk, I will present SonicMoE, a hardware/algorithm co-design that addresses these challenges through three contributions. First, I will derive an activation memory-efficient MoE algorithm for fine-grained MoEs by avoiding materialization of any intermediate tensor whose size scales with the number of activated experts. Second, I will describe IO-aware grouped GEMM kernels for both NVIDIA Hopper and Blackwell GPUs that fuse gather operations with global-memory loads, fuse activation functions with the GEMM epilogue, and hide memory IO behind tensor-core computation through Ping-Pong scheduling on Hopper and Tensor Memory double-buffering on Blackwell. Third, I will introduce a tile-aware token rounding routing method that eliminates compute wasted on grouped-GEMM padding under highly sparse MoE settings while preserving downstream task performance. For a 7B fine-grained MoE on H100 GPUs, SonicMoE reduces activation memory by 45% and improves forward-pass throughput by 1.86× over ScatterMoE, achieving training throughput on 64 H100s comparable to ScatterMoE on 96 H100s. I will further outline ongoing research for extending these IO-aware optimization techniques to expert parallelism and low-precision training in MXFP8. Reading List: https://docs.google.com/document/d/1RiC19A195_AGxRByVPD304wK79JY2hEm7kW1hYd… Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0

Rohit Agarwal will present his General Exam "AI Alignment in Agentic Pipelines via Incentives and Correction" on Friday, May 15, 2026 at 2:00 PM in CS 301 and via zoom.
by CS Grad Department 12 May '26

12 May '26

Rohit Agarwal will present his General Exam "AI Alignment in Agentic Pipelines via Incentives and Correction" on Friday, May 15, 2026 at 2:00 PM in CS 301 and via zoom. Zoom link: https://princeton.zoom.us/j/7714894406 Committee Members: Elad Hazan (advisor), Sanjeev Arora, Peter Henderson Abstract: We propose a mechanism-design perspective on AI alignment in agentic pipelines. The key observation is that alignment in a multi-agent setting is a fixed-point problem: penalizing misbehavior may deter a solver, but it can also reduce an auditor's incentive to monitor, since auditing then mainly incurs cost on a population that already appears aligned. Thus, robust alignment requires not only discouraging bad behavior, but also preserving incentives for oversight. We also discuss the applications of this viewpoint in real-life Large Language Model settings, in coding through an empirical reinforcement learning setup, and in mathematics through empirical agentic pipeline design. Reading List: https://docs.google.com/document/d/1Ji1xpqK-0S5saeVjwodH07aXmU_iQo0XvYYVTcV… Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0