Research

Outstanding Graduate Research in Computational Science

1st Prize: Srihari Nanniyur (Computer Science) Advisor: Siddhartha Jayanti

Multiplication Algorithms, Historical and Modern: Analysis and Formal Verification

We bring together the disciplines of formal verification, analysis of algorithms, and math history to analyze and machine-verify efficient multiplication algorithms from the medieval period to the twentieth century. First, we translate (from Sanskrit) and analyze the space-efficient medieval Indian Kavatasandhi algorithm, and we develop an even more space-efficient variant: Laghava Kavatasandhi. The modern fast multiplication algorithms we verify include Karatsuba, Toom-Cook, and Schönhage-Strassen (FFT-based). Finally, we verify two division algorithms (Goldschmidt and Newton-Raphson) that rely on fast multiplication. Our algorithmic specifications and proofs are written in Lean 4 with the assistance of the AI theorem prover Aristotle.

2nd Prize: Flora Perlmutter (Ecology, Evolution, Environment, and Society) Advisor: Justin Mankin

The Role of Sea Surface Temperatures in Regional Precipitation Variability and Trends

Robust regional precipitation projections are critical for planning and decision-making around water availability under climate change. A key source of uncertainty in precipitation projections is the pattern of oceanic warming. In this research, we create a library of the responses of river basin precipitation to sea surface temperature (SST) at every ocean grid cell using a linear regression model. We build a novel reconstruction of SST-forced precipitation that reveals SST forcing has significantly contributed to anomalies and trends in river basin precipitation. This understanding can be used to provide a foundation for constraining precipitation projections.

3rd Prize: Jae Hyung Woo (Psychological & Brain Sciences) Advisor: Alireza Soltani

Contribution of Amygdala to Dynamic Model Arbitration Under Uncertainty

The amygdala is a key subcortical brain region that is critical for learning about both rewarding and aversive stimuli. Yet, its precise contribution to decision-making remains debated. Using reinforcement learning models fitted to monkeys' choices during decision-making tasks, we show that the amygdala helps arbitrate between stimulus-based and action-based learning systems, rather than simply contributing to reward learning in a broad sense. Specifically, we found that the amygdala determines the initial balance between these competing systems and updates that balance as evidence accumulates. This novel role of amygdala helps reconcile conflicting earlier accounts of amygdala function and offers a broader framework for understanding how brains flexibly select among alternative internal models of the world in uncertain environments.

Outstanding Undergraduate Research in Computational Science

1st Prize: Joseph Quaratiello (Engineering Sciences) Advisor: Anthony Rizzo

Physics-Based Flow Matching for Full-Field Prediction of Silicon Photonic Devices

Silicon photonics is already pushing past the traditional limits Moore's Law imposes on transistor-based integrated circuits. Today, it powers applications ranging from high-bandwidth datacenter interconnects and biosensors to quantum computers, and is poised to underpin the energy-efficient hardware needed to sustain ever more power-hungry AI. Realizing this vision depends on rapidly designing increasingly complex photonic circuits, a process currently bottlenecked by costly electromagnetic simulations. My work, PIC-Flow, is a physics-based generative model that predicts full electromagnetic field solutions for silicon photonic devices in milliseconds, up to 50× faster than leading open-source solvers, and lays the foundation for tools that generate, simulate, and optimize entire photonic chips autonomously, collapsing design cycles from months to minutes.

Publication: https://arxiv.org/abs/2605.06929

2nd Prize: Elisaveta (Lisa) Samoylov (Computer Science) Advisor: Soroush Vosoughi

Representing Lean Proofs as Trajectories in Latent Space

AI increasingly automates proof-writing in Lean, used by mathematicians for interactive theorem proving. Existing models embed each step by surface syntax, ignoring what defines proof steps: the change they induce in the proof state. We train a Transformer to embed steps by their symbolic effect, viewing proofs as trajectories through this learned space. Across 13,500 LeanWorkbook proofs, our representation beats a syntax baseline on next-tactic retrieval; longer proofs wind circuitously through similar regions rather than traveling farther. Five proof styles emerge as geometric signatures, enabling provers to recognize what kind of proof they're writing.

3rd Prize: Manzi Fabrice Niyigaba (Computer Science) Advisor: Yujun Yan

SAGE: A Synthetic Graph Framework for Personalized Student Knowledge-State Modeling

How many questions does it take to infer what a student knows, and can we minimize that? We introduce SAGE, the first framework to formalize student assessment as a Bayesian sequential decision problem over a knowledge graph extracted directly from educational materials. SAGE adaptively selects questions that maximize information gain, updates Bayesian beliefs over concept mastery from each response, and propagates these beliefs across the graph to infer mastery on related concepts never directly tested. As a result, a student’s full knowledge state can be recovered from a few well-selected questions, significantly outperforming previous baselines. This brings us closer to scalable personalized assessment and precision education.