Collaborative Research: AIMING: AI Tools to Knowledge Discovery and Rigorous Reasoning in Polyhedral Geometry

The project aims to develop innovative artificial intelligence (AI) tools to study polyhedra, which are fundamental in various fields such as combinatorics, discrete geometry, and optimization. The complexity of polytopes makes it challenging for researchers to gain insights and draw connections between their structures and properties. This project addresses this challenge by leveraging AI to enhance mathematicians' abilities to generate polyhedral samples, discover new conjectures, and conduct rigorous reasoning on polyhedral geometry. This research is significant as it not only advances the mathematical field, but these innovations are expected to significantly advance the understanding and application of polyhedral geometry in various scientific and engineering domains, as well as advance the potential of AI for mathematical reasoning. The project also supports education by creating tools that can be used in teaching. Additionally, the project promotes diversity and inclusivity in STEM by engaging underrepresented groups through workshops and mentoring programs, thereby inspiring a broader range of students to pursue careers in these fields. The technical scope of the project includes developing new methods for data generation, knowledge discovery, and formal reasoning in polyhedral geometry. The project will use AI techniques such as diffusion methods and reinforcement learning to create diverse, high-quality polyhedral samples. A key innovation is the development of Polyhedral-GPT, which integrates large language models to provide clear, interpretable outputs using a polyhedral transformer. The project also aims to enhance computational efficiency by combining fast, informal AI techniques with rigorous formal verification. Additionally, a black-box interpreter will automate the translation of polyhedral knowledge into natural language, minimizing human intervention and streamlining the process from conjecture generation to formal proof verification. The integration of optimization, algebraic geometry, and SAT solvers will further facilitate automatic proof processes, contributing to the project's overall efficiency and accuracy. 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.