Madeline Bumpus
MIT Department: Aeronautics and Astronautics
Faculty Mentor: Prof. Chuchu Fan
Research Supervisors: Kunal Garg, Yilun Hao
Undergraduate Institution: Howard University
Hometown: Toledo, Ohio
Website: LinkedIn
Biography
Madeline Bumpus is a senior at Howard University pursuing a bachelor’s degree in Computer Science with a minor in Mathematics. Currently, she works in the REliable Autonomous Systems Lab at MIT (REALM) under Dr. Chuchu Fan researching autonomous planning. Her previous work on Voronoi diagrams in the Hilbert metric resulted in a publication in the 2023 Canadian Conference on Computational Geometry. She is a proud Karsh STEM Scholar and is passionate about introducing our next generation to STEM. Madeline also serves as the president of her university’s math club. In her free time, she enjoys music, weightlifting, and playing rugby. She intends to pursue a Ph.D. in Computer science or Artificial Intelligence and Decision Making.
Abstract
Optimizing Cooperative Strategies in Overcooked: A Formal Approach Using Foundation Models
Madeline Bumpus1, Yilun Hao2, Chuchu Fan2
1Department of Electrical Engineering and Computer Science, Howard University
2Department of Aeronautics and Astronautics, Massachusetts Institute of Technology
This project applies formal verification techniques, specifically satisfiability modulo theory (SMT), to the cooperative cooking game “Overcooked” to optimize task management and strategy in dynamic environments. Overcooked provides a challenging, real-time setting that mimics operational issues seen in multi-agent systems, making it an ideal testbed for advanced AI strategies. This project pioneers the integration of formal methods to enhance in-game decision-making processes, which has implications beyond gaming, potentially improving AI behaviors in similar real-world scenarios such as robotics, autonomous vehicles, and logistics. By leveraging SMT to solve these models, the project ensures strategies are not only theoretically sound but also practically viable because SMT solvers are designed to ensure satisfiability. This approach fills a significant gap in research on dynamic interactive systems, where traditional heuristic methods fall short, offering a robust toolset for sophisticated decision-making processes in various applications, ultimately advancing the field of AI and multi-agent systems.
