Unspoken Logic: Understanding and bridging the gap between free-form and LLM-interpretable natural language mathematical proofs

Autoformalization, the translation of natural language into formal language, is challenging for many reasons. One key issue is that humans express logic in a rich and diverse set of ways, and autoformalization of a mathematical proof can fail even if the proof is rigorous from the perspective of other humans. To have AI tools for mathematics be widely accessible, it is important that autoformalization systems be able to accept a wide range of input. In this work, we examine the misalignment between free-form human natural language and the language best suited for autoformalization. We analyze fully-correct student-written proofs to identify recurring sources of ambiguity that hinder formalization, and we develop a natural language pre-processing system that converts free-form math proofs into a form that leads to more correct autoformalizations. We evaluate this system to identify the ambiguities the translator can and cannot resolve.