In the paper "Planting Undetectable Backdoors in Machine Learning Models" by Goldwasser et al (arXiv:2204:06974), the authors establish the notion of "black-box undetectability" for machine learning models and prove it in many cases. This is a backdoor that is undetectable by merely looking at inputs and outputs of the model. The paper also introduces the concept of "white-box undetectability."  We aim to consider this stronger notion and outline how even with the knowledge of entire model weights, there may be undetectable backdoors in a model. More specifically, we establish an idea where one takes an innocuous model (say a Multi-Layer-Perceptron model) and enlarges it by adding "dummy" edges and using appropriate non-linear activation functions to effectively place a backdoor in the model. In our project, we establish a proof of concept by backdooring an MNIST classifier.

Formalization is the process of translating human-written mathematical proofs into a form that can be verified by a computer. A popular tool for this is Lean, a proof assistant that represents proofs as code. However, the process of formalizing proofs in Lean can be slow and time-consuming. Our research explores so-called "autoformalization" strategies, which aim to automate the generation of Lean proofs. We propose a tree-based search framework to formalize mathematical theorems in Lean using Language Models. This approach explores potential proof steps as branches in a tree, using AI models to suggest "tactics" at each node. This has the benefit of avoiding hallucinations by rigorously checking that AI suggestion represent valid Lean code. We employ both Large Language Models such as Claude Sonnet 3.5 and specialized fine-tuned Small Language Models such as Lean-Dojo. We use Pantograph to interact with Lean, leveraging its native support of Monte Carlo tree search. We assemble a small set of simple and medium-difficulty mathematical theorems to benchmark against, called nanoF2F. Additionally, we benchmark our system on the well-established miniF2F benchmark created by OpenAI.

Determining the genus of a graph—the smallest surface on which it can be embedded without edge crossings—is a fundamental problem in graph theory with applications in circuit design, transportation networks, and data visualization. Existing genus computation methods often require extensive case-by-case analysis, and the problem is NP-hard in general. To address this, we developed and analyzed PAGE, a novel algorithm that efficiently determines a graph’s genus by enumerating non-backtracking closed directed trails and optimizing search iterations. We established an upper bound on its runtime as O(n(4m/n)^(n/t)) for graphs of girth t and implemented performance optimizations using hash sets for cycle tracking and adjacency list storage for rotation systems. We then conducted empirical comparisons against existing methods, including SAGEMath and MULTI_GENUS, demonstrating PAGE’s superior scalability, particularly for large 3-regular cage graphs. These results suggest PAGE’s potential to improve genus computation, contribute to open problems in topological graph theory, and enhance applications in fields requiring efficient graph embeddings.

In this project, we study the order polytopes of generalized snake posets, a particular family of polytopes (geometric shapes with flat sides) defined in recent work by von Bell and coauthors. We specifically investigate triangulations of these polytopes, which are subdivisions of the polytopes into simplicies (arbitrary-dimensional generalizations of the triangle). To do so we examine their secondary polytopes. The secondary polytope of a polytope is a related polytope in which each vertex corresponds to a triangulation of the original polytope and each edge corresponds to a bistellar flip (a specific type of transformation between triangulations), capturing the combinatorial relationships between different triangulations in a geometric object. Von Bell and coauthors conjecture that the secondary polytopes of order polytopes of snake posets have multiple unusually nice properties similar to those of the associahedra, a well-known family of polytopes that admit nice combinatorial descriptions and appear in many areas of mathematics. The overall goal of this project is to prove these conjectures. Collaborating with fellow undergraduates Molly Bradley (University of Pennsylvania), Mario Tomba (Dartmouth), and Katherine Tung (Harvard), I have written code to compute details of the smallest examples of these secondary polytopes, proved related theorems/results, proposed some new conjectures based on observed patterns in the examined examples, and made partial progress towards proving multiple of the von Bell conjectures. This project is ongoing, and we continue to explore multiple ways to approach the conjectures and more broadly understand the secondary polytopes.

In this work, we present two new geometric properties of ellipses that emerged while studying problems related to mass transportation. The first property states that if we shrink the ellipse proportionally and consider any tangent to the smaller ellipse, the two points where this tangent intersects the original ellipse always sum to the point of tangency. This reveals a fundamental symmetry in how ellipses scale and interact with their tangents. The second property describes a special set of interior points that arise by tracing how tangents from a fixed boundary point behave across a family of smaller ellipses. We prove that this set forms another ellipse, exactly half the size of the original, centered at the midpoint between the origin and the fixed boundary point. These findings offer new insights into classical geometry and may have potential applications for problems in mathematics and other fields. 

