Colloquia and Seminars

Many program‑safety verification tasks reduce to deciding the satisfiability of Constrained Horn Clauses (CHCs). When a program depends on bit‑level behavior such as bitwise logic, shifts, or overflow‑sensitive arithmetic, encoding its CHCs over the theory of fixed‑size bit‑vectors is exact but scales poorly, whereas encoding them over integer arithmetic is far more tractable but requires an expensive modeling of the bit‑level operations that can cancel out the gain. We present the first implementation of a theory‑modular framework, designed by our advisors, that avoids committing to either theory. It partitions a set of bit‑vector CHCs into a bit‑vector fragment and an integer fragment linked by interface constraints, and a backward‑reasoning algorithm discharges the two with separate, theory‑specific solvers, crossing between them and iteratively strengthening the interface to avoid re‑deriving already‑refuted reasoning. We further present a proof‑of‑concept abstraction‑refinement extension that abstracts bit‑manipulating subexpressions during translation and refines them on demand, lightening the load on the bit‑vector solver.

We initiate the study of online contracts, which integrate the game-theoretic considerations of economic contract theory, with the algorithmic and informational challenges of online algorithm design. Our starting point is the classic online setting with preemption of Buchbinder et al. [SODA'15], in which a hiring principal faces a sequence of adversarial agent arrivals. Upon arrival, the principal must decide whether to tentatively accept the agent to their team, and whether to dismiss previous tentative choices. Dismissal is irrevocable, giving the setting its online decision-making flavor. In our setting, the agents are rational players: once the team is finalized, a game is played where the principal offers contracts (performance-based payment schemes), and each agent decides whether or not to work. Working agents reward the principal, and the goal is to choose a team that maximizes the principal's utility. Our main positive result is a 1/2-competitive algorithm when agent rewards are additive, which matches the best-possible competitive ratio. Our algorithm is randomized and this is necessary, as we show that no deterministic algorithm can attain a bounded competitive ratio. Moreover, if agent rewards are allowed to exhibit combinatorial structure known as XOS, even randomized algorithms might fail. En route to our competitive algorithm, we develop the technique of balance points, which can be useful for further exploration of online contracts in the adversarial model.

My research focuses on knowledge and dynamics of language models - spanning their fine-tuning efficiency, training dynamics, and mergeability. I will begin by introducing Fast Forward, a simple optimization strategy that significantly accelerates large segments of low-rank training to save computational costs. Next, I will explore the training dynamics of large language models, revealing the fundamental disconnect between how internal parametric knowledge and external knowledge are acquired and forgotten over trainin.. We will then transition to the biological domain to examine the training dynamics of protein language models. Finally, I will conclude by exploring the underlying causes of model mergeability, demonstrating how a base model's prior knowledge influences the success of merging multiple fine-tuned models into a single multitask model. Together, these works provide deeper insights into the mechanics of model knowledge and learning and offer practical methods for more efficient and robust AI development.

Classical approaches to geometric differential invariants begin by specifying a transformation group, analytically deriving the corresponding invariant differential quantities, and constructing numerical schemes to approximate them. This work takes a data-driven perspective and introduces a self-supervised deep learning framework for learning group-equivariant semi-local geometric operators directly from point samples of planar curves. Specifically, we train a neural network to act as a discrete differentiation operator. Remarkably, the learned operator behaves as a discrete approximation to differentiation with respect to the corresponding group-invariant arc length. The framework requires no fixed parameterization and remains robust under non-uniform sampling and noise. Experiments demonstrate that the learned operators generalize across a wide range of curve geometries and successfully handle line-preserving transformation groups, including the Euclidean, similarity and equi-affine groups. The learned differential operators transfer directly to downstream shape-analysis tasks without retraining. The resulting framework is a data-driven foundation for approximating geometric invariants from discrete observations.

Free recall is a standard memory task in which a subject is presented with a sequence of items and, after presentation, asked to retrieve as many as possible in any order. Understanding free recall is not only a question of retrieval capacity, but also of retrieval structure: recalled items appear in clusters, transitions are highly non-random, and retrieval depends strongly on temporal position. We introduce the Tree of Memory (TOM), a computational model in which memory is represented by a hierarchical episodic data structure (episodic tree) augmented with a sparse semantic graph. Experience is organized across multiple temporal scales in different levels of the hierarchy, and recall is modeled as a probabilistic search process over this representation. Specifically, retrieval proceeds through a stochastic depth-first traversal of the episodic tree, interleaved with local exploration of semantic edges whenever an item is reached.

We characterize distinct asymptotic recall regimes and show that the expected number of retrieved items grows logarithmically or as a sublinear power law, depending on how the probability of traversing deeper levels of the memory hierarchy scales with list length. We also study how the same memory representation supports different retrieval algorithms. This allows us to ask how changes in search strategy and auxiliary structure affect recall efficiency. One variant introduces additional semantic links that guide retrieval through a learned sequence, yielding linear recall in list length with high probability. Another uses a small set of pointers to recently formed subtrees, enabling efficient retrieval of entire temporal chunks. These variants highlight explicit trade-offs between recall performance, representation complexity, scalability, and auxiliary memory. Simulations further show that TOM reproduces canonical empirical signatures of free recall. Together, these results suggest that hierarchical representations and probabilistic graph search provide a compact computational framework for understanding both spontaneous and strategy-driven memory retrieval.