Collaborative Research: AIMing: Synergy of Machine Learning and Automated Reasoning to Solve Math Challenges

This project will explore new ways to address complex mathematical problems by integrating advanced machine learning techniques with automated reasoning. By combining artificial intelligence with formal mathematical methods, the research team will advance the knowledge of some long-standing open problems in mathematics and computer science. These disciplines are crucial for the development of technologies that ensure software reliability, security, and efficiency --- key aspects in the digital age. The project not only supports the exploration of theoretical knowledge but also the practical application of these new algorithms to improve the tools that are integral to the technological infrastructure. The project will support two students, a mathematician and a computer scientist, who will closely work together to achieve the proposed goals. In technical terms, the project will use three specific open problems within graph theory and combinatorics as test cases to evaluate the effectiveness of new algorithms. The first objective will involve applying machine learning to develop efficient symmetry-breaking clauses to determine the values of small Ramsey numbers. Secondly, transformer-based methods will be used to generate small Folkman graphs. Lastly, the project will tackle a realizability problem related to point sets in a plane, aiming to understand and create configurations with larger than previously known planar discrepancies. This project will be a collaboration between mathematicians and computer scientists aiming to explore the synergy between machine learning and SAT solvers. The research team will improve methods for addressing these difficult problems, potentially obtaining both theoretical insights and novel computational techniques in mathematical and computational sciences. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.