用代码结构生成数学形式化语句，提升大模型自动形式化能力。
TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition
- 将代码分解为文档、主函数和依赖函数，构建类数学形式化结构。
- 在多个数学推理基准上显著提升模型表现，最高增益达68.82%。
- 无需新增数学知识，即可让现有模型更好理解形式化数学命题。
大型语言模型在非正式与形式化（如 Lean 4）数学推理方面表现优异，但在将非正式数学表述转化为形式化陈述的自动形式化任务上仍存在困难。当前数学大模型性能受限于大规模非正式-形式化语句对数据集的稀缺性。有趣的是，自动形式化所用的形式语言与编程语言在结构上具有相似性，而代码数据规模庞大。然而，现有基于代码训练的模型难以有效迁移至形式化数学，原因在于两者在结构和语法上的差异。为此，我们提出 TopoAlign 框架，将广泛可用的代码仓库转化为数学大模型的训练资源。TopoAlign 将代码分解为文档字符串、主函数和依赖函数，并重构为在结构上类比形式化陈述的组件。我们在 DeepSeek-Math、Qwen-3 和 Herald 三个前沿模型上进行训练，并在 MiniF2F、Putnam 与 ProofNet 基准上评估。结果表明，TopoAlign 显著提升了 DeepSeek-Math 的表现，在 BEq@10 上提升 17.77%，在 typecheck@10 上提升 68.82%；同时对 Herald 也带来可测量的改进，分别提升 0.12% 和 1.09%，且未引入任何新的数学知识。
原文摘要 · Abstract (English)
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. 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. Interestingly, the formal languages used in autoformalisation share structural similarities with programming languages, and code data is available at scale. However, current models trained on code do not transfer effectively to formal math, due to structural and syntactic differences between them. To address this, 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. We train three state-of-the-art models, DeepSeek-Math, Qwen-3 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, and also measurably improves Herald by 0.12% on BEq@10 and 1.09% on typecheck@10 despite introducing no new mathematical knowledge.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。