Framework Leverages Code Repositories to Train Better AI Models for Mathematical Formalization

Large language models show promise in both informal reasoning and formal mathematical proof systems like Lean 4, yet they struggle to perform autoformalisation—the translation of human-readable mathematics into machine-verifiable formal statements. A key constraint is the shortage of paired datasets containing both informal and formal versions of the same mathematical content.

Bridging Code and Math#

Researchers at arXiv have identified an opportunity: formal mathematical languages share structural patterns with programming languages, and code repositories exist at massive scale. The challenge is that current models trained on code don't generalize well to formal mathematics due to syntactic and architectural differences between the two domains.

To solve this mismatch, a team introduced TopoAlign, a framework that repurposes code as training data for mathematical reasoning models. The approach breaks down source code into three components—docstrings, main functions, and dependency functions—then reconstructs these pieces into arrangements that structurally resemble formal mathematical statements. This transformation allows models to learn patterns relevant to mathematical formalization without requiring new math-specific corpora.

Performance Improvements#

The researchers trained three established models using TopoAlign: DeepSeek-Math, Qwen-3, and Herald. Testing on standard mathematical benchmarks (MiniF2F, Putnam, and ProofNet) showed measurable gains. DeepSeek-Math saw particularly strong improvements: 17.77% on BEq@10 and 68.82% on typecheck@10 metrics. Herald also benefited, with smaller but meaningful gains of 0.12% on BEq@10 and 1.09% on typecheck@10.

Notably, these improvements came without introducing any additional mathematical knowledge into the training process—the framework simply restructured existing data to make underlying patterns more accessible to the models.