[ Software Research Lunch ]


The Stanford Software Research Lunch is a weekly event on Thursday where students and researchers present their latest work to peers. Talks are open to anybody, but regular attendees are expected to give a presentation on their work.

Mailing list: software-research-lunch@lists.stanford.edu (subscribe via mailman)

Calendar: ical

Format: The lunch is held every week during fall, winter and spring quarter. The first week of every quarter is an organizational lunch where people can sign up to give a talk. If you'd like to give a talk, please contact Matthew Sotoudeh or Anjiang Wei.

Past quarters: Fall 2023, Spring 2023, Winter 2023, Fall 2022, Winter 2021, Fall 2020, Winter 2020, Fall 2019, Spring 2019, Winter 2019, Fall 2018, Spring 2018, Winter 2018, Fall 2017, Spring 2017, Winter 2017, Fall 2016.

Upcoming quarters: Spring 2024.

Ordering Food: For suggestions for those ordering food for the lunch, see here.


1/11: TBD (Ying Sheng)

Time: Thursday, January 11, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Ying Sheng

Food:


1/18: Program Analysis: A Journey through Traditional Methods, Emerging Data-Driven Approaches, and Machine Learning Applications

Time: Thursday, January 18, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Ke Wang

Abstract: Program analysis, the process of analyzing source code to derive its properties, has been a prominent research area for decades. Effective program analysis methods have played a pivotal role in ensuring program correctness and optimizing performance. In this talk, I will walk you through a journey centered around program analysis, in particular, it starts with classical symbolic-, logic-based analysis/testing techniques, ventures into the realm of emerging data-driven approaches, and concludes with their applications in machine learning models. I will not only share the results of my research in compiler optimization, bug detection, and model hardening, but more importantly, I will discuss my research vision and plan for building the next-generation programming environment.

Food:


1/25: Fairness in serving large language models

Time: Thursday, January 25, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Ying Sheng

Abstract: High-demand LLM inference services (e.g., ChatGPT and BARD) support a wide range of requests from short chat conversations to long document reading. To ensure that all client requests are processed fairly, most major LLM inference services have request rate limits, to ensure that no client can dominate the request queue. However, this rudimentary notion of fairness also results in under-utilization of the resources and poor client experience when there is spare capacity. While there is a rich literature on fair scheduling, serving LLMs presents new challenges due to their unpredictable request lengths and their unique batching characteristics on parallel accelerators. This paper introduces the definition of LLM serving fairness based on a cost function that accounts for the number of input and output tokens processed. To achieve fairness in serving, we propose a novel scheduling algorithm, the Virtual Token Counter (VTC), a fair scheduler based on the continuous batching mechanism. We prove a 2x tight upper bound on the service difference between two backlogged clients, adhering to the requirement of work-conserving. Through extensive experiments, we demonstrate the superior performance of VTC in ensuring fairness, especially in contrast to other baseline methods, which exhibit shortcomings under various conditions.

Food:


2/1: Garbage Collection

Time: Thursday, February 1, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Matthew Sotoudeh

Abstract: We'll answer some natural questions regarding asymptotic lower and upper bounds on the performance of garbage collection in adversarial environments.

Food:


2/8: KDRSolvers: Scalable, Flexible, Task-Oriented Krylov Solvers

Time: Thursday, February 8, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: David K. Zhang

Abstract: We present KDRSolvers, a novel framework for representing sparse linear systems and implementing Krylov subspace algorithms on heterogeneous, distributed-memory parallel computers. KDRSolvers unifies a variety of sparse matrix storage formats (e.g., COO, CSR, CSC) with the language of dependent partitioning, representing the formats as abstract maps that relate a matrix's domain, range, and nonzero entries. This unification enables KDRSolvers to define universal co-partitioning operators for matrix and vector data, not tied to any specific storage format, which facilitates rapid prototyping and performance evaluation of different data layouts and partitioning strategies. KDRSolvers also introduces multi-operator systems in which matrices and vectors can be constructed from multiple non-contiguous pieces without data movement. Our implementation of KDRSolvers, which targets the Legion runtime system, achieves greater flexibility and competitive performance compared to established systems, such as PETSc and Trilinos. In experiments with up to 256 nodes on the Lassen supercomputer, our implementation achieves up to a 9.6% reduction in execution time per iteration on large problem sizes.

Food:


