Columbia Engineering’s Class of 2023 showcased their inventive solutions to challenging problems at the 8th annual Senior Design Expo. Projects varied from an approach that aims to reinvent IV (intravenous) administration for NICU patients to a novel capture system to remove space debris. More than 50 teams spanning eight departments presented their innovations and research at a packed showcase held May 4 at Roone Arledge Auditorium to a crowd of peers, professors, alumni, and STEM enthusiasts.

The biomedical engineering team behind NuJet (Anjali Nair, Isa Nuñez, Athena Pagon, Vish Rao, Elías Tzoc-Pacheo), attempted to solve the need for a cost-effective vaccine delivery to make vaccines more accessible, sustainable, and sanitary. 

“Syringes and needles are the most common form of vaccine delivery, despite many of the components being single-use,” said Pagon. 

On top of this, there are strict storage, transportation and disposal requirements, leading to a high-cost model that is typically only accessible in high resource centers. Their solution, a low-cost needle-less injector, generates a pressurized fluid stream that delivers the vaccine right below the skin while reducing cross-contamination, waste, and cost.

Inspired by individuals who suffer from overstimulation and anxiety, the electrical engineering students behind Musical Meditation (Tess Fallon, Alexandr Petuhov, Leonardo Arvan, Madeline Denis) developed a pair of headphones that reads the user's heart rate, while playing calming music that adjusts itself in an attempt to slow down the person’s heartbeat. 

Some designs focused on improving existing solutions. AMPF, also known as the Automated Pothole Filler (Jose Chanchavac, Phillipe Dumeny, Javier Lopez, Jerry Qu, Justin Tucker) aimed to simplify the process of filling potholes, which typically requires work from a large team of workers, typically five to 10 people at a time. “Our solution greatly reduces the number of people needed to about one to two workers,” said Javier Lopez, who recently received a degree in mechanical engineering. While AMPF focused on earthly solutions, DEMI (Miles Huntley-Fenner, Christina Wrightm Yidi Reiss, Leon Aharonian, Nicolas Aldana) focused on safely securing space debris, also known as space junk, which poses a serious threat to the welfare and sustainability of orbital activities. Their two-stage capture system encloses the debris and seals it in a storage chamber, which is something that other solutions lack.

Image

Sustainability was a common theme among many projects, with the expectation of improving systems that currently affect the environment. AQUA4 (Anton Deti, Emily Milian, Itai Savin, Kennedi Wade) developed a water rerouting system that repurposes water used in the bathroom. Students from the Department of Earth and Environmental Engineering researched how best to treat contaminated soil in New York City, with hopes to rid the soil of harmful metals such as lead and arsenic (Mantjita Camara, Emily Lord, Dane Miller). 

Many civil engineering models were built this year with sustainability in mind, from re-designing Dam systems to better serve the flora and fauna of the surrounding area (Ruben Bazalar, Caroline Cailloux, Kevin Cardenas, Yunus Kovankaya, Zhihao Liu, Ariana Novo) to cost-effective Brooklyn housing made entirely of recycled shipping containers (Charlie Henry Renner, Abraham Oh, Katherine Koziol, Amin Mojarad, Isabella Citera, Tes S DeJaeger). 

Other visionary projects aimed to improve skills, through games and physical exercise. With focus on creativity, the students behind ZyloZinger (Sienna Brent, Alex Yu, Haris Zia) created an interactive xylophone game that challenges hand-eye coordination. In an effort to improve athletic training, Deadliftr (Yelaman Sain, Kyrie Lorfing, Matt Klenk, Sam Wustefeld, Will Hamilton) aimed to develop a device to help weightlifters on their deadlift training, creating a wireless device that gives athletes real-time feedback on their form. 

Image

“I feel inspired and energized by all of the inventive projects on display here today and I know the rest of you feel the same,” said Dean Shih-Fu Chang in his address preceding the event. “It truly shows how creative our field of engineering and applied science is and our commitment to being engineers for humanity.” 

Recent work directed by professors Ronghui Gu and Jason Nieh introduced a new tool, Spoq, that significantly reduces the complex efforts people must use to verify real-world software and makes it possible to verify existing C systems code without modifications. Formal verification offers a systematic and rigorous approach to software and hardware verification, helping to ensure that systems behave correctly and meet their intended specifications. With Spoq, many aspects of formal verification can be automated, significantly reducing manual proof efforts for verification. The paper was presented at the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference on July 12, 2023.

Why it matters

System software forms the software foundations of our computing infrastructure. Modern system software is large, complex, and imperfect, with vulnerabilities that can be exploited to compromise the security of a system. Formal verification offers a potential solution to this problem by mathematically proving that system software can provide critical security guarantees. Unfortunately, it remains too difficult and requires too much human effort to apply in practice.

Previous tools developed by Nieh’s and Gu’s teams introduced verification techniques to make certain proofs possible that could not have been done before. Spoq’s key feature is that it automates the tedious and time-consuming parts of many proofs. “Spoq can generate results in about an hour compared to doing it manually, which can take months or years to formally verify a system,” says Xupeng Li, the paper's lead author and a PhD student with both Nieh and Gu.

What's next

Over the next few months, the lab is focused on making Spoq open-source so that formal verification can be widely deployed to secure the foundations of our computing infrastructure's software.

About the Study

Conference: 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference (July 10-12, 2023, Boston, MA)

Title: “Spoq: Scaling Machine-Checkable Systems Verification in Coq”

Authors: Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh, Columbia Engineering

