Abstract
Large Language Models (LLMs) excel at both informal and formal (e.g. Lean 4) mathematical reasoning but still struggle with autoformalisation, the task of transforming informal into formal mathematical statements. Autoformalisation helps pair the informal reasoning of LLMs with formal proof assistants which enable machine-verifiable generation and mitigate hallucinations. Yet, the performance of current Math LLMs is constrained by the scarcity of large-scale corpora, particularly those containing pairs of informal and formal statements. Although current models are trained to generate code from natural language instructions, structural and syntactic differences between these and formal mathematics limit effective transfer learning. We propose TopoAlign, a framework that unlocks widely available code repositories as training resources for Math LLMs. TopoAlign decomposes code into docstrings, main functions, and dependency functions, and reassembles these components into analogues that structurally mirror formal statements. This produces structurally aligned code data that can be used for training Math LLMs without requiring additional human annotation. We train two state-of-the-art models, DeepSeek-Math and Herald, and evaluate them on the minif2f, Putnam, and ProofNet benchmarks. TopoAlign provides substantial gains for DeepSeek-Math, improving performance by 17.77% on BEq@10 and 68.82% on typecheck@10. Despite introducing no new mathematical knowledge, our framework achieves gains of 0.12% and 1.09% for Herald on BEq@10 and typecheck@10, respectively, demonstrating that training on aligned code data is beneficial even for specialized models.
Abstract (translated)
大型语言模型（LLMs）在非正式和正式数学推理（如Lean 4）方面表现出色，但它们仍然在自动形式化任务上遇到困难。自动形式化的目的是将非正式的数学陈述转换为正式的数学表述，这一过程有助于将LLM的非正式推理与证明辅助工具相匹配，从而实现机器可验证的生成并减少幻觉（错误信息）。然而，当前数学模型的表现受限于大规模语料库的稀缺性，尤其是包含非正式和正式声明配对的语料库。尽管现有的模型被训练从自然语言指令生成代码，但这些语言与正式数学之间的结构和语法差异限制了有效的迁移学习。 我们提出了一个名为TopoAlign的框架，该框架解锁了广泛可用的代码仓库作为数学LLM的培训资源。TopoAlign将代码分解为文档字符串、主函数和依赖函数，并重新组合成类似于正式声明的结构镜像体，从而生成可以用于训练数学模型且无需额外人工注释的结构对齐代码数据。 我们使用两个最先进的模型——DeepSeek-Math和Herald，在minif2f、Putnam和ProofNet基准测试上进行实验。TopoAlign框架为DeepSeek-Math带来了显著改善，在BEq@10上的性能提升了17.77%，在typecheck@10上的性能提高了68.82%。尽管我们的框架并未引入新的数学知识，但仍然使得Herald模型的BEq@10和typecheck@10分别获得了0.12%和1.09%的改进，这表明即使是专门化的模型也能够从对齐后的代码数据训练中受益。 该研究证明了通过结构化映射现有代码资源以适应数学LLM培训的有效性，并展示了利用这种资源改善模型性能的巨大潜力。
URL
https://arxiv.org/abs/2510.11944
