SCML: A Publishing Forum for
Symbolic Computation and
Machine Learning

Abstract: Autoformalization, translating informal mathematical text into formal machine-checkable code, has recently attracted new interest thanks to advances in large language models. However, progress has been hindered by the lack of high-quality parallel corpora pairing natural language with formal code, especially for less widely used systems such as Agda. In this work, we address this gap by demonstrating a systematic data generation pipeline via the Informath project based on Grammatical Framework on the informal side and Dedukti on the formal side. Using this method, we construct a 400K “4-to-3” parallel corpus spanning four formal languages (Dedukti, Agda, Rocq, Lean) and three natural languages (English, French, Swedish). To validate the utility of the approach, we fine-tune the open-source Qwen2.5-7B-Instruct model and achieve substantial gains: BLEU-4 improves from 32.90 to 76.16, and Agda syntax error rate falls from 98.43% to under 8%. We further explore joint training across multiple formal and natural languages, demonstrating that multilingual and multi-formal regimes yield notable improvements in low-resource scenarios. Our work establishes an easily extensible multilingual autoformalization system and a test dataset with hand-written theorem statements paired with Agda, Dedukti, Lean, and Rocq. We will also propose some systematic insights into dataset construction and multilingual training for future research.