When carbon dioxide emissions are high within a room, short and long-term health effects on humans have been observed. Natural gas stoves are common household appliances that contribute to carbon dioxide emissions. The purpose of this study is to model how the burners of a natural gas stovetop may impact the air quality and potential health risks within households. I measured carbon dioxide emissions from a Samsung gas range with one to four burners on maximum heat in thirty-minute intervals using an Aranet4 Home sensor. The results were observed to have an overall increase in carbon dioxide emissions correlating to the number of burners being used concurrently. Carbon dioxide concentrations reached harmful levels within thirty minutes when two or more burners were used. Knowing how the rates of carbon dioxide concentrations within a room may increase in correlation to use of one, or multiple, burners would provide users of gas ranges with a reference point on how the air quality may change over time. This would allow for a better understanding of the risks associated with natural gas stovetop usage regarding the health impacts of close exposure to high carbon dioxide concentrations. Future analysis can be conducted on the different rates of carbon dioxide emissions for functions of natural gas ovens.

Ongoing research towards the realization of the future Solar System Internet (SSI) has demonstrated the potential for using Delay Tolerant Networks (DTN) to create a scalable communications network that overcomes routing complications found in outer space. At present, traditional time synchronization protocols do not scale well in outer space networks, and yet it is unavoidable that some level of time synchronization is required to ensure crucial network functionality (such as scheduled data transmission between nodes) is well supported. The result of this is a necessity to design and implement a scalable, automated time synchronization protocol within the DTN architecture. This presentation covers the development towards one such protocol initially proposed by Moy et. al in 2024. More specifically, we focus on subsequent simulation work with the goal of understanding how implementation details of the algorithm and ramifications of the SSI’s network architecture may affect the convergence behavior of clock times, such as those regarding parameter selection, clustering of nodes in a network, and contradictory setups due to inconsistent knowledge of the network topology between nodes. To address these conditions, we first review the protocol as proposed in 2024. Through simulation, we cover the potential effects of degrees of network clustering and of choosing underlying equation solvers for time convergence on simple network layouts. We conclude with an analysis of a simulation based on the network architecture of a recent DTN experiment campaign involving the International Space Station (ISS). Preliminary results suggest that the convergence of clock times can occur under the tested conditions using the proposed algorithm, but that the convergence behavior and the final “agreed upon” time may differ. These results and future works thereby inspired may be used to inform the scheduling and implementation of the clock synchronization protocol within the network architecture of the SSI.

Self-organized criticality is the concept that certain systems naturally evolve to a critical point where one more incremental addition will cause the whole system to shift or reorganize. It is thought that many natural phenomena such as earthquakes, avalanches, and wildfires exhibit and can be explained according to this. The probability of a certain size event (“avalanche”) occurring can be described using the power-law distribution. Our work focused on finding the parameterizing exponent of this distribution. To accomplish this, we created computer simulations of Activated Random Walk (ARW) a probabilistic model that exhibits self-organized criticality and has good potential for universality. By finding the critical exponent in the power-law distribution describing ARW stabilization, we advance the understanding of self-organized criticality and add to a body of research which may improve our ability to predict disastrous events and their effects.

In mathematics, a symmetry of an object is an invertible mapping from the object to itself. In classical geometry, symmetries are described by group actions. However, group actions are not enough to capture all of the symmetries of some objects. In particular, algebras have symmetries given by Hopf actions of quantum groups called quantum symmetries. In this project, we aim to classify the quantum symmetries of gentle algebras given by Hopf actions of generalized Taft algebras. Path algebras are algebras associated to a directed graph. All finite dimensional algebras can be understood as quotients of path algebras including gentle algebras. The directed graphs associated with gentle algebras can be obtained by gluing copies of particular directed graphs with 1-4 edges. Our approach is to start by classifying Taft actions on these smaller directed graphs. Then, we will determine how these actions glue together to give us Taft actions on any gentle algebra. There is a known parametrization of Taft actions on path algebras, and this project is a step in generalizing this to Taft actions on any finite dimensional algebra.

Tame knots, which are equivalent to a polygonal knot with a finite number of sides, have well-studied invariants; conversely, wild knots that exhibit infinite and pathological behavior are difficult to study and classify. Knot mosaics, introduced by Lomanoco and Kauffman, are an example of a complete invariant for tame knots. Our project aims to expand the existing formal system of knot mosaics to develop an invariant for wild knots. We define n-singular mosaic tangles, the mosaic analog of tangle insertions in pseudoknots and singular knots, and we formalize a system of infinite insertion that generates a wild mosaic to represent certain wild knots. We also intend to define wild mosaic equivalence moves to capture the notion of wild knot equivalence in the mosaic setting. This gives insight to many wild knots explored in existing literature and provides methods to generate and classify new examples.

The Tait graph, an undirected graph with signed edges derived from a knot diagram, is fundamental to knot theory and algebraic topology, enabling the study of knot invariants and topological properties. Despite its importance, widely-used software packages like SageMath and SnapPy lack native functionality for Tait graph construction and manipulation. Our research addresses this gap by presenting an efficient algorithm to construct the signed Tait graph and its associated dual graph from a knot's Planar Diagram Code (PD-Code). We validated our algorithm by comparing the reduced weighted Laplacian matrices of our constructed graphs with those of nearly 3,000 classified knots up to 12 crossings. Future work will extend our implementation to support additional functionalities such as Reidemeister moves, Jones polynomial calculations, and directed edge representations. By deploying our code on SageMath, we aim to provide a valuable tool for researchers in knot theory and related fields.