Colloquia and Seminars

A well-known application of the celebrated color-coding technique is fast detection of paths in a distributed setting with limited bandwidth, by propagating a signal along colorful paths [Even et al., DISC 2017]. However, since vertices of the same color are indistinguishable by this procedure, it cannot detect induced paths, as they appear the same as cycles.

We present a distributed local-counting technique that allows us to design fast algorithms for detecting induced paths, improving upon the state of the art in several aspects (time complexity, detection variant, and more).

The following observation illustrates our key technical ingredient: For each edge, count the number of signals, over all permutations of the random coloring, that terminate at that edge. An induced path contributes one to that count, while a cycle contributes two. Refining and generalizing this idea lets us distinguish induced 4-paths from other 4-vertex subgraphs in constant time and yields fast algorithms for detecting paths of lengths 5 and 6.

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.

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.

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.