Tyler Josephson, an assistant professor in the Department of Chemical, Biochemical, and Environmental Engineering at UMBC, has received an Amazon Research Award to improve the accuracy of scientific computing. The project, titled “Autoformalization for Scientific Computing in Lean,” aims to bridge the gap between complex scientific theories and the computer code used to simulate them.
In modern science, researchers use computer simulations to model everything from new medicines to climate change. However, these simulations often rely on code that is difficult to check for errors. If a mistake is made when translating a mathematical equation from a research paper into a computer program, it can lead to incorrect findings.
While "formal methods"—a type of high-level logic used to prove code is correct—are common in cybersecurity and hardware design, they are rarely used in general science because they are difficult and time-consuming for humans to learn and use to write code.
Tyler Josephson, second from right, works with students in the lab (Marlayna Demond '11/UMBC)
Josephson, who leads the AI and Theory-Oriented Molecular Science (ATOMS) Lab at UMBC, is developing a new AI system to help solve this. Using a specialized programming language called Lean, the team is building AI "agents" that can read scientific papers and automatically translate the math into formally verified code.
"We don't think humans will manually formalize a century of scientific theory without machine assistance," Josephson notes, highlighting the need for AI-human collaboration to scale these efforts.
The award provides almost $77,000, which Josephson plans to use to support student researchers on the project.
Ultimately, the tools could help researchers tackle challenges such as designing new materials for gas separation or speeding up drug discovery by providing a rock-solid foundation for digital experiments.