Dimitri Dimanidze ’23 — This summer, I worked as a research intern assisting professor McCartin-Lim. This was a life-changing experience for which I want to thank Wabash Career services, the Computer science department, and especially Professor McCartin-Lim.
The research was called “Machine learning for proofs”. During the first month of the internship, we explored different paths we could explore. Teaching a machine learning model to prove something or to check a proof is like a big puzzle and many researchers around the world work on solving one piece of it. Therefore, we were looking for a problem we wanted to solve. Throughout this month I read research papers and then discussed the ideas with the professor.
After a month of thinking and gathering tools and ideas, we settled on the task of teaching a transformer model to transform Boolean formulas into conjunctive normal form. The Transformer model is a state of art model in sequence-to-sequence NLP tasks, however, its potential with arithmetic or working with symbolic data has not been fully explored. our work serves as a kind of benchmark for the model, where we explore how well it performs and generalizes on formulas of different sizes. During the second month of the internship, I tinkered with a code of the Transformer model and ran experiments, gathering and discussing the results with the professor.