2/15: TBD (Geoff Ramseyer)

Time: Thursday, February 15, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Geoff Ramseyer

Food:


2/22: Split Groebner Bases for Satisfiability Modulo Finite Fields

Time: Thursday, February 22, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Alex Ozdemir

Abstract: Satisfiability modulo finite fields enables automated verification for cryptosystems. Unfortunately, previous solvers scale poorly for even some simple systems of field equations, in part because they build a full Gröbner basis (GB) for the system. We propose a new solver that uses multiple, simpler GBs instead of one full GB. Our solver, implemented within the cvc5 SMT solver, admits specialized propagation algorithms, e.g., for understanding bitsums. Experiments show that it solves important bitsum-heavy determinism benchmarks far faster than prior solvers, without introducing much overhead for other benchmarks.

Food:


2/29: Better Defunctionalization through Lambda Set Specialization

Time: Thursday, February 29, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Benjamin Driscoll

Abstract: Higher-order functions pose a challenge for both static program analyses and optimizing compilers. To simplify the analysis and compilation of languages with higher-order functions, a rich body of prior work has proposed a variety of defunctionalization teques, which can eliminate higher-order functions from a program by transforming the program to a semantically-equivalent first-order representation. Several modern languages take this a step further, specializing higher-order functions with respect to the functions on which they operate, and in turn allowing compilers to generate more efficient code. However, existing specializing defunctionalization teques restrict how function values may be used, forcing implementations to fall back on costly dynamic alternatives. We propose lambda set specialization (LSS), the first specializing defunctionalization teque which imposes no restrictions on how function values may be used. We formulate LSS in terms of a polymorphic type system which tracks the flow of function values through the program, and use this type system to recast specialization of higher-order functions with respect to their arguments as a form of type monomorphization. We show that our type system admits a simple and tractable type inference algorithm, and give a formalization and fully-mechanized proof in the Isabelle/HOL proof assistant showing soundness and completeness of the type inference algorithm with respect to the type system. To show the benefits of LSS, we evaluate its impact on the run time performance of code generated by the MLton compiler for Standard ML, the OCaml compiler, and the new Morphic functional programming language. We find that pre-processing with LSS achieves run time speedups of up to 6.85x under MLton, 3.45x for OCaml, and 78.93x for Morphic.

Food:


3/7: LLMs for the Lean Theorem Prover and Mathematics

Time: Thursday, March 7, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Brando Miranda

Abstract: Morph Prover v0 7B, the first open-source model trained as a conversational assistant for Lean users. This model was trained in collaboration with Nous Research and the Safe and Trustworthy AI Research (STAIR) group at Stanford led by professor Sanmi Koyejo, with major contributions by Brando Miranda of Stanford and help from Peter Holderrieth of MIT and Jin Peng Zhou of Cornell. Thanks to Nomic AI's GPT4All Vulkan support, this model can run on any consumer GPU. Morph Prover v0 7B is a chat fine-tune of Mistral 7B which achieves state of the art results in autoformalization while performing better than the original Mistral model on benchmarks like AGIEval and MMLU. It was trained with a proprietary synthetic data pipeline with code data generated by the Morph Code Index. Contrary to the conventional emphasis on dataset size, we explore the role of data alignment---an often overlooked aspect of data quality---in training capable Large Language Models (LLMs). This is especially promising for data scare tasks like, like AutoFormalization. We define AutoFormalization as the processes of translating natural language into formal language (e.g., Lean). We find a strong, predictable negative relationship that correlates the alignment coefficient between a model's training and evaluation data and the model's loss on the respective downstream task like AutoFormalization. These findings suggest a re-evaluation of LLM training approaches, demonstrating the relevance of data alignment compared to data size, especially in specialized downstream tasks such as AutoFormalization.

Food:


3/14: Software Lightning Talks

Time: Thursday, March 14, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Matthew Sotoudeh, Paul Crews, Zachary Yedidia, David K. Zhang, Mert Hidayetoglu, Robert Schenck, ...

Abstract: Multiple speakers from our department will each give a short lightning talk on one of their projects. Note to make time for multiple speakers, we will start promptly at noon instead of having the traditional 15-minute social time.

Food:


3/21: TBD (Rupanshu Soi)

Time: Thursday, March 21, 2024, 12 noon - 1pm
Location: Gates 415

Speaker: Rupanshu Soi

Food: