- talks - lists.cs.princeton.edu

Joomy Korkut will present his FPO "Foreign Function Verification Through Metaprogramming" on October 9th, 2024 at 3pm in
by Gradinfo 25 Sep '24

25 Sep '24

Joomy Korkut will present his FPO "Foreign Function Verification Through Metaprogramming" on October 9th, 2024 at 3pm in Friend 202. Committee members: Examiners: Andrew Appel (adviser), Aarti Gupta, David Walker Readers: Zakary Kincaid and Matthieu Sozeau (INRIA Nantes) All are welcome to attend. Abstract: CertiCoq is a compiler from Coq to C that is verified in Coq. Thanks to CertiCoq’s mechanically checked proof of compiler correctness, users can be sure that programs they write and verify in Coq’s rich type system output the same results when compiled to C (and to machine language, via the CompCert verified compiler). However, in practice, large programs are rarely written in a single language; additional languages are used for better performance or for capabilities that the primary language lacks. In particular, because Coq lacks user-defined primitive types, mutation, and input/output actions, CertiCoq-compiled code must interact with another language to have those capabilities. Specifically, Coq code must be able to call C code and C code must be able to inspect and generate Coq values and call Coq code. But what happens to the correctness proofs when these two languages interact? A foreign C function has to be memory-safe, return the expected result, and have the expected side effect (or no effect). A specification that expresses these requirements must combine plain Coq, for the functional parts, and a program logic for C (such as the Verified Software Toolchain [VST]), for the verification of C functions. While VST is embedded in Coq, its specification language is quite different. Bridging this gap by connecting plain Coq and VST theorems in both directions requires a system of techniques and methods, many of which are made feasible by using metaprogramming as a general methodological approach. In this dissertation, I describe these techniques and methods. VST proofs about C foreign functions do not directly translate to proofs about Coq primitives. To bridge this gap, I propose a method of relating foreign functions and types to their functional models, allowing users to write proofs in plain Coq. I also provide examples of Coq programs with primitive types, mutation, and I/O actions, along with their correctness proofs, and demonstrate VeriFFI, the verified foreign function interface for CertiCoq.

1 0

Invitation: Natural and Artificial Minds Launch Event: Thurs, Sept 26, 4pm
by Emily C. Lawrence 20 Sep '24

20 Sep '24