Funding: This work was supported in part by three Amazon Research Awards, a Guggenheim Fellowship, a VMware Systems Research Award, an NSF CAREER Award, DARPA contract N66001-21-C-4018, and NSF grants CCF-1918400, CNS-2052947, and CCF-2124080. 

COI: Ronghui Gu is the founder of and has an equity interest in CertiK.

Header image: Tang Family Assistant Professor of Computer Science Rongui Gu (left) and Professor of Computer Science Jason Nieh (right).

Over time, the AI system, which the team designed by modifying a state-of-the-art framework, got better at telling when seemingly unique fingerprints belonged to the same person and when they didn’t. The accuracy for a single pair reached 77%. When multiple pairs were presented, the accuracy shot significantly higher, potentially increasing current forensic efficiency by more than tenfold. The project, a collaboration between Hod Lipson’s Creative Machines lab at Columbia Engineering and Wenyao Xu’s Embedded Sensors and Computing lab at University at Buffalo, SUNY, was published today in Science Advances.

Study findings challenge–and surprise–forensics community

Once the team verified their results, they quickly sent the findings to a well-established forensics journal, only to receive a rejection a few months later. The anonymous expert reviewer and editor concluded that “It is well known that every fingerprint is unique,” and therefore it would not be possible to detect similarities even if the fingerprints came from the same person. 

The team did not give up. They doubled down on the lead, fed their AI system even more data, and the system kept improving. Aware of the forensics community's skepticism, the team opted to submit their manuscript to a more general audience. The paper was rejected again, but Lipson, who is the James and Sally Scapa Professor of Innovation in the Department of Mechanical Engineering and co-director of the Makerspace Facility, appealed. “I don’t normally argue editorial decisions, but this finding was too important to ignore,” he said. “If this information tips the balance, then I imagine that cold cases could be revived, and even that innocent people could be acquitted.” 

While the system’s accuracy is not sufficient to officially decide a case, it can help prioritize leads in ambiguous situations. After more back and forth, the paper was finally accepted for publication by Science Advances.

Unveiled: a new kind of forensic marker to precisely capture fingerprints

One of the sticking points was the following question: What alternative information was the AI actually using that has evaded decades of forensic analysis? After careful visualizations of the AI system’s decision process, the team concluded that the AI was using a new kind of forensic marker. 

“The AI was not using ‘minutiae,’ which are the branchings and endpoints in fingerprint ridges – the patterns used in traditional fingerprint comparison,” said Guo, who began the study as a first-year student at Columbia Engineering in 2021. “Instead, it was using something else, related to the angles and curvatures of the swirls and loops in the center of the fingerprint.” 

Columbia Engineering senior Aniv Ray and PhD student Judah Goldfeder, who helped analyze the data, noted that their results are just the beginning. “Just imagine how well this will perform once it’s trained on millions, instead of thousands of fingerprints,” said Ray.

A need for broader datasets

The team is aware of potential biases in the data. The authors present evidence that indicates that the AI performs similarly across genders and races, where samples were available. However, they note, more careful validation needs to be done using datasets with broader coverage if this technique is to be used in practice.

Transformative potential of AI in a well-established field

This discovery is an example of more surprising things to come from AI, notes Lipson. “Many people think that AI cannot really make new discoveries–that it just regurgitates knowledge,” he said. “But this research is an example of how even a fairly simple AI, given a fairly plain dataset that the research community has had lying around for years, can provide insights that have eluded experts for decades.” 

He added, “Even more exciting is the fact that an undergraduate student, with no background in forensics whatsoever, can use AI to successfully challenge a widely held belief of an entire field. We are about to experience an explosion of AI-led scientific discovery by non-experts, and the expert community, including academia, needs to get ready.”

About the Study

Journal: Science Advances

Title: Unveiling Intra-Person Fingerprint Similarity via Deep Contrastive Learning

Authors: Gabe Guo, Aniv Ray, Judah Goldfeder, and Hod Lipson, Columbia Engineering; Miles Izydorczak, Tufts University; and Wenyao Xu, University at Buffalo, SUNY.

The work is part of a joint University of Washington, Columbia, and Harvard NSF AI Institute for Dynamical Systems, aimed to accelerate scientific discovery using AI.

Funding: The study was supported by NSF AI Institute for Dynamical Systems 2112085, and NSF REU Site 2050910.

COI: The authors declare no financial or other conflicts of interest.

Blockchains and the applications they support raise new challenges for economics, computer science, and game theory.

At the 2023 Columbia CryptoEconomics (CCE) Workshop, held December 6-7, practitioners, researchers, and academics gathered at the University’s Manhattanville campus to discuss challenges, recent progress, and opportunities in the economics of blockchain protocols. In keynote presentations, contributed talks, and panel discussions, leading experts discussed topics including proposer-builder separation, MEV, layer 1 security rehypothecation/restaking, and roll-ups.

The workshop, which was co-hosted by the Briger Family Digital Finance Lab at Columbia Business School, Columbia Engineering, and the Ethereum Foundation, underscored Columbia’s commitment to interdisciplinary research that seeks impact beyond the walls of the University. 

“We advocate for the convergent collaboration among academics, practitioners, and industry,” said Shih-Fu Chang, dean of Columbia Engineering and Morris A. and Alma Schapiro Professor of Engineering, in his opening remarks. 

“As interest in the crypto space waxes and wanes, support at various universities has come and gone,” said co-organizer Tim Roughgarden, professor of computer science at Columbia Engineering and the head of research at a16z Crypto. “Columbia has been fairly unique among its peer institutions by having unflagging support for the advancement of this technology and the science behind it.”

Details about the event and a full lineup are available here.

Full recordings of all sessions are available here.