You are invited to the launch event for [ https://ai.princeton.edu/nam | Natural and Artificial Minds ] (NAM), a new AI Lab research initiative reenvisioning theory-driven cognitive science research in the age of artificial intelligence. [ https://ai.princeton.edu/nam-launch | Natural and Artificial Minds (NAM) Launch Event ] Date: Thursday, September 26, 4-6pm Location: Maeder Hall at Andlinger Center, 86 Olden Street [ https://forms.gle/bAMBy4PWEY8w3g61A | Registration ] The program opens with remarks by NAM co-directors Sarah-Jane Leslie and Tania Lombrozo. Two distinguished keynote lectures will follow: “Natural and Artificial Minds: Are they as Smart as We think?” by James L. (Jay) McClelland , and “ Empowerment as Causal Learning: Causal Learning as Empowerment ” by Alison Gopnik. The event will conclude with a reception. We look forward to seeing you on September 26 th ! Best regards, Sarah-Jane and Tania Sarah-Jane Leslie Class of 1943 Professor of Philosophy Tania Lombrozo Arthur W. Marks ’19 Professor of Psychology

1 0

CSML Lunchtime Faculty Series: Sept 24 at 12:30pm
by Emily C. Lawrence 19 Sep '24

19 Sep '24

Center for Statistics and Machine Learning Faculty Lunchtime Seminars Featuring CSML Affiliated Faculty Members Speaker: Peter Henderson, Princeton University Title: AI Safety, Governance, and Evaluation When Models Can be Customized Day: September 24, 2024 Place CSML, Bendheim House, 26 Prospect Ave, Room 103 Time: 12:30-1:30 PM Lunch available from12:15 with RSVP to csml(a)princeton.edu Host: Peter Ramadge, CSML Director, Gordon Y.S. Wu Professor of Engineering Event info: [ https://csml.princeton.edu/events/ai-safety-governance-and-evaluation-when-… | https://csml.princeton.edu/events/ai-safety-governance-and-evaluation-when-… ] Abstract: New regulatory requirements would have AI model developers assure that models cannot induce harms even when downstream users can modify the model in different ways. This talk will examine these regulatory regimes, the challenges of such pre-deployment evaluation requirements, and potential paths forward for addressing safety concerns.

1 0

Ziyang Xu will present his FPO "A Fast and Extensible Memory Profiling Framework" on September 27, 2024 at 10am in Friend 125.
by Nicki Mahler 16 Sep '24

16 Sep '24

Ziyang Xu will present his FPO "A Fast and Extensible Memory Profiling Framework" on September 27, 2024 at 10am in Friend 125. The members of his committee are as follows: Examiners: David August (adviser), Aarti Gupta, Amit Levy Readers: Zachary Kincaid and Simone Campanoni (Northwestern University) Abstract: Recent advancements in automatic parallelization offer a promising way to fully leverage modern processors, yet these techniques remain underutilized. To understand this gap, this dissertation presents a field study of the computational usage and needs. The study reveals that although many researchers have access to abundant parallel resources, they often lack the necessary tools or expertise to utilize them effectively, highlighting the need for practical, user-friendly, and efficient solutions. This dissertation explores the practicality of memory profiling, a critical technique for automatic parallelization. Memory profiling captures programs' dynamic memory behavior, assisting in debugging, tuning, and enabling advanced compiler optimizations. Building practical memory profilers often requires extensive compiler expertise, adeptness in program optimization, and significant implementation efforts, leaving a gap in the availability of fast and efficient profilers. To bridge this gap, this dissertation presents PROMPT, a pioneering framework for streamlined development of fast memory profilers. With it, developers only need to specify profiling events and define the core profiling logic, bypassing the complexities of custom instrumentation and intricate memory profiling components and optimizations. By integrating dynamic binary instrumentation alongside LLVM-IR and source instrumentation, PROMPT ensures comprehensive memory access coverage while reducing reliance on binary instrumentation. Two state-of-the-art memory profilers were ported to PROMPT with all features preserved. By focusing on the core profiling logic, the code was reduced by more than 65% and the profiling speed was improved by 5.3x and 7.1x respectively. To further underscore PROMPT's impact, a tailored memory profiling workflow was constructed for a sophisticated compiler optimization client. In just 570 lines of code, this redesigned workflow satisfies the client's memory profiling needs while achieving more than 90% reduction in profiling time and improved robustness compared to the original profilers.

1 0

Reminder: PPH seminar TODAY @ 12 pm, Guillermo Sapiro
by Emily C. Lawrence 12 Sep '24

12 Sep '24

Please join the Princeton Precision Health (PPH) Initiative for a seminar on Friday, September 13, at 12:00 pm, at 252 Nassau Street: Guillermo Sapiro, PhD, Electrical and Computer Engineering, Princeton University A Wearable-Based Biomarker of Aging and Its Association With Disease and Behavior Biomarkers of aging play a vital role in understanding human longevity and have the potential to inform clinical decisions and new interventions. Existing measures of biological age are typically based on blood, saliva, vital signs, or clinical imaging. Wearables, however, can make convenient, frequent, and inexpensive measurements throughout daily life, scaled to an entire population. We propose PPGAge, a biomarker that is non-invasively, passively, and longitudinally measurable by photoplethysmography (PPG) collected from a consumer wearable. With data from the Apple Heart & Movement Study (n=213,593 participants and over 149 million participant-days), we develop a statistical model of healthy aging and study its association with disease and behavior. PPGAge predicts chronological age with mean absolute error (MAE) of 2.43 years (95% CI 2.33--2.53) in a healthy cohort and 3.18 years (95% CI 3.16--3.19) in a general cohort. Among participants with a PPGAge gap (i.e., the deviation between predicted age and chronological age) larger than 6 years, diagnosis rates of heart disease, heart failure, and diabetes are 1.5--5 times the age- and sex-adjusted average. PPGAge is also associated with behavior, including smoking, exercise, and sleep. In longitudinal analyses, PPGAge exhibits a sharp increase during pregnancy and around the time of certain types of cardiac events. With additional evidence, PPGAge may be a useful surrogate for healthy aging in the study of human longevity and the treatment of age-related conditions. Joint work with A. Miller, J. Futoma, S. Abbaspourazad, C. Heinze-Deml, S. Emrani, and I. Shapiro. Lunch will be provided. Please note that getting to the seminar space currently requires that you climb a set of stairs. If an accommodation is needed, please contact PPH in advance at: [ mailto:princetonPPH@princeton.edu | princetonPPH(a)princeton.edu ]

1 1

PPH seminar on Friday @ 12 pm, Guillermo Sapiro
by Emily C. Lawrence 09 Sep '24

09 Sep '24

Please join the Princeton Precision Health (PPH) Initiative for a seminar on Friday, September 13, at 12:00 pm, at 252 Nassau Street: Guillermo Sapiro, PhD, Electrical and Computer Engineering, Princeton University A Wearable-Based Biomarker of Aging and Its Association With Disease and Behavior Biomarkers of aging play a vital role in understanding human longevity and have the potential to inform clinical decisions and new interventions. Existing measures of biological age are typically based on blood, saliva, vital signs, or clinical imaging. Wearables, however, can make convenient, frequent, and inexpensive measurements throughout daily life, scaled to an entire population. We propose PPGAge, a biomarker that is non-invasively, passively, and longitudinally measurable by photoplethysmography (PPG) collected from a consumer wearable. With data from the Apple Heart & Movement Study (n=213,593 participants and over 149 million participant-days), we develop a statistical model of healthy aging and study its association with disease and behavior. PPGAge predicts chronological age with mean absolute error (MAE) of 2.43 years (95% CI 2.33--2.53) in a healthy cohort and 3.18 years (95% CI 3.16--3.19) in a general cohort. Among participants with a PPGAge gap (i.e., the deviation between predicted age and chronological age) larger than 6 years, diagnosis rates of heart disease, heart failure, and diabetes are 1.5--5 times the age- and sex-adjusted average. PPGAge is also associated with behavior, including smoking, exercise, and sleep. In longitudinal analyses, PPGAge exhibits a sharp increase during pregnancy and around the time of certain types of cardiac events. With additional evidence, PPGAge may be a useful surrogate for healthy aging in the study of human longevity and the treatment of age-related conditions. Joint work with A. Miller, J. Futoma, S. Abbaspourazad, C. Heinze-Deml, S. Emrani, and I. Shapiro. Lunch will be provided. Please note that getting to the seminar space currently requires that you climb a set of stairs. If an accommodation is needed, please contact PPH in advance at: [ mailto:princetonPPH@princeton.edu | princetonPPH(a)princeton.edu ]

1 0

DeCenter: upcoming events
by Emily C. Lawrence 05 Sep '24

05 Sep '24

The DeCenter hopes you had a great summer and is excited to welcome you back to campus with some exciting announcements. We are excited to announce our first two events of the year. Our first on-campus seminar of the year will be given by Aviv Zohar, a professor at the Hebrew University of Jerusalem and a Princeton University Sabbatical Visitor. His talk, titled "Speculative Denial-of-Service Attacks in Ethereum," will take place on September 18th, 2024, at 4:30 PM in the Friend Center Convocation Room (113). We are also excited to announce the inaugural Princeton University DeCenter Alumni Mixer. This alumni-only event will take place on October 17th from 6:00 PM to 8:00 PM at the Arlo NoMad Hotel rooftop in NYC and will feature a short talk from the DeCenter faculty directors. The event is free to alums, but space is limited, so please register through the provided Eventbrite link to secure your spot. [ https://www.eventbrite.com/e/1002571938657?aff=oddtdtcreator | https://www.eventbrite.com/e/1002571938657?aff=oddtdtcreator ]

1 0

Yue Tan will present her FPO "FAASTEN: An Architecture and implementation for securing cloud applications" on September 5, 2024 at 11am in CS 302.
by Gradinfo 15 Aug '24

15 Aug '24

Yue Tan will present her FPO "FAASTEN: An Architecture and implementation for securing cloud applications" on September 5, 2024 at 11am in CS 302. The members of her committee are as follows: Amit Levy (advisor), Maria Apostolaki, Wyatt Lloyd Readers: Mae Milano and Marcus Peinado (Microsoft Research) All are welcome to attend. The FPO abstract follows below: Modern web applications have evolved into intricate networks of micro-applications, posing challenges in ensuring the security of user data confidentiality and integrity. In the current discretionary security paradigm, developers must enforce policies for every microapplication and all data paths that can arise at run-time. A promising alternative paradigm, decentralized information flow control (DIFC), suggests that the underlying system should enforce policies by tracking information flows. As the cloud has become a standard operating system for developing web applications, this paper proposes the first DIFC design for the cloud. We present Faasten, an architecture and implementation for securing cloud applications. Faasten includes a DIFC model and a FaaS-inspired system interface that implements the DIFC model. We provide a detailed interface security analysis and showcase how three representative cloud applications benefit from Faasten. We also show that Faasten introduces negligible latencies in controlling information flows and policy storage costs.

1 0

Samuel Ginzburg will present his FPO "VectorVisor: A Binary Translation Scheme for Throughput-Oriented GPU Acceleration" on Thursday, August 29, 2024 in CS 302 at 1pm.
by Gradinfo 15 Aug '24

15 Aug '24

Samuel Ginzburg will present his FPO "VectorVisor: A Binary Translation Scheme for Throughput-Oriented GPU Acceleration" on Thursday, August 29, 2024 in CS 302 at 1pm. The members of his FPO committee follows below: Examiners: Michael Freedman (Advisor), Wyatt Lloyd, and Amit Levy Readers: Mae Milano and Mohammad Shahrad (UBC) All are welcome to attend. Please see abstract below. Beyond conventional graphics applications, general-purpose GPU acceleration has had significant impact on machine learning and scientific computing workloads. Yet, it has failed to see widespread use for server-side applications, which we argue is because GPU programming models offer a level of abstraction that is either too low-level (e.g., OpenCL, CUDA) or too high-level (e.g., TensorFlow, Halide), depending on the language. Not all applications fit into either category, resulting in lost opportunities for GPU acceleration. We introduce VectorVisor, a vectorized binary translator that enables new opportunities for GPU acceleration by introducing a novel programming model for GPUs. With VectorVisor, many copies of the same server-side application are run concurrently on the GPU, where VectorVisor mimics the abstractions provided by CPU threads. To achieve this goal, we demonstrate how to (i) provide cross-platform support for system calls and recursion using continuations and (ii) make full use of the excess register file capacity and high memory bandwidth of GPUs. We then demonstrate that our binary translator is able to transparently accelerate certain classes of computebound workloads, gaining significant improvements in throughput-per-dollar of up to 2.9× compared to Intel x86-64 VMs in the cloud, and in some cases match the throughput-per-dollar of native CUDA baselines.

1 0

Kaifeng Lyu will present his FPO "Implicit Bias in Deep Learning Optimization: A Mathematical Examination" on Friday, August 9, 2024 at 10:30 AM in CS 402 and Zoom.
by CS Grad Department 02 Aug '24

02 Aug '24

Kaifeng Lyu will present his FPO " Implicit Bias in Deep Learning Optimization: A Mathematical Examination " on Friday, August 9, 2024 at 10:30 AM in CS 402 and Zoom. Location: Zoom link: https://princeton.zoom.us/j/99448789401 The members of Kaifeng ’s committee are as follows: Examiners: Sanjeev Arora (Adviser), Elad Hazan , Chi Jin Readers: Danqi Chen , Jason Lee 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: Deep learning has achieved remarkable success in recent years, yet training neural networks often involves a delicate combination of guesswork and hyperparameter tuning. A critical aspect of this process is the “implicit bias” of optimization methods, where minor changes in the optimization setup—without affecting the small training loss at convergence—can drastically shift the solution to which the model converges, thereby affecting test performance. This dissertation presents a collection of results that mathematically characterize this implicit bias in various training regimes. The first part of this dissertation explores how gradient descent, even without explicit regularization, can converge to solutions that maximize the margin. Previous results have established the first-order optimality of margin for homogeneous neural networks in general, but the global optimality of margin is not guaranteed due to their non-convex nature. This dissertation provides in-depth theoretical analyses when data has simple structures: for linearly separable data, we present both positive and negative results on whether the global optimality of margin can be attained. Furthermore, we show how this margin-based view can be used to explain interesting generalization phenomena in training neural networks with or without explicit regularization, including the simplicity bias and grokking phenomena. The second part of the dissertation presents two results that capture the implicit biases induced by finite learning rate. Many existing analyses, including the margin-based ones in the first part, describe implicit biases that hold even when the learning rate is infinitesimal. However, practical implementations use finite learning rates, which have been empirically observed to benefit generalization. We analyze how full-batch GD with finite learning rates, combined with key training components like normalization layers and weight decay, create a bias towards flatter minima, which are positively correlated with better generalization. Additionally, we study the implicit bias in stochastic optimization and derive rigorous approximations for the dynamics of adaptive gradient methods like Adam and RMSprop via Stochastic Differential Equations (SDEs) to capture the effect of finite learning rates. Based on this, we also derive the square root scaling rule as a practical guideline for adjusting the optimization hyperparameters of adaptive gradient methods when changing batch size.

1 0