ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data
Authors: Xiaoyang Liu
Kangjie Bao
Jiashuo Zhang
Yunqi Liu
Yu Chen
Yuntian Liu
Yang Jiao
Tao Luo
Venue: NeurIPS 2025 poster ()
Keywords: Autoformalization
Formal Mathematics
Lean 4
Automated theorem proving
Dataset
Primary area: machine_learning_for_sciences

Abstract: Autoformalization, the automatic translation of mathematical content from natural language into machine-verifiable formal languages, has seen significant progress driven by advances in large language models (LLMs). Nonetheless, a primary barrier to further improvements is the limited availability of parallel corpora that map informal mathematical text to its formal counterpart. To address this limitation, we propose ATLAS (Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data), a novel data generation framework designed to produce large-scale, high-quality parallel corpora of theorem statements. Distinct from prior approaches, ATLAS begins with a concept repository, accelerates the improvement of the student model through expert iteration combined with knowledge distillation, and introduces two novel augmentation strategies that exploit the structural characteristics of formal languages. Running the proposed ATLAS framework for 10 iterations, we construct an undergraduate-level dataset of 117k theorem statements and develop the ATLAS Translator by fine-tuning Llama3.1-8B-Instruct with LoRA. This model establishes a new state of the art, demonstrating statistically significant improvements over both the Herald Translator and the Kimina-Autoformalizer across all benchmarks (p<0.05, two-sided t-test). Furthermore, we demonstrate that the full-parameter fine-tuning of a stronger base model on the ATLAS dataset leads to superior performance. The datasets, model, and code are available at https://github.com/XiaoyangLiu-sjtu/ATLAS.

ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data
Xiaoyang Liu', Kangjie Bao', Jiashuo Zhang', Yunqi Liu', Yu Chen',
Yuntian Liu', Yang Jiao Tao Luo
School of Mathematical Sciences, Shanghai Jiao Tong University
2 Institute of Natural Sciences, MOE-LSC, CMA-Shanghai, Shanghai Jiao Tong University
SPEIT, Shanghai Jiao Tong University
JoinTTech Co., Ltd (jiaoyang2002, luotao41]6sjaa eww.stt..du.coo edu. cn
Abstract
Autoformalization, the automatic translation of mathematical content from natural language into machine-verifiable formal languages, has seen significant progress driven by advances in large language models (LLMs). Nonetheless, primary barrier to further improvements is the limited availability of parallel corpora that map informal mathematical text to its formal counterpart. To address this limitation, we propose ATLAS (Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data), novel data generation framework designed to produce large-scale, high-quality parallel corpora of theorem statements. Distinct from prior approaches, ATLAS begins with concept repository, accelerates the improvement of the student model through expert iteration combined with knowledge distillation, and introduces two novel augmentation strategies that exploit the structural char- acteristics of formal languages. Rumning the proposed ATLAS framework for 10 iterations, we construct an undergraduate-leve dataset of 117k theorem statements and develop the ATLAS Translator by fine-tuning Llama3. 1-8B-Innsruee with LoRA. This model establishes a new state of the art, demonstrating statistically significant improvements over both the Herald Translator and the across all benchmarks (p < 0.05, two-sided t-test). Furthermore, we demonstrate that the full-parameter fine-tuning of stronger base model on the ATLAS dataset leads to superior performance. The datasets, model, and code are available at hittps://ght giggthu........ com wwt.//aaaaaaauuss/////aa.aa.
1 Introduction
In modern mathematics, the escalating complexity proofs, combined with the increasing reliance computer-assistee assisted arguments, has raised substantial concerns about reliability. Errors in traditional proofs can remain undetected for extended periods, while computer-assise lack transparency and are difficult to verify manually. thereby raising issues of trust within the mathematical community. For example, the Four Color Theorem's 1879 proof went unchallenged for over decade before its flaw was discovered. The first computer-assisted proof in 1976 raised concerns due to its unverifiable computations, prompting further debate. Only in 2005 was the proof formally verified using Coq 4. To address such issues, formal languages like Isabelle [29], HOL Light (10), Coq, and Lean 7 have been developed to rigorously verify the correctness of proofs.
proofs frequently
However, writing mathematical content in formal languages requires significant time and effort, as well as a deep familiarity with these languages, making the process highly ibbor-intensive. This
Corresponding authors: Yang Jiao, Tao Luo
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

highlights the critical importance of autoformalization, which aims to translate theorem statements and proofs from natural language (NL) into their formal language (FL) counterparts [44] Since
the precise formalization of statements can provide valuable training data for automated theorem proving [21], current research primarily focuses on the autoformalization of theorem statements. In this context, recent progress has shown encouraging results, primarily achieved by fine-tuning large language models (LLMs) with parallel corpora of theorem statements. For clarity, we hereafter refer to theorem statements expressed in natural language as NL statements, those expressed in formal language as FL statements, and their pairs as parallel statements. Furthermore, while ATLAS is a general framework for any formal language, this work focuses Lean 4 22 as the target language.
To construct parallel statements, previous studies such as MMA [ and Herald [9] extract FL statements from Mathlib [35] and generate their NL counterparts using LLMs. However, the limited size of Mathlib imposes restrictions on the scale of the resulting datasets. Alternative methods, including Lean Workbook [5]] and DeepSeek-Prowe Prover [46], attempt to generate FL. statements from NL sources obtained via large-scale web scraping- Although this approach greatly alleviates the limitations on dataset size, it requires extensive pre-processing to obtain high-quality, formalizable NL statements, which significantly reduces overall efficiency. Consequently, is essential to design a more effective method for generating large-scale, high-quality parallel statements.
In this work, we introduce ATLAS, a data generation framework composed of three key components: Data Lifting, Data Synthesis, and Data Augmentation.
Data Lifting. Unlike previous approaches, this work integrates FL statements and NL statements its starting point. Specifically, mathematical concepts abstracted and extracted directly from Mathlib to synthesize NL statements. This method not only overcomes scale limitations but also eliminates the need for data pre-processing.
Data Synthesis. Adopting the knowledge distillation [ paradigm, teacher models guide the student model's learning process, and the Lean compiler is jointly employed to ensure that the generated FL statements are both semantically accurate and syntactically valid. The resulting parallel statements are hereafter referred to "synthetic data".
Data Augmentation. The synthetic data are further expanded using two techniques: augmentation via proof and contraposition. The core idea is to leverage Lean 4's capability whereby the Infoview provides real-time updates of the current state after each proof step. The additional parallel statements generated are hereafter referred to "augmented data".
Finally, the synthetic and augmented data are combined to fine-tune the student model. The expert iteration 3D, 31 approach then employed to iteratively execute ATLAS. After 10 iterations, we build an undergraduate-leve dataset comprising 177k parallel statements and train the ATLAS Translator. The performance of the ATLAS Translator shows statistically significant improvements over both the Herald Translator and the Autofo-Autoformaliize across all benchmarks.
Our main contributions are follows:
1. We propose ATLAS, novel framework for generating large-scale, high-quality parallel statements. Unlike previous work that starts from NL statements or FL statements, our innovative approach begins by extracting concepts directly from Mathlib through process we call Data Lifting. Based on these concepts, we employ Data Synthesis and Data Augmentation synthesize and augment the parallel statements.
2. We introduce the ATLAS dataset and the MathQual dataset. The former comprises 117k undergraduate-leve parallel statements, making it one of the largest available. In contrast, the latter contains 465 graduate-level natural language statements, designed to assess the model's autoformalization capability more challenging data.
3. We develop the ATLAS Translator, which establishes new state of the art by demonstrating statistically significant improvements over strong baselines across all benchmarks (p < 0.05, two-sided t-test). Furthermore, we demonstrate that the full full-parameter fine-tuning of stronger base model on the ATLAS dataset leads to superior performance.

---

Fine-tuning
(a) Litting
(b) Synthesis
Theeem norpoct about CONGHAAA,
ATIAR
Fierist Stngte derielee aest anatysts
Comminnity
toestic: resting
Den/ carppet.
Mathill
Concept Repository
Concapts
Teacher Model
NL Statement
Student Model
Next Iteration
Re-Compilo
nemenn -
(c) Data Augmantation
PrN
Q
Statement
X
Teacher Model
K
Proof
ATLAS Dataset
Lean Complier
Teacher Model
Contraposition
Figure I: The overview of the proposed ATLAS framework.
Related Work
The task of autoformalization be machine translation problem [39. aiming to convert natural language content into expressions consistent with the target formal language's syntax and vocabulary. Early approaches 6 40) have utilized neural machine translation techniques to address the autoformalization of theorem statements. With the rapid advancement of L.LMs, recent research I.LM-based autoformalization
Autoformalization.
be broadly categorized into three 43 58 have explored few-shot prompting to enable LLMs to perform autoformalization effectively. Second, some methods 2 25 26 further enhance performance by fine-tuning LLMs with parallel statements. Finally, retrieval-augmentt -ugmented generation techniques achieve additional improvements.
main paradigms. First, researchers [1]
have been combined with LLMs
Meanwhile, another line of research focuses on the autoformalization of proofs [6 55 a more
challenging task that closely resembles simplified form of automated theorem proving 3 19 32
38
48). For example, DSP [16] leverages LLMS to generate informal proofs, which are subsequently mapped to formal proof sketches. These sketches then as guidance for automated theorem provers to fill in the remaining proof gaps.
Dataset Generation. Obtaining large-scale, high-quality parallel corpora of theorem statements remains significant challenge. Previous efforts 9
have tackled this problem by extracting FL statements from relevant repositories (e.g., Mathlib) and using L.Mss to generate their NL counterparts. However, the limited size of these repositories constrains the scalability of the resulting datasets. On the other hand, some approaches [18 46 [1] take the opposite direction by collecting NL statements from large-scale web sources and translating them into FL representations. While this strategy enables the creation of large-scale datasets, these web-based pipelines rely on extensive preprocessing to filter high-quality, formalizable NL statements, thereby diminishing overall efficiency.
15 45
Methodology
Our framework ATLAS, illustrated in Figure [ comprises three components: Data Lifting, Data Synthesis, and Data Augmentation. The framework begins with data lifting, which constructs the concept repository, described in Section 3.11 Building this foundation, Section 332 details the subsequent data synthesis workflow. Finally, Section 3.3 explains our approach to data augmentation.
3.1 Data Lifting
the most extensive mathematical library within the Lean community, provides a vast collection of formalized notations (e.g.. ||:|]), concepts, and theorems. This wealth of resources forms the cornerstone of autoformalization. Consequently, importing Mathlib practically essential before translating NL statement into FL statement.
Mathlib. Mathlib 35

---

Pre-Process Free
Workflow
Typical Work
Scalability
Correctness
NL
HERALD
X
Communic
Mathill
NL
FL
Lean Workbook
?
Internet
Corpus
FL
ATLAS
?
Communty
Mathilb
Concept
Repository
Lifting
Figure 2: Comparison of different methods for constructing parallel statements.
However, the reliance on Mathlib reveals a critical limitation: when NL statements involve mathe- matical concepts absent in Mathlib, such as subgradients, the autoformalization process is prone to failure. This issue has affected prior work that begins by collecting NL statements. For example, Lean Workbook uses LLMs categorize 458,692 NL statements and selects 327,870 based this classification, primarily aiming to exclude NI. statements involving concepts not present in Mathlib. In contrast, extracting FL statements from Mathlib does face this challenge, but the library's size constrains the scalability of the resulting datasets.
In contrast to previous work, proposed method takes novel approach by beginning with the extraction of concepts directly from Mathlib through a process we refer to as Data Lifting, By utilizing these concepts, we employ LLMs synthesize NL statements. As shown in Figure 2 this starting point eliminates the need for pre- pre-processing while ensuring scalability.
Correctness. For synthetic data, an important consideration is the correctness of the mathematical propositions themselves. However, in the context of autoformalization, the correctness of the mathematical proposition secondary, or even insignificant. What critical in this synthetic process is that the formalized statement is not only syntactically valid but also semantically equivalent to its natural language counterpart. This perspective stems from the primary objective of autoformalization and reflects the realities of mathematical practice, as the correctness of propositions conjectures seldom known priori. Therefore, prior to formal verification, propositions must be precisely formalized in formal language even if they ultimately turn out to be incorrect.
For example, the following example from the Lean Workbook illustrates that, although the NL statement itself is incorrect (due to the lack of a declaration for the scope of b, c). the FL statement semantically equivalent the NL statement and syntactically valid. Therefore, this constitutes a valuable piece of synthetic data. We further explore the limitations about correctness in Appendix
lean workbook plus 62 3(abb 6 daa) I (ab be + ca)² 5
theorem
lean workbook Satook_pluu__ee
plus_62 Vab R, (a
b a) - A (a b
2 c
(a by sorry
a)
In the subsequent experimental section, we construct the concept repository based on undergraduate- level mathematical content included in Mathlib. Following Mathlib's 's organization by domain, topic, and concept, our concept repository comprises domains, topies, and 350 concepts. Further details regarding the composition of the concept repository are provided in Appendix

---

3.2 Data Synthesis
Upon establishing the concept repository, the module is dedicated producing substantial number of high-quality parallel statements by means of knowledge distillation. The following subsections provide detailed description of each phase, with the specific prompts provided in Appendix F
NL Statements Generation. In this context, the teacher model serves the role of NL Statements Generation (NL--Gen) by randomly sampling concepts from the constructed concept repository to synthesize NL statements. To balance diversity and feasibility, we follow previous approaches
14 33 by sampling two concepts for each NL. statement and the detailed comparisons against MUSTARD [44 are provided in Appendix A This choice is motivated by the observation that using only a single concept often leads the LLM to generate NL statements that are biased toward well-known, classic mathematical propositions, thus limiting diversity. Conversely, requiring each NL statement to involve many distinct concepts would be overly restrictive, as such problems are uncommon in mathematics and may exceed the capabilities of LLMs.
NL Statements Translation. For the synthetic NL statements described above, we employ the student model to translate them into the corresponding FL statements, thereby enabling subsequent tests of syntactic validity and semantic accuracy to ensure the quality of the parallel statements.
FL Statements Parsing. Before conducting syntactic validity test on these FL statements, we use the tactic #check to decompose each FL statement into the following four components: cheorem_name, name, theorem_ theorem_variables, variables, content is then systematically organized line by line, both within and across these components.
soorre__hyoohesees and ceeeorem_concluse
The
Compared to presenting the entire content on single line, this line-by-line configuration, especially for statements with substantial content, significantly enhances the clarity of compiler feedback. In particular, error locations become much more explicit, enabling LLMs more effectively identify and correct errors in FL statements that fail to compile.
FL Statements Compilation. In this phase, the Lean compiler is employed to verify the syntactic validity of FL statements by determining whether they can be compiled successfully. If compilation fails, detailed error messages are returned, specifying the location and cause the error, thereby enabling more efficient subsequent revision. In addition, the student model is unable generate headers, a standard header, import Mathlib, is automatically appended prior to compilation.
FL Statements Revision. For FL statements that fail to compile, we utilize the corresponding NL statements and compilation error messages as context, providing this information to the teacher model serving as FL Statements Revision (FL-Rev) for modification. The modified FL statements then subjected to a second round of compilation.
Unlike conventional knowledge distillation, the teacher model in our approach is tasked with revising the FL statements generated by the student model based on the provided error messages, rather than generating FL statements directly. There are two primary reasons for this design. First, it is generally much easier to revise existing FL statements than to construct them anew; consequently, this strategy is more likely to produce syntactically valid FL statements after modification. Second, as the performance of the student model improves through iterative learning, the need for FL-Rev diminishes, thus maintaining the efficiency of the overall framework.
FL Statements Alignment. For FL statements that pass either the first or second compilation, the teacher model acting as the FL Statements Aligmment (FL-Align) evaluator assesses their semantic accuracy in translating the corresponding NL statement, ensuring no information is omitted or mistranslated. Specifically, the model assesses each pair of parallel statements and assigns a rating from three categories: good, average, poor. Pairs rated good or average are incorporated into the synthetic data, while those rated as poor, along with FL statements that fail both compilations, have only their NL statements preserved for the next iteration.
5

---

3.3 Data Augmentation
This module augments the synthetic data obtained in Section 3.2 using two innovative methods: proving these FL statements and converting them into their contrapositives, in order to further expand the scale of the resulting dataset. Figure illustrates an example of the data augmentation process.
thoures te, 10e0
(ff: Contimoous
V.n. set.
[a
(o.c Contimunusth (F no (Setutee
R
Cortiiious
1ng
Neb a.a
0.2 R-2.--W
(n = +
B
101 a..,
b..b.
Updated State Proof Step
2007.
Original Statement
No,
Intro
in s.a.a N, Vi V.x Setutee
Proof Step
Cannttiuuuu Contimununds (Get.Iee
coriti x
contraposel
Contraposition
Updated State Contraposition
Reconstructed Statement
Figure 3: Demonstration of the proof step and contraposition augmentation methods.
SeepSeek-Prover V1.5 [47] to generate a corresponding proof. The resulting proof steps are then executed sequentially. Each time tactic is successfully applied and the proof process is not yet complete, Lean's Infoview updates the proof state, displaying the current variables, hypotheses, and conclusions. Based on this information, new FL statements be constructed.
Augmentation via Proof. For each FL statement in the synthetic data,
Augmentation via Contraposition. In Section 3.2 FL Statement Parsing, we obtain the theorem_ theorem_hypotheee hypothhseseesseeeeeeeeeees for each FL statement. Furthermore, by extracting the names of all hy- potheses and applying the contrapose! tactic, we can transform the original proposition into an equivalent contrapositive statement for each hypothesis. Leveraging the information provided by Lean's 's Infoview, new FL statements can again be constructed.
Augmentation Data Construction. The aforementioned augmentation operations both rely on Lean Infoview. However, Infoview occasionally results in information loss, particularly concerning type-related details. Although Lean supports implicit type inference, this capability does not extend to all types. To address this, perform FL Statements Compilation on the augmented FL statements and retain only those that compile successfully.
Furthermore, in the process of data augmentation, the primary consideration is the extent of diversity introduced relative to the original data. To maximize this diversity, we employ the following strategies. For the first augmentation method, we retain only those FL statements produced in the final proof step. For the second method, we utilize the Levenshtein distance (53) to select FL statements that exhibit the greatest dissimilarity from the synthetic FL statements. Finally, we utilize LLMs to translate these augmented FL. statements into their corresponding NI. statements, thereby constructing parallel statements. The used translation prompt can be found in Appendix

---

6K
Stdeet Made
Teacher Modal
7127 12
Proof Aug. Bato Contruses on Data
Synnelic Data
Stddnt Data
7k
7385%
Amount
Rounds
24
3
10
2k
8k
10k
Rounds
Amount
Figure 4: Data Generation Statistics Across ATLAS Iterations. Left: The number of synthetic data produced by the teacher and student models at each iteration, with the ratio of student-generated data indicated. Right: The composition of the generated data for each round, including synthetic data, proof augmentation data, and contraposition augmentation data.
pass
pass@8
pass@32 32
(a) ProofNet
(b) PutnamBench
MathQual
Compilation (%)
20
80
60
10
10
Rounds
Rounds
Rounds
Figure 5: Performance of the student model on benchmarks throughout the iterative training process.
4
Experiments
4.1 ATLAS dataset Construction
4.1.1
Experimental Setup
We employ DeepSeek- V2.5 22 as the teacher model and Llama3.1-888 Ins-tnrrut X as the student model, for which utilize nucleus sampling [12] with top p=0.9 and a temperature of 0.6 for generation. To demonstrate the effectiveness of our framework, we aim to transform the general- purpose student model into the Lean 4 expert [4]]
The training procedure of the student model comprises three stages:
Model Initialization. We use LeanDojo [50] to extract FL statements from Mathlib and employ LLMs to generate NL statements, constructing dataset of 56,830 examples. Together with Lean Workbook, this dataset initializes the student model.
Expert Iteration. In each iteration, 10,000 new NI. statements are generated and combined with the remaining NL statements from the previous round to create the synthetic and augmented data. The student model is then fine-tuned on this dataset before proceeding to the next iteration, with this process repeated for total of 10 rounds.
Final Re-training, Llama3.1-88
re- re-irrined on the data generated during expert iteration (referred to as the ATLAS dataset) to develop the ATLAS Translator.
All three stages are fine-tuned using LoRA 13 with LLaMA-Factoon 57 for 3 epochs, with total
batch size of 128 and learning rate of 1. 5.0-5 with cosine decay schedule. All experiments are conducted on single NVIDIA A100 GPU with 40GB of memory. In particular, during the Expert

---

Iteration stage, fine-tuning required only 10 minutes to 1 hour, with minimal hardware requirements and low computational cost, further demonstrating the efficiency of our framework.
4.1.2 Experiment Results
As illustrated on the left side of Figure 4 the total amount of synthetic data produced by both the teacher and student models increases across ATLAS iterations. Notably, the proportion of data generated by the student model (indicated by the Student Data Ratio) grows substantially, rising from 42.68% % in round I to 82.30% in round 10. This demonstrates the increasing capacity of the student model autonomously contribute to the synthetic data as training progresses.
Meanwhile, the right side presents the detailed composition of the generated data for each round. It is evident that with each iteration, only does the overall quantity of data increase, but the contributions from proof and contraposition augmentation methods also become more prominent. This diversified data augmentation strategy effectively enhances the variety of the dataset, allowing subsequent model iterations to benefit from richer and more diverse training signals. We refer to the synthetic and augmented data as the ATLAS dataset, whose statistics are shown in Table []
Figure 5 presents the student model's pass rates on benchmarks across iterative rounds, clearly demonstrating a steady and significant improvement as training progresses. These results indicate that our framework effectively and continuously enhances the student model's 's autoformalization ability, certain extent, since successful compilation is a prerequisite for correct formalization. In addition, Appendix [F] provides some examples of the synthetic data to illustrate the evolution of the student model's 's behavior during successive iterations, including cases that achieve successful formalization after several rounds as well as cases that remain unsolved even after 10 iterations.
Table 1: Statistics of the ATLAS dataset
Synthetic Data
Proof Aug. Data Contraposition Aug. Data
Total
ATLAS dataset
54,641
22.103
40,401
117,145
4.2
ATLAS Translator Evaluation
4.2.1
Experimental Setup
The datasets used for evaluation are ProofNet (2), PutnamBench [36 and MathQual. The version of ProofNet utilized in this evaluation is sourced from DeepSeek MathQual is graduate-level dataset introduced in our work, consisting of 465 NL statements, specifically designed assess the model's generalization ability on more challenging problems. Detailed information on the construction process and specifics of MathQual can be found in Appendix D
Dataset.
Baselines. We compare ATLAS Translator with the teacher model DeepSeek- V3 23 (as V2.5 no longer provides API services), the initialization model Llama3. I-nitaaiiiiiiiiiiiioonn the previous state- of-the-art model Herald Translator
[9], and the latest work Kimina Aatiina-Autooommaliize (37) to evaluate its performance. DeepSeek- is with sampling temperature of 0.7, and the prompt used is provided in Appendix [F] Herald Translator and Kinina-Autoforma
utilize the sampling and prompt settings from their original papers, while Llama3.1 1 Initialiization and ATLAS Translator follow the configurations in Section 4.1
To conduct the evaluation, we follow the validation pipeline described in the Lean Workbook (51) and Herald [9], which includes several key steps:
Validation Pipeline.
1. Translation. We translate the NL statements into FL statements using the corresponding model.
2. Compilation. We use the Lean compiler to verify the syntactic validity of the FL. statements.
3. Tack-Translation For FL statements that pass compilation, we use
[52] to translate them back into NL statements.

---

Table Overall results of the competing baselines and ATLAS Translator. The boldface refers to the highest score and the underline indicates the next best result of the models. indicates that testing not performed because the corresponding model uses that dataset during training. "** signifies statistically significant improvements (two-sided 1-test with p < 0.05) over the best baseline.
ProofNet
PutnamBench
MathQual
Model
pass
pass@8
pass 32
pass@1
pass
pass
pass@1
pass@8
pass
DeepSeck-V3
18.82%
34.07%
41.35%
11.53%
27.74%
37.33%
4.90%
13.42%
17.29%
Llama3. 1-1...11-000 I-Initializaaion
23.56%
42.75%
51.54%
19.30%
45.58%
62. 16%
6.97%
15.61%
22.02%
Herald Translator
31.43%
78.57%
20.36%
52.56%
71.35%
10.92%
31.83%
45.33%
Kimina- Aatimal-atoofomaiiee
19.01%
38.97%
50.71%
ATLAS Translator
39.46%
67.28%
78.71%
23.16%
55.51%
72.93%
22.75%
45.85%
58.23%
Table 3: Ablation study on the three components. The boldface refers to the highest score and the underline indicates the next best result of the models.
ProofNet
PutnamBench
MathQual
Model
pass 69
p
pass 32
pass
pass@8 8
pass 32
pass
pass66322
w// Synthetic
24.10%
51.86%
67.06%
15.99%
42.46%
58.15%
11.79%
29.76%.
40.82%
wso Proof Aug.
37.41%
64.85%
76.39%
22 88%
53,23%
70.71%
22.97% %
44.69%
56.13%
ws/o Contraposition Aug.
39.039
66.09%
77.79%
22.70%
52.56%
69.56%
22.97%
44.95%.
57.20%
ATLAS Translator
39.46 %
67.28%
78.71% %
23.16%
55.51
72.93%
22.75%
45.85
58.23%
ILI Check. Qwen2.5 49 used to compare the back-translace NI. statements with the original NL statements to ensure semantic accuracy.
We consider the translation successful if any of these candidates pass both the compilation and NLI check. For detailed discussion and case study of the validation pipeline's 's effects, especially the NLI check. please refer Appendix B
Evaluation Metrics. We use the pass@ k metric (5) with k 1, 1, 32, as larger values of k enable LLMs better realize their potential in generating diverse outputs, which beneficial for addressing challenging tasks 17 4I]. To reduce randomness, we conduct 5 experiments using the seeds 42, 43, 44, 45, 46, and report the mean of the results. To examine statistical significance, we further perform two-tailed t-test with < 0.05.
4.2.2 Overall Results
The overall results presented in Table 2 At a glance, we find that the proposed ATLAS Translator outperforms all competing baselines across datasets and all pass@k k metrics, thereby confirming the efficacy of our framework. Further insights will be explored through the subsequent analysis.
Comparison with Teacher and Initialization Model. The experimental results clearly demonstrate that ATLAS Translator significantly outperforms its teacher model DeepSeek-Vy V3 and initialization model Llama3. I-Iittialization across all benchmarks. Notably, on ProofNet, ATLAS achieves pass@ @1 score of 39.4994 99.46% nearly doubling DeepSeek- V3's 18.82% and surpassing Llama3. I's 23.56%. More importantly, similar improvements are consistently observed in pass@8 8 and pass@33 32 metrics, as well as across other benchmarks, strongly validating the effectiveness of ATLAS framework.
Comparison with Competing Models. When examining the comparison with competing models, ATLAS Translator shows remarkable advantages over both the Herald Translator and the newer mmnin--Autoformmlizee With the exception of ProofNet's @3, statistically significant improve- ments are observed in all other metrics and across all other benchmarks. Furthermore, considering that Herald Translator utilizes 1,160k data points for fine-tuning and that Sinina-Autoformal consistently involves Lean 4 experts during its training process, it is noteworthy that the ATLAS Translator achieves these results using only 117k data points and without any human intervention. This further underscores the effectiveness of the ATLAS framework.

---

Table 4: Additional results of LoRA and full- full-parameter fine-tuning on various base models with the ATLAS dataset. "*" denotes full-param parameter fine-tuning. Abbreviations: L (Llama-3.1-8P Instruct), D (DeepSeek-Prre) Prover- 115.-11----- Base), and Q (one:55-Code-----nnseee refers to the highest score and the underline indicates the best result of the baselines. "." indicates that testing not performed because the corresponding model uses that dataset during training.
The boldface
Model
miniF2F
ProofNet
PutnamBench
Vaatiiuaal
piss 1
puss
1
pass0
passis
passti
piss
puss
passt0 52
Herald Transiator
26.02%
23,44%
291g
31.43%
7M.57%
52.56%
71,3515
10:9256
31.83%
45.33%%
Sinino--uzofoommliier
19.01%
ATLAS Transiator (L)
66.60%6
58.52%
93.244
67.28%
78.711
23.161
55.51%
72,9316
22.755%
58.23%
ATI.AS Trandatorr (1.)
69.675
02.42%
96.935%
47.98%%
666)
86.5256
38.549
73. 2999
$4.99%
40.22%
78.485
ATLAS Trandator (D)
67.01%
90.98%
95.31%
39.51%
69: 19.19%
$1.625
25.641%
59.00%
75.75%
24.30%
49.59%
63.
ATLAS Transtator (D)
77.25%
93.65%
95.50%
54.99%
80.86%
58.95%
42.89%
76.95%
87.86%
38.91256
67.31%
79.78%
ATLAS Trandatto Q))
66 60%
91 80%
96 72%
58.81%
71 43%
84. 10%
29 70%%
66. 77%
82. 25.25%
28. 17%
54.19%
68. 17%
AILAS Tranclator (Q)
69.80 09.88%
89.75%
92.62%
50.67%
79.511
36.25%
39.91%
76.92%
87.56%
37.63%
65.59%
76.34%
4.2.3 Ablation Study
The results of the ablation study are shown in Table where we also conduct 5 experiments using the same seeds and report the mean results. The removal of syntheric data leads to the most significant performance drop across all datasets and metrics, underscoring its critical role in training robustness. In contrast, omitting proof or contraposition augmentation data results in a more moderate decline in performance. Nevertheless, the full model consistently achieves the highest scores or, at the very least, competitive second-best results, thereby validating the synergistic effect of all components.
4.2.4 Additional Results
The results of applying LoRA and full-parameter fine-tuning to various base models on the ATLAS These experiments reveal two key insights.
dataset are detailed in Table 4
First, a primary finding is that full-parameter fine-tuning consistently and significantly outperforms the more parameter-efficiert LoRA approach. This performance gap is particularly pronounced for the BrrSSeekPrroer--..55-.
model; on miniF2F (56]. full-parameter fine-tuning achieves pass@ @1 score of 77.25% a substantial improvement of over 10 absolute points compared to its LoRA counterpart (67.01 %). This trend holds true across all three base models.
Furthermore, the results highlight the critical role of the base model. The DeepSeek- ParsSeek-Proer--.. Prover- V1.5-7B- Base model, when fine-tuned on the ATLAS dataset, achieves new state-of-the-art results most benchmarks, with impressive pass@ @1 scores of 54.99% on ProofNet and 42.49% on PutnamBench. This outcome is expected, given the model's extensive pre-training on Lean-related corpora. Conse- quently, we hypothesize that employing more powerful base model as the student model within our iterative framework would further enhance its overall efficiency.
Conclusion
In this paper, we propose novel framework to advance autoformalization by synthesizing and augmenting large-scale, high-quality parallel statements. Our method addresses key limitations of existing approaches, such the finite amount of data that can be extracted from Mathlib and the extensive pre-processing required for data obtained from web scraping. Through comprehensive experiments, we verify the effectiveness of the ATLAS framework and achieve new state of the art.
Acknowledgments and Disclosure of Funding
This work is sponsored by the National Key R&D Program of China Grant No. 2022YFA1008200 (T. L.). We also thank Shanghai Institute for Mathematics and Interdisciplinary Sciences (SIMIS) for their financial support. This research was funded by SIMIS under grant number SIMIS-ID-202S-ST. The authors grateful for the resources and facilities provided by SIMIS, which were essential for the completion of this work. We appreciate the insightful discussions with Wei Zhao, Xinpu Tu, and Shuyu Yin during the early stages of the project, as well as Tao Zhu's valuable involvement in the human evaluation at a later stage.
10

---

References
[1] A. Agrawal, S. Gadgil, Goyal, Narayanan, and Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07522 2022.
[2] Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers. D. Radev, and J. Avigad. ProofNet: Autoformalizing and formally proving undergraduate-llvel mathematics. arXiv preprint arXiv:2302. /2433, 2023.
[3] Z. Azerbayev, H. Schoelkopf, K. Paster, M. D. Santos, S. McAleer, A. Q. Jiang, J. Deng. Biderman, and S. Welleck. Llemma: An open language model for mathematics. In The Twelfth International Conference on Learning Representations, 2024.
[4] B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliârre, E. Giménez, Herbelin, al. The Coq proof assistant reference manual. INRIA, version, 6(11), 1999.
[5] M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. D. O. Pinto. J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, et Evaluating large language models trained on code. arXiv preprint arXiv:2107.03377, 2021.
[6] G. Cunningham, R. C. Bunescu, and D. Juedes. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. In Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP), pages 25-32. Association for Computational Linguistics, 2023.
[7] L. De Moura, S. Kong, Avigad, Van Doom, and von Raumer. The Lean theorem prover (system description). In Automated IeduutiionCADE. 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378-388. Springer, 2015.
[8] A. Dubey, A. Jauhri, A. Pandey, A. Kadian, A. Al-Dahle, A. Letman, A. Mathur, A. Schelten, A. Yang, A. Fan, et al. The Llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024.
[9] G. Gao, Y. Wang. J. Jiang, Q. Gao, Qin, T. Xu, and B. Dong, Herald: A natural language anno- tated Lean 4 dataset. In The Thirteenth International Conference on Learning Representations, 2024.
[10] J. Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265-269. Springer, 1996.
[11] G. Hinton, O. Vinyals, and J. Dean. Distilling the knowledge in neural network. arXiv preprint arXiv:1503.0253), 2015.
[12] A. Holtzman, J. Buys, L. Du, M. Forbes, and Y. Choi. The curious case of neural text degeneration. In International Conference on Learning Representations, 2020.
[13] E. J. Hu, yelong shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang. L. Wang, and W. Chen. LoRA: Low-rank adaptation of large language models. In International Conference Learning Representations, 2022.
[14] Y. Huang, X. Lin, Z. Liu, Q. Cao, H. Xin, H. Wang, Z. Li, L. Song, and X. Liang. MUSTARD: Mastering uniform synthesis of theorem and proof data. In The Twelfth International Conference on Learning Representations, 2024.
[15] A. Q. Jiang, W. Li, and M. Jamnik. Multilingual mathematical autoformalization arXiv preprint 23X1::331..0375. 2023.
[16] A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Wu. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. The Eleventh International Conference on Learning Representations, 2023.
[17] A. Q Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Wu. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. The Eleventh International Conference on Learning Representations, 2023.
11

---

[18] J. Li, E. Beeching, L. Tunstall, B. Lipkin, R. Soletskyi, S. Huang, K. Rasul, L. Yu, A. Q. Jiang, Z. Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13:9, 2024.
[19] Y. Li, D. Du, L. Song, C. Li, W. Wang, T. Yang, and H. Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprini arXiv:2412.20735. 2024.
[20] Z. Li, Wu, Z. Li, X. Wei, X. Zhang, F. Yang, and X. Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024.
[21] Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, et al. Goedel-prover: frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640. 2025.
[22] A. Liu, B. Feng. Wang. B. Wang. B. Liu, C. Zhao, C. Dengr, C. Ruan, D. Dai, D. Guo, et al. Deepseek-v2: A strong, economical, and efficient -ffeeer- language model. arXiv preprint arXiv:2405.04443 044444444 2024.
[23] A. Liu, B. Feng, B. Xue, B. Wang, B. Wu, C. Lu, C. Zhao, C. Deng, C. Zhang, C. Ruan, et al. Deepseek-v3 technical report. arXiv preprint 29447774 2024.
[24] Q. Liu, X. Zheng, X. Lu, Q Cao, and Yan. Rethinking and improving autoformalization: Towards faithful metric and dependency retrieval-basee approach. In The Thirteenth International Conference on Learning Representations, 2025.
[25] J. Lu, Y. Wan, Y. Huang, J. Xiong, Z. Liu, and Z. Guo. Formalalign: Automated alignment evaluation for autoformalization. The Thirteenth International Conference on Learning Representations, 2024.
[26] Lu, Y. Wan, Z. Liu, Y. Huang, Xiong, C. Liu, Shen, H. Jin. J. Zhang, H. Wang, al. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406.0199 2024.
[27] L. d. Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction-CADD 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pages 625-635. Springer, 2021.
[28] L. Murphy, K. Yang. J. Sun, Li, A. Anandkumar, and X. Si. Autoformalizing euclidean geometry. In Forty-first International Conference Machine Learning, 2024.
[29] L. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
[30] S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344 2022.
[31] Polu and I. Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009. 033933, 2020.
[32] Z. Ren, Z. Shao, Song, Xin, H. Wang, W. Zhao, Zhang, Z. Fu, Q. Zhu, D. Yang, et al. beepseek-prover-ee Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
[33] V. Shah, D. Yu, K. Lyu, S. Park, N. R. Ke, M. C. Mozer, Y. Bengio, S. Arora, and A. Goyal, Al-assisted generation of difficult math questions. In The 4th Workshop on Mathematical Reasoning and Al at NeurlPS' 24, 2024.
[34] C. Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 31, 2020, Proceedings 13, pages 3-20. Springer, 2020.
[35] The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, Jan. 2020.
12

---

[36] G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri. PutnamBench: Evaluating neural mncorem-provent on the putnam mathematical competition. In The Thirty-eigh Conference on Neural Information Processing Systems Datasets and Bench- marks Track, 2024.
[37] H. Wang. M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, al. -imina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504. 1354, 2025.
[38] H. Wang, H. Xin, C. Zheng, Z. Liu, Q. Cao, Y. Huang, Xiong, H. Shi, E. Xie, J. Yin, Z. Li, and X. Liang. LEGO-Prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024.
[39] Q. Wang, C. Brown, C. Kaliszyk, and J. Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 85-98, 2020.
[40] Q. Wang, C. Kaliszyk, and J. Urban. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pages 250-270. Springer, 2018.
[41] R. Wang, J. Zhang, Y. Jia, R. Pan, S. Diao, R. Pi, and T. Zhang. Theoremllama: Transforming general-purpor purposs Ilms into lean4 experts. arXiv preprint arXiv:2407.0320; 2024.
[42] X. Wang, Y. Chen, and W. Zhu, survey on curriculum learning. IEEE transactions on pattern analysis and machine intelligence, 44(9):455-45776 2021.
[43] Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353- 32368, 2022.
[44] Z. Wu, S. Huang. Z. Zhou, H. Ying, J. Wang, D. Lin, and K. Chen. (ieemmm2.5-ssepprovve Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410. 15700, 2024.
[45] Z. Wu, J. Wang, D. Lin, and K. Chen. Lean githh:: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407. 17227, 2024.
[46] H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. DeepSeek- Prover: Advancing theorem proving in Ilms through large-scale synthetic data. In The 4th Workshop on Mathematical Reasoning and Al at NeurlPS 24, 2024.
[47] H. Xin, Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Du, W. Gao, H. Zhang, Q Zhu, D. Yang, Z. Gou, Z. Wu, F. Luo, and C. Ruan. SrepSeek-Prover--e Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In The Thirteenth International Conference on Learning Representations, 2025.
[48] R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen. Bfs- prover: Scalable first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.088. 03438, 2025.
[49] A. Yang, B. Yang, B. Zhang, B. Hui, B. Zheng, B. Yu, C. Li, D. Liu, F. Huang, H. Wei, et al. Qwen2.5 technical report. arXiv preprint 15115 2024.
[50] K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, Yu, S. Godil, R. J. Prenger, and A. Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024.
[51] H. Ying, Z. Wu, Y. Geng, J. Wang, D. Lin, and K. Chen. Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024.
13

---

[52] H. Ying, S. Zhang, L. Li, Z. Zhou, Y. Shao, Z. Fei, Y. Ma, J. Hong, K. Liu, Z. Wang, Y. Wang. Z. Wu, S. Li. F. Zhou, H. Liu, S. Zhang, W. Zhang, H. Yan, X. Qiu, Wang, K. Chen, and D. Lin. InternI Open math large language models toward verifiable reasoning. CoRR, 0bs//2402.06332, 2024.
[53] L. Yujian and L. Bo. A normalized levenshtein distance metric. IEEE transactions on pattern analysis and machine intelligence, 29(6):199111095, 2007.
[54] L. Zhang, X. Quan, and A. Freitas. Consistent autoformalization for constructing mathematical libraries. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020-4033, Association for Computational Linguistics, Nov. 2024.
[55] C. Zheng, H. Wang, Xie, Z. Liu, Sun, H. Xin, Shen, Z. Li, and Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309. /5866, 2023.
[56] K. Zheng. J. M. Han, and S. Polu, miniF2F: cross-system benchmark for formal Olympiad- level mathematics. In International Conference on Learning Representations, 2022.
[57] Y. Zheng, R. Zhang, Zhang. Y. Ye, and Z. Luo. LlamaFactoryy Unified efficient fine-tuning of 100+ language models. In Y. Cao, Y. Feng, and D. Xiong, editors, Proceedings of the 62nd Anmual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations), pages 400-410 Association for Computational Linguistics, Aug. 2024.
[58] J. P. Zhou, C. E. Staats, W. Li, C. Szegedy, K. Q Weinberger, and Y. Wu. Don't Trust: Verify grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, 2024.
14

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The scope and contributions of the paper included in the abstract and intro- duction. Please refer to the first and last paragraph of Section for scope and contributions, respectively.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
limitation section is included in the Appendix A
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model sellsspeciiiationn asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
15

---

Answer: [NA].
Justification:
The paper does not have any theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proof's can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: We have provided all implementation details in Section 4.1.J and Section 4.2.1 All prompts used are given in Appendix F
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, descríbing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e-g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
5. Open access to data and code
16

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification:
The datasets, model, and code are available at https: com/
XiaoyangLiu-sjtur ATLAS
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips... cc/
for more details.
While encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to rum to reproduce the results. See the NeurIPS code and data submission guidelines (https
/tips.cc/ppble.. wwtppbplcggguiiieecceeeeeeooeeee http:/gddes//eee/ https//CooSuubiiisce stibbbbmmssoooooooocc. for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Question:
Answer: [Yes]
Justification: We have provided all implementation details in Section 4.1.1 and Section 4.2.1 All prompts used are given in Appendix F
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
We run the experiments times with seeds 42, 43, 44, 45, 46, report the mean results, and perform a two-tailed t-test with p < 0.05 to demonstrate statistical significance in Table
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
17

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative еπτог rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: We provide the details of compute resources in the last paragraph in Section 4
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics http:///waarrrpccccpppaaccccacaa
Answer: [Yes]
Justification:
We have made that our paper conforms with the NeurIPS code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: We discuss the potential positive impacts that our framework will bring in the Section
Guidelines:
The answer NA means that there is no societal impact of the work performed.
18

---

If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), faimess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA].
Justification:
The paper poses no such risks.
Guidelines:
The answer NA means that
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but encourage authors to take this into account and make best. faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: We have cited the original paper or attached the link to the existing assets used in this paper.
Guidelines:
The answer NA means that the paper does existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset used and, possible, include a URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
19

---

If assets are released, the license, copyright information, and terms of use in the thcode. has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, paperswi
latasets.paperssi
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA].
Justification:
The paper does not release new assets up to now.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA].
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country institution) were obtained?
Answer: [NA].
Justification: The paper does not involve crowdsoureing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
20

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [Yes]
Justification: In Sections and we provide detailed introduction on how LLMs are incorporated into our framework. In Appendix F we present the prompts used for each LLM in our framework.
Guidelines:
The answer NA means that the method development in this research does not involve LLMs as any important, original, or non non-standard components.
Please refer to our LLM policy for what should or should be described.
21

---

A Motivation, Limitations, and Future Work
Motivation. Our work builds upon MUSTARD [14] by addressing of its primary limitations. And solutions to these limitations constitute the core contributions of this paper.
Data Sourcing, MUSTARD sources concepts from the Khan Academy Website, which can create a "formalization bottleneck" as some concepts lack a direct counterpart Mathlib. To overcome this, ATLAS sources concepts exclusively from Mathlib, guaranteeing a valid formalization path for every statement from the start.
Generation Efficiency. MUSTARD's reliance on GPT-4 for correction loops is costly, low-yield process: over 90% of initial generations fail the prover validation, resulting final dataset of only 6k samples. In contrast, the teacher-student distillation framework in ATLAS is highly efficient, dramatically reducing costs and enabling the generation much larger dataset of 117k high-quality pairs.
Limitations. key limitation of our work is that we do not verify the correctness of the synthetic mathematical propositions in the ATLAS dataset. This decision is based on two primary factors. First, the autoformalization task is fundamentally about the fidelity of translation from natural language to formal language; the underlying truth value of a proposition does not alter the core translation challenge. Second, the current capabilities of automated theorem provers are insufficient for reliably verifying a large corpus of undergraduate--ever mathematics. For example, the state-of- the-art PerpSeee-Proee--Wee V2-671B B2 only achieves 7.44% success rate on PutnamBench, making large-scale verification prohibitively challenging and costly.
Nevertheless, we acknowledge that training models on a corpus containing false propositions poses potential risk for downstream applications, particularly for the automated theorem proving task. To quantify this risk, we performed an analysis estimate the prevalence of incorrect propositions in our dataset. We randomly sampled 100 propositions from ATLAS and established ground truth for their correctness using panel of experts, which included human evaluators alongside advanced LLMs (DeepSeek-R) I and Gemini-2.5-PPre analysis classified 60 of the sampled propositions as true and as false. This finding provides baseline estimate of the dataset's 's truthfulness and highlights an area for future work in synthetic data refinement.
Using majority vote consensus from this panel, our
Another limitation is the diversity of data enhanced by proof. The augmentation-via- designed generate novel propositions by treating each step of formal proof as a semantic transformation. Ideally, the final proposition in proof chain should be substantially different from the original. However, a limitation of the current implementation that the practical diversity of these transformations can be constrained, particularly when the proof relies on trivial tactics.
method
To quantify the textual diversity of augmented data, we conducted an analysis on 100 randomly sam- pled propositions. We measured the BLEU score between the original and augmented versions, where lower score signifies greater novelty. The analysis revealed that augmentation-vian -iiaiioooo----oooooooooooooooooe (Average BLEU: 0.6709) produces less diverse statements on average than sitmrentttionvviccoonrrppssosssi (Average BLEU: 0.6026). To enhance the former, we plan implement stricter filtering mechanism that, for example, disallows augmentations generated from trivial tactics.
Future Work. A primary direction for future work is to implement more explicit curriculum learning 42 strategy to guide the model's improvement. This strategy comprises two main compo-
nents:
Compositional Complexity. We will restructure the concept repository into a graph, enabling the systematic generation of a curriculum. New theorems will be synthesized by progressively increasing both the conceptual distance between ideas (i.e., path length in the graph) and the number of concepts required to form a valid statement.
Conceptual Hierarchy. We will introduce a graded concept repository (e.g., high school + undergraduate + graduate). The model must demonstrate proficiency at one level before unlocking access the next, creating a structured path toward mastering more advanced topies.
Together, these mechanisms will enable our pipeline to autonomously generate a curriculum of increasing difficulty, creating powerful virtuous cycle of self-imprrvemmnn.
22

---

A more ambitious goal is to extend our framework from formalizing individual statements to entire mathematical theories. This direction is inspired by dependency-awand retrieval-based methods like RAutoformalizer [24]. While such methods improve performance by retrieving premises at inference time, our work focuses on data generation. promising synthesis of these ideas is to integrate the core principle of dependency awareness directly into our data generation process.
Our technical approach for this involves restructuring the concept repository into dependency-awend tree. During synthesis, we will generate data in a bottom-up, layer-by-layer fashion, explicitly preserving the logical dependencies from foundational axioms to advanced theorems. The result- ing structured dataset would be ideal for training next-gent next-generation models capable of theory-level autoformalization.
B Discussion for Validation Pipeline
In this section, we discuss and examine the reliability and equity of our validation pipeline and evaluate instances of both successful and unsuccessful validations.
28 automated evaluation of translated statements. However, all of these approaches are based on the mutual proof the translated FL. statements and the labeled FL. statements. Considering the development of the field of automated theorem proving, it is unrealistic to use this method for automated evaluation on undergraduate and graduate datasets, the most powerful model currently, SeepSeek-Prover-VVe V2-671B, has only achieved a proof rate 7.44% on PutnamBench.
Discussion. Recently, there has been some work 20
24
Conversely, concerning the validation pipeline, it is important to highlight that validation based on LLMs can sometimes diverge from human judgment, particularly in instances of false positives. Nevertheless, this approach remains standard in the field (e.g., see Lean Workbook [5I], Herald [9] and is currently one the few viable solutions for large-scale automated evaluation. This is primarily because conducting human expert reviews under the pass @ l: metric is impractical.
In our implementation of the validation pipeline, especially the NLI check, the primary objective is establish a fair performance evaluation among different models. As demonstrated in the subsequent experiments, all the baseline models and our proposed model yield comparable results regarding the proportion of false-positive cases, indicating that the validation pipeline is relatively fair.
Experiment Results. To provide a clearer illustration of the false positive cases and the fairness discussed earlier, conduct experiment to evaluate the outcomes that pass through the validation pipeline. Specifically, we select the entire ProofNet dataset, consisting of 371 natural language statements, and translate it using the ATLAS Translator, well two baseline models: the Herald Translator and the Llama-3.1 Initialization.
The outputs of autoformalization that successfully pass validation are classified by human experts into three distinct categories: correct translations, minor errors, and major errors. These classifications adhere to the evaluation criteria established in Herald [9.
Correct Translation. A correct translation must accurately reflect the mathematical meaning of the natural language statement. In cases where the original statement is ambiguous, allow the formalized statement to adopt any mathematically valid interpretation.
If the formalized result deviates from the original statement but can be easily corrected by altering single formal definition or restructuring single logical relation within the hypothesis or statement, it is classified as a minor error.
Minor Error.
Major Error. All other cases are classified as major errors.
As shown in Table 5 the ATLAS Translator and other baseline models also experience false positives, exhibiting comparable false positive rates, which ensures a fair comparison. In Sections B.T B.2 and
B.3
provide examples for cach of these three categories.
23

---

Table 5: Human evaluation results of validation passed statements
Model
Validation Passed
Correct Translation
Minor Error
Major Error
Llama3. 1- Initialization
82
43
30
9
Herald Translator
134
79
31
24
ATLAS Translator
151
26
26
B.1
Correct Examples
# Example
Suppose that f is holomorphic in an open set Ω. Prove that if Re(f) is constant, then f is constant.
theorem Lm_name (Q DifferentiableOn Cf () (h : Aee, Q A Q, (f 2) re re) E VEE,, f2 f :- by sorry
(hl Is0pen D (f : C (hf
(f w)
# Example
Let X be a topological space; let A be a subset of X. Suppose that for each æ E A there is an open set U containing such that U A. Show that open in X.
theorem name (X : Type*} [TopologicalSpace X] (A Set X) (hA V A, 3 U, Is0pen U A
Is0pen A : by sorry
# Example
Let p: X + Y be closed continuous surjective map such that p- ((v)) is compact, for each y E (Such map called perfect map.) Show that if Y is compact, then X compact.
theorem ma_name {X Y Type*} [TopologicalSpace X]
TopologicalSpace Y] [CompactSpace Y] {p X + Y} (hp
Continuous p) (h Function Surjective p) (h 4 y Y.
IsCompact (p -1 (y))) CompactSpace X :- by sorry
B.2 Minor Error Examples
# Example
Show that fo log(sin wa)da = log 2.
theorem
im_name (π R) ʃ in (0 .)..1, Real log (Real. sin n x)/m) Real log by sorry
Analysis: Incorrectly formalizing sin म as sin( * 2)/T.
# Example 2 Let f be real uniformly continuous function on the bounded in R!. Prove that f is bounded on E.
theorem cm_name (f : R R) (E Set R) (hE IsCompact
hff
UniformContinuuusunn f E) a X, V E, If x1 M by sorry Analysis: In the formalization, the condition that the set E is bounded is strengthened E being compact.
# Example
Let R be a commutative ring with , Prove that a nilpotent element of then ab is unit for all b R.
theorem tm name (R Type*} [CommRing R] IsDomain R [Nontrivial R
bab R) (ha : IsNilpotent a) IsUnit (1 - = by
sorry
Analysis: in the formalization, additional assumption made that R is domain.

---

B.3 Major Error Examples
# Example
If Co +... Ca-1 + Cu. 0, where Ca...., Cn real constants, prove that the n+l
equation Co + C5 + ....4 +0 Cn-12" 1-=== + Cn =0 0 has at least one real root between and 1.
theorem
ma_e (n : N) (hn
0
<
n) (c
Fin
(n + 1) 7
R)
(hC
Σ
Fin (n + 1), C (i + 1) = 0)
3
R, 0 5 A x
1
A
C 0
2 3
C
7
9
c 10 10 i by sorry
Analysis: The polynomial is written explicit terms instead of general sum, losing generality for arbitrary n.
# Example
G is group in which (ab)² = a'b' for three consecutive integers i, prove that abelian.
theorem
tm ma_e {G : Type*} [Group Gl [Fintype G] [AddCommMonoid G
[MulAction G] (a b G) (i k R) (h i +
k) (h' (a* b) i = b
by
sorry
Analysis:
Omitted the assumptions (ab)² = alb and (ab)* a²b only stated (ab)* = a'b'.
Example
Prove that set U M is open if and only if none of its points limits of its complement.
theorem tm name {M Type*} [MetricSpace M] [Topologi caaSpace M] ( Set M) Is0pen + z E U, v y Uc, * y by sorry Analysis: This formalization does not faithfully express the conclusion about limit points of the complement."
C Concept Repository
The complete concept repository is composed of 13 domains, 55 topics, and 350 concepts. For the sake of clarity and brevity, Table presents a subset of topics from 3 domains, along with their corresponding concepts. And the full repository can be accessed in the open-source material.
D MathQual
The MathQual dataset is derived from graduate qualification examinations from multiple universities, including Boston University, Johns Hopkins University, University of Texas Dallas, University of California, Los Angeles, University of California Riverside, and University of Georgia. Table presents the domains included the MathQual dataset and the process of creating the dataset is elaborated as follows.
1. Relevant PDF documents retrieved from official websites.
2. Optical Character Recognition (OCR) technology is employed to convert these documents into Markdown format.
3. High-quality, formalizable problem statements are meticulously selected through manual filtration process. Notably, for proof problems consisting multiple sub-questions, we amalgamate the overarching contextual conditions of the main problem with the specific conditions of each sub-question, thereby constructing several distinct problem statements.
4. The problem statements are categorized according to Mathematics Subject Classification (MSCF)
hhngss//bomath.ooolllsssstcatta
25

---

Table 6: Partial list of mathematical concepts in the concept repository
Domain
Topic
Concept
vector space, product of vector spaces, vector subspace, quotient space, sum of subspaces, direct sum, complementary subspaces, linear independence, generating sets, bases, existence of bases, linear map, range of linear map, kernel of a linear map, algebra of endomorphisms of a vector space, general linear group
Fundamentals
Duality
dual vector space, dual basis, transpose a linear map
Finite-
lnite-dimensionallty, isomorphism with K", rank of linear map, rank a set vectors, isomorphism with bidual
dimensional
Linear Algebra
vector spaces
multilinnar map, determinant of vectors, determinant of endomorphisms, orientation of IR-ector space
Multilinearity
coanutative-rin-vvllie matrices, field-valued matrices, matrix representation of a lincar map, change of basis, rank of matrix, determinant, invertibility
Matrices
Endomorphism polynomials
annihilating polynomials, minimal polynomial, characteristic polynomial, Cayley- Hamilton theorem
Structure theory
eigenvalue, cigenvector, generalized eigenspaces, Selaa--Cheaalle--uunooo decomposition
endomorphisms
radius convergence, continuity, diffcrentiahility with respect to the complex variable, complex exponential, extension trigonometric funetions(cos) to the complex plane, extension of trigonometric functions(sin) the complex plane, power series expansion of elementary functions(cos)) power series expansion of elementary functions(sin)
Complex Valued series
Single Variable Complex Analysis
holomorphic functions, Cauchy formulas, analyticity a holomorphic function, principle of isolated zeros, principle analytic continuation, maximum principle, holomorphic stability under uniform convergence
Functions complex variable
topology of a metric space, induced topology, finite product of metric spaces, limits of sequences, cluster points, continuous functions, homeomorphisms, compactness in terms of open covers (Borel-I Lebesgue, scquential compactness is equivalent compactness (Bolzano-Wal Weierstrass) connectedness, connected components, path connectedness. Lipschitz functions. uniformly continuous functions, Hleine-Cante theorem, complete metric spaces, contraction mapping theorem
Topology and Metric Spaces
topology normed vector space, Banach open mapping theorem, equivalence norms finite dimension, norms I|: on R" and C" absolutely convergent series in Banach spaces, continuous linear maps, norm of a continuous linear map, uniform convergence
Topology
Normed vector spaces on It and
(sup-norm), normed space of bounded continuous functions, completeness the space of bounded continuous functions, Heine- Borel theorem (closed bounded subsets are compact in finite dimension), Riesz' lemma (unit-ball characterization of finite dimension), Arzela-Ascofi thcorem
e
Hilbert projection theorem, orthogonal projection onto closed vector subspaces, dual space, Riesz representation theorem, inner product space 12, completeness of (2, inner product space L completeness L?, Hilbert bases, example, the Hilbert basis trigonometric polynomials, Lax-Milgram theorem
Hilbert spaces
26

---

Table 7: Domain Classification and Problem Counts in MathQual
Domain
Count
Algebraic geometry
Algebraic topology
26
Associative rings and algebras
Calculus of variations and optimal control; optimization
Category theory; homological algebra Combinatorics
Commutative algebra
43
Difference and functional equations
Differential geometry
Field theory and polynomials Functional analysis Functions of complex variable General topology
32
23
101
24
Global analysis, analysis on manifolds Group theory and generalizations Harmonic analysis Euclidean spaces Linear and multilinear algebra; matrix theory Manifolds and cell complexes Mathematical logic and foundations
18
51
7
25
11
Measure and integration
Number theory
5
Operator theory
Ordinary differential equations
2
Partial differential equations
Potential theory
7
Probability theory and stochastic processes Real functions
4
Several complex variables and analytic spaces Topological groups, Lie groups
3
Total
465
27

---

E
Case Study
This section presents both successful and unsuccessful cases of synthetic data during the ATLAS iterative process. Tables to 13 display successful cases generated by ATLAS, while Tables 14 and iilllustrtee the failed cases, each accompanied by corresponding analyses. The FL statements consist of multiple rounds, with content highlighted in red boxes indicating syntactic emrors or inconsistencies with the relevant NL statements. Iteration for each data point ceases when there are no syntactic or semantic errors in the FL statement. The cases below demonstrate that, as the model iterates, it is able to formalize mathematical concepts Lean with increasing accuracy.
Table 8: A successful case generated by ATLAS
Analysis: In the first round, the model incorrectly formalized the matrix notation in Lean. However, in the second round, the formalization correct.
Concept1:
commutative-ring-reee valuued matrices
Domain1: Linear algebra
Concept2: determinant
Domain2:
Linear algebra
atatement: For any commutative ring R and any matrices A and B
over R, the determinant their product equal to the product of their determinants, i.e., det(AB) det det(B)
FL statements:
Round
theorem
{R Type*) [CommRing R] (n N)
(A B Matrix (Fin n) R)) (A det = Aedet B.det == by
sorry
Round 2
theorem tm_name {R Type*} [CommRing R] (n N) (A B Matrix (
Fin n) (Fin n) R) (A det A. det B. det by sorry
Table 9: A successful generated by ATLAS
Analysis:
In the two rounds, model was unable to correctly formalize the concept "derivative." " However, in the third round, it successfully formalizes this concept, demonstrating that the model effectively masters it after the learning experiences of the first two rounds.
Concept1: Leibniz formula
Domain1: Single Variable Real Analysis
Concept2: hyperbolic trigonometric functions
Domain2: Single Variable Real Analysis
statement: The derivative of the hyperbolic sine function, sinh(z), can expressed using the Leibniz formula as (i) = cosh(zz)
FL statements:
Round
theorem
(x R) deriv sinh cosh
by sorry
Round
theorem tm_ Same deriv sinh cosh : by sorry
Round 3
theorem tm_name name HasDerivAt (fun x R => Real sinh x) (Real. cosh x) by sorry
28

---

Table 10: successful case generated by ATLAS
Analysis: In the first round, the model failed to correctly formalize the concepts of "domain" and "being an injection on certain set." In the second and third rounds, learned how to formalize "domain," " but struggled accurately formalize "being injection certain set." In the fourth round, it successfully formalized these concepts.
Concept1:
metric structure
Domain1:
Single Variable Real Analysis
Concept2: derivative at point
Domain2: Single Variable Real Analysis
NL statement: If a function f is differentiable at e and f'(c) # 0, then there exists neighborhood U of such that f is injective U.
statements:
Round
theorem tm_name (f R-+R) R) (c R) (hf Differentiablett f c
deriv f 0) (U Set R), E U)
(InjectiveOn U)
by sorry
Round
theorem tm_ name (f R+RR (c : RR (hf DifferentiableAt f c)
(he deriv f # 0) U E nhds c, Function Function.Injectiinn InjectiveOn f U
by sorry
Round
theorem tm_name (f R) (a (hf (he deriv f c + 0) : BUE nhds c,
DifferentiableAt c)
Function Injective (f (A x) U) (xx x) (U U))
by sorry
Round
theorem name (f R R) (c RR) (hf DifferentiableAt f c)
(h'f deriv f # 0) U nhds c, Set InjOn f U :- by
sorry
29

---

Table 11: A successful case generated by ATLAS
Analysis: In the previous rounds, model was unable to correctly formalize "the order a finite group" and the concept of "two coprime positive integers", and there was unnecessary formalization. However, in the eighth round, the formalization was done correctly.
Concept1: direct product of groups
Group Theory Concept2: & is euclidean ring
Domain1:
Domain2:
Ring Theory
atatement: Let G and H be groups. If G x H is cyclic, then G and If cyclic and their orders are coprime. FL atatements:
Round 3
theorem
{G Type*} [Group G] [Group H] (h IsCyclic ( H)) IsCyclic G IsCyclic
lat.coPrime (orderOf0f G) (order0f0f H) : by sorry
Round
theorem tm_name {G H Type*} [Group G] [Group H] (hG IsCyclic
(G H)) (hH IsCyclic (H G) IsCyclic IsCyclic
Nat. coPrime (order0f0f (order0f0f H) by sorry
Round 5
theorem tm_ne name (G H Type*} [Group G] [Group H] (hG IsCyclic (G H)) IsCyclic G IsCyclic A
Nat. coPrime (Nat card G) (Kat card H) by sorry
Round 6
theorem tame {G Type*} [Group G] [Group H] [Fintype G] [
Fintype H] (hG IsCyclic (6 H)) (hll IsCyclic (H G)
IsCyclic IsCyclic A
Nat.coPrima (Fintype. card G) cart H) by sorry
Round
theorem name {G Type+} [Group G] [Group H] [Fintype G] [
Fintype H] (hG IsCyclic (6 H)) (hHl IsCyclic (H G) )
IsCyclic IsCyclic A (Fintype. card G) ged (Fintype.. card H) = = == by sorry
Round 8
theorem tm name {G Type*} [Group G] [Group H] [Fintype G] [ Fintype H] (h IsCyclic (G H)) IsCyclic A IsCyclic H (Fintype. card G). (Pintype.card card H) 1 := by sorry
30

---

Table 12:
A successful case generated by ATLAS
Analysis: In rounds seven, the incorrect formalization "Finset" was used. In round eight, the model revised it to "toFinSet," but it remained incorrect. Finally, in round nine, the formalization was done correctly. Note: The translation results for rounds to 4 were subpar and lacked any significant insights, they not displayed.
Concepti:
Cauchy-Schwarz inequality
Bilinear and Quadratic Forms Over Vector Spac Concept2: counting measure
Domain1:
Domain2: Measures and integral calculus
NL statement: For any finite set and functions f, 9 S + R, the Schwarz inequality holds: (Eaes f())g(=)) (Eres f(x)²) (Exesg(a))
FL statements:
Round 5 ~
theorem
tm name (S FinSet R (f g R R) E x in 8, f g
x) 2 S ( x in S, x 2) ( x in 8, X 2) := by
sorry
Round 8
theorem name (S Set R) (hS S. Finite) (f g S R)
S.toFinSet
g x) ~ < (E x in to
x 2)
3 x in S. toFinSet
x 2) := by sorry
Round 9
theorem tame {S Type*} [Fintype S] (f S RR ( 8,
f g x) 2 ( I 2) ( 5, 8 2) by sorry
31

---

Table 13: A successful case generated by ATLAS
Analysis: In the first two rounds, there were formalization errors in Lean syntax, while in rounds three and four, the formalization expressed overly strong semantics. However, in round five, the
formalization was done correctly.
Concept1: K[X]
euclidean ring when is a field
Domain1: Ring Theory
Concept2: inverse trigonometric functions
Domain2: Single Variable Real Analysis
statement: Let K field. For any polynomial f(X) K[X], there exists a polynomial g(X) E K[X] such that f(X) g(X) = if and only if s(x) is a constant polynomial. This property is analogous to the invertibility of non-zero constants in the context of inverse trigonometric functions.
statements:
Round
theorem tm_name {K Type*} [Field x] (f Polynomial K) (3 (g
Polynomial K) Polynomial mul f g = 1 1 +>
f.coeffs.all all ((*))+0) => 0) by sorry
Round 2
theorem
{K Type*) [Field x] (f K[X)) (3 g K[x], * *g- + f (1
K) = by sorry
Round 3
theorem tame {K Type*} [Field K] (f PPolyooial K) () g Polynomial K, f g 1) = 1=ivve
sorry
Round
theorem tm_eame {K Type*} [Field K] (f Polynomial K) (3 g Polynomial K, g 1) ==1 := by sorry
Round 5
theorem name (K Type*) [Field K] (f Polynomial K) (3 g
Polynomial K, g 1) (3 c K, Polyyomiall. c) by sorry
32

---

Table 14: failed case generated by ATLAS
Analysis:
The model was unable to conrectly formalize the concept of a Gaussian integer ring.
Concept1: field C of complex numbers
Domain1:
Ring Theory
Concept2: greatest common divisor
Domain2: Ring Theory
NL statement: Let a and 3 be non-zero elements in the ring of Gaussian
integers Z[i]. Then the greatest common divisor ged(a, 3) in Z[i] is Gaussian integer of the form 7 = yi, where and y integers.
statements:
Round
theorem tm_name {a C} (he : IsAlgebraic a) (h : IsMonic Polynomial map (algebraMap z C) (x c a)))
IaBuclideanDomain (Z(a)) by sorry
Round
theorem sm_name (a z[i)) (ha : a 0) (h3 8 # 0) 3 x
2, 3 7 : Z[il, +++ * I A 7 ged B := by sorry
Round 3
theorem tm_nam (a B Z[i]) (ha a a 0) (h3 8 0) 3 12
il, 7 ged a 3 3 y 2, 7
:= by sorry
Round
theorem tm name (a B[i]) (ha : a a 0) (h3 8 0) (y :
[i]) (x 2), xty A ged a B : by sorry
Round 5
theorem name (a B[i]) (ha a 0) (h3 8 3 (y & [i]) (x y Z), x A ged B by sorry
Round
theorem tm. name (a Z[i]) (ha a 0) (h3 8 0) 3 12 i], 3 x 2, (x, y) A = ged a $ : by sorry
Round 7
theorem tm_na name (a Z[i]) (ha i1, 7 ged a 8 by sorry
0) (h3 8 0) 3 12
Round
theorem tm tm_nare name (a Z[i]) (ha : a a 0) (h3 : 8 0) 12
i], = ged a B A 3 x y : Z, x := by sorry
Round 9
theorem name (a 2[i]) (ha # 0) (h3 88 0) 3 12 il. 7 ged a B by sorry
Round
theorem tm name (a 2[i)) (ha : a # 0) (h3 * 0) 3 12
i], ged a 3 := by sorry
33

---

Table 13: A failed case generated by ATLAS
Analysis:
The model unable formalize such relatively complex problem, and there were also certain issues with the natural language statement itself.
Concepti: Taylor's theorem with Lagrange form for remainder
Domain1: Single Variable Real Analysis
Concept2: affine function
Domain2: Affine and Euclidean Geometry
NL statement: For function f that is + interval containing and the Taylor polynomial of degree at approximates f(x with an error term that can be expressed as an affine function of (x (
times differentiable
FL statements:
Round 1
theorem tm_name (n N) (f R - (hf x, (x E Set Icc
-> HasFDerivAt (f' x) f x) (x R) (hx x Set Ice a : :3
c : R, f taylorPolynomial n a ffr c (x a) (n 1)
by sorry
Round 2
theorem tm (a R) (n N) (f R+R) (hf 4 x, f =
in range (n 1), (f~[i] (x - 11))
R
f x E in range (n 1), (f-[i] a (x a) i i!)
(x a) (n 1) : by sorry
Round 3
theorem tame (n N) (a xax: : R (hf 4 k N, k - Differentiableln Icc x)) ccc R x iteratedDeriv n fa c (x a) (n 1) = by sorry
(fun => iteratedDeriv n x) (Set.
Round 4
theorem
name (n N)
(a R) (f R+ (hf ContDiff R (n
+ f) 3 k R (f a in FinSet FinSet. range (n 1).
(f [i a (x a) i 1 (i 1)1)) * (x a)
1) : by sorry
Round 5
theorem tm_name (f : : (n N) (a B) (hf ContDiff R (n
1) f) f 2 8 fx= (x a) +g (x
(n+ by sorry
Round 6
theorem tm. name (f R +) (a x R) (n N) (hf : ContDiff R (n
+ 1) f) 3 k R, xx=
(f) a)
(x a) (1 (Nat.
factorial (n + 1))) (f (n 1) a) (x a) (n 1) +
(x a)
1) :- by sorry
Round 10
theorem tame (n N) (a R) (f - (hf K N. k
DifferentiableDn R (fun deriv [k] 1 x) (Set.Ie a))
3 p R +R, vx: E, x by sorry
(n 1)
34

---

Prompt Templates
This section presents all the prompts used to facilitate the reproducibility of our work.
Prompt Template for Statements Translation (DeepSeek-) V33)
Please autoformalize the following problem in Lean 4 with header. Use the following theorem names: tm nama. Respond strictly with the translation, without any additional explanation. An'n
Prompt Template for Back-Translattee Translation
the formal statement into natural language:'n" 44JJo[UNNSED__OOE)) 146jassistantln
Prompt Template for NLI Check
You experienced mathematics expert and educator with extensive experience in mathematical problem analysis. need you to analyze the fundamental nature of the following two mathemattcal problems.
# Focus
1. Core mathematical concepts and principles
Problem-solvee approaches and methodologies
3. Ultimate objectives of the problems
# Ignore:
Variations in wording
2. Changes in contextual scenarios
# Present your answer using exactly this format: AnalysistnInsert your analysis here
# Conclusion\nreply llsamell or lldifferentll with "II" format
# Please approach this analysis with professional rigor. Math Problem 1: (informal_sse |
Math Problem 2:
Prompt Template for NL Statements Generation
You are an expert mathematics professor tasked with creating proof problems for undergradu- ate mathematics majors. Your assignment is to construct a proof problem that integrates [conceptl] from [domainl] and (concept2) from (domain2).
Requirements:
1. Create concise theorem appropriate for undergraduate mathematics majors.
The theorem should be brief, not exceeding 50 words.
3. Incorporate both specified concepts into the theorem naturally.
State the theorem clearly and concisely.
5. Ensure the theorem is simple enough be easily translated into Lean4.
Format exactly:
AnswerlnInsert your problem with "I[" format, i.e. ITTherre:: Insert the theorem natural language here.
35

---

Prompt Template for NI. Statements Translation (ATLASS)
You expert in the Lean4 theorem prover. Your task is translate theorems from natural language into formal Lean4 statements. Please follow these guidelines:
1. Carefully analyze the given theorem in natural language. Translate into correct and precise Lean4 formal statement.
3. Use the following format for your response: theorem tm name: The theorem's Lean4 formal statement by sorry
4. Focus solcly on the translation. Do not attempt to prove the theorem or provide additional explanations.
5. Ensure that your translation accurately captures all the mathematical concepts and relationships expressed the natural language version.
6. Use appropriate Lean4 syntax, including correct use of quantifiers, implications, and mathematical symbols.
7. If the theorem involves specific mathematical structures (e.g.. groups, rings, topological spaces), use the corresponding Lean4 definitions and notations.
Remember, the goal is to create a syntactically correct and semantically accurate formaliza- tion in Lean4. Your translation should be faithful to the meaning of the original theorem while adhering to Lean4 conventions and best practices.
Now please begin by carefully reading the natural language statement provided, and then proceed with your translation into Lean4.
Prompt Template for FL Statements Revision
You math expert and expert in Lean4. Your task is modify the Lean4 code based on the given natural language description of a theorem, the corresponding Lean4 code, and the error message from the Lean compiler.
Requirements:
1. Correct the Lean4 code to make it compile successfully.
Lean4 code may lack or have additional declarations of certain content. You can add or remove them as much as possible to keep it consistent with the natural language description. No need to import any packages, because Mathlib will be imported by default import Mathlib.
Carefully read the content and provide your modified answer: =*leean4 code*wAn w\n forral _statement] \m= Compiler error messageso*'n cooppllermemmttee wwweeerrrrraarpeeeeeee /n* language statements=in
Format exactly:
# AnalysisInInsert your analysis here Answer'nInsset your revised Lean4 code with "I"" format, i.e. lltheorem tm name your revised Lean4 code here := by sorryll
36

---

Prompt Template for FL. Statements Alignment
You math expert and expert in Lean4. Your task is check the alignment between the given natural language description of theorem and the corresponding Lean4 code.
Requirements:
Determine whether the Lean4 code is missing declarations of certain entities.
2. Assess whether the Lean4 code accurately represents the theorem described in the natural language.
3. Carefully read the content and provide your answer: **Lean4 code*sIn [for- mal mal_statement/ (ilatement\lnwwnauurs /nnauuraall language statementwwin (innorrml_ssaaeeenane
Format exactly:
# Analysis:AnInsers your analysis here
Answerlnreply llgoodll, llaveragell or lipoorl!
Prompt Template for FL. Statements Translation
You are math expert and an expert in Lean4. Your task is to translate theorems from Lean4 code into natural language.
Requirements:
1. Focus solely on the translation. Do not attempt to prove the theorem or provide additional explanations.
2. The theorem's natural language statement should be brief, not exceeding 50 words. Carefully analyze the given theorem Lean4 code (formal statement] ) and provide your translation in natural language.
Format exactly:
AnswerknInsert your translation with "Il" format, i.c. I1Theorem: Insert the theorem in natural language here.
37


Reviews:
[{"review_id": "TpAB6PewjE", "reviewer": "Reviewer_z8Zj", "summary": "The paper proposes ATLAS, a framework for autoformalizing mathematical theorems by generating high-quality parallel datasets of natural and formal statements. Starting from Mathlib concepts, it uses data lifting, synthesis, and augmentation (via proofs and contraposition) to build a 117k-statement dataset. The resulting ATLAS Translator outperforms prior models like HERALD and Kimina on benchmarks, achieving new state-of-the-art results with less data and no human supervision.", "questions": "- As a core baseline, HERALD benchmarked heavily on MiniF2F. I was wondering what is the performance of ATLAS on it (MiniF2F)?", "limitations": "yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Pros\n- Well written paper, easy to follow. I especially appreciate the super illustrative examples in the appendix that qualitatively explain the error types.\n- Amazing performance with super affordable compute budget (i.e., one A100).\n\nCons:\n- Each of the component does not appear super novel: data lifting (MUSTARD), synthesis (MMA, ProofNet, Lean Workbook), augmentation (DeepSeek-Prover). Nevertheless, the authors did a good job to put everything together.\n- Despite briefly mentioned, I believe slightly more comparisons against MUSTARD [1] and RAutoformalizer [2] might be worthy.\n\n[1] Huang, Yinya, et al. \"Mustard: Mastering uniform synthesis of theorem and proof data.\" arXiv preprint arXiv:2402.08957 (2024).\n\n[2] Liu, Qi, et al. \"Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach.\" The Thirteenth International Conference on Learning Representations. 2025.", "was_revised": false, "final_justification": "", "rebuttal": "We sincerely thank you for your positive feedback on our paper's clarity and impressive performance-to-compute ratio. We also appreciate your constructive questions, which have helped us further strengthen the manuscript. Below, we address the points you raised.\n\n\n> **Q1: Performance on the miniF2F Benchmark**\n\n**A1:** Thank you for the excellent suggestion to evaluate our model on miniF2F. We agree that this is essential for a thorough comparison to the HERALD Translator baseline. In response, we have now evaluated the ATLAS Translator on it. \n\n**The results show that ATLAS Translator performs comparably to HERALD Translator on miniF2F, and significantly outperforms it on the other three benchmarks.** We also do not report results for Kimina-Autoformalizer as its training set includes the miniF2F benchmark.\n\n|Model|miniF2F|||ProofNet|||Putnam|||MathQual|||\n|-|-|-|-|-|-|-|-|-|-|-|-|-|\n||pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|\n|HERALD Translator|76.02%|93.44%|95.29%|31.43%|64.85%|78.57%|20.36%|52.56%|71.35%|10.92%|31.83%|45.33%|\n|Kimina-Autoformalizer|-|-|-|-|-|-|-|-|-|19.01%|38.97%|50.71%|\n|ATLAS Translator|77.25%|93.65%|95.90%|54.99%|80.86%|88.95%|42.49%|76.93%|87.86%|38.92%|67.31%|79.78%|\n\n**The ATLAS Translator is based on Deepseek-Prover-V1.5-7B-Base, full-parameter fine-tuned on the ATLAS dataset. Accordingly, all results reported throughout the paper have been updated to reflect this change.*\n\n\n> **Q2: Detailed Comparison to MUSTARD and RAutoformalizer**\n\n**A2:** Thank you for highlighting these two important works. Based on your suggestion, we have now added a more detailed discussion in Appendix A: Motivation, Limitation and Future Works.\n\n**MUSTARD:** MUSTARD [1] is a key inspiration for our work. **Our approach builds upon it by addressing two primary challenges, and our solutions to them represent the core innovations of our work.**\n\n1. **Data Sourcing:** MUSTARD sources concepts from Khan Academy Website, which can create a \"formalization bottleneck\" as some concepts lack a direct counterpart in Mathlib. To avoid this, ATLAS sources concepts exclusively from Mathlib, guaranteeing a valid formalization path for every statement from the start.\n\n2. **Generation Efficiency:** MUSTARD's reliance on costly GPT-4 correction loops is a high-cost, low-yield process, with over 90% of initial generations failing prover validation and ultimately producing only ~6k samples. In contrast, ATLAS's teacher-student distillation framework is highly efficient, dramatically lowering costs and enabling us to generate our much larger dataset of 117k high-quality pairs.  \n\n**RAutoformalizer:** RAutoformalizer [2] is a dependency-based retrieval approach. This is complementary to our work. **The key distinction is that ATLAS focuses on generating a high-quality training dataset from scratch, while RAutoformalizer improves performance by retrieving relevant premises at inference time.**\n\n- A promising future direction is to extend our work from formalizing individual statements to mathematical theories. We propose achieving this by integrating our ATLAS data generation framework with dependency-aware methods like RAutoformalizer.\n\n-  A concrete technical path involves restructuring our mathematical concept repository into a dependency-aware tree. During synthesis, we would generate data in a bottom-up, layer-by-layer fashion, explicitly preserving the logical dependencies between foundational axioms and more advanced theorems. The resulting structured dataset would be ideal for training next-generation autoformalization models, paving the way for true theory-level autoformalization.\n\n\nWe hope these clarifications and additions have fully addressed your concerns, and we are grateful for the opportunity to improve our paper based on your feedback.\n\n---\n\n[1] Huang, Yinya, et al. \"MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data.\" The Twelfth International Conference on Learning Representations. 2024.\n\n[2] Liu, Qi, et al. \"Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach.\" The Thirteenth International Conference on Learning Representations. 2025."}, {"review_id": "tZqi8VAP4m", "reviewer": "Reviewer_szrQ", "summary": "This paper presents ATLAS, an autoformalization framework designed to translate natural language mathematical theorems into formal language equivalents. ATLAS establishes its datasets through three key steps: data lifting, data augmentation, and data synthesis. Empirical results demonstrate that the ATLAS translator, which is fine-tuned on the curated ATLAS dataset, significantly outperforms existing baselines and achieves a new state-of-the-art performance.", "questions": "- Could the teacher model be further tuned by \"exploring more challenging autoformalization problems,\" potentially allowing the framework to evolve on its own?\n- In the experiments, only LoRA was used for fine-tuning the model. Given that the dataset size is relatively sufficient, what is the performance like when employing full-parameter fine-tuning?\n- I am also curious about the expert iteration stage within the framework. Specifically, it is possible to synthesize formal theorems based on the collected formal concepts, then transform them into natural language versions, followed by SFT training of the student model instead of the expert iteration. This approach could also be enhanced through data augmentation. What are the results of applying this method?", "limitations": "Yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 2, "strengths_and_weaknesses": "### Strengths\n- This paper focuses on a significant problem in the field of formal theorem proving.\n- The overall framework presented is both interesting and promising. Moreover, its generality has the potential to inspire further enhancements and applications.\n- The dataset created is of high quality, and experimental results indicate that the model fine-tuned on this collection of 117K data points can achieve results comparable to existing baselines, which are typically trained on much larger datasets.\n\n### Weaknesses\n- Compared to existing baselines, the ATLAS Translator does not demonstrate significant improvements, particularly on the ProofNet and PutnamBench datasets.\n- The ablation study reveals that the primary gains stem from the data synthesis of the teacher models, while the proposed data augmentation methods have somewhat less impact.\n- There is some concern regarding the validation pipeline. The existing methods [20, 24, 28] rely solely on automated theorem provers to verify the logical equivalence between formalization results and ground truths. This may be considerably easier than actually proving the theorems themselves (if not, please correct me). Therefore, it would be beneficial to consider incorporating this approach as an additional evaluation method.\n- While I agree that the correctness of a theorem may be secondary in certain contexts, many tasks involving LLM training for theorem proving necessitate the formalization of correct and provable theorems as training materials. Thus, it would be beneficial to report some results in this direction on a smaller test set.", "was_revised": true, "final_justification": "This paper addresses a critical problem in formal theorem proving. The proposed method and dataset are valuable contributions to the community, and I recommend accepting this paper.", "rebuttal": "Thank you for your detailed and insightful review of our paper. We are especially encouraged that you recognize the significance of the problem we are tackling and find our overall framework to be \"interesting and promising.\" We are particularly grateful for your observation that our high-quality dataset allows ATLAS Translator to achieve results comparable to baselines that use much larger training sets, which is a central point of our contribution. We also deeply appreciate your constructive critiques and thoughtful questions and  address each of your questions and comments in detail below.\n\n\n>**Q1: Limited Performance Gains and Full-Parameter Fine-Tuning**\n\n**A1:** Thank you for raising these critical points. To thoroughly investigate, we perform an expanded experiment. This involved fine-tuning three distinct base models on the ATLAS dataset: Llama3.1-8B-Instruct, DeepSeek-Prover-V1.5-7B-Base, and Qwen2.5-Coder-7B-Instruct, denoted as **ATLAS Translator (L), (D), and (Q)**, respectively-using both LoRA and **full-parameter (denoted by * )** fine-tuning methods, and benchmarking them against existing baselines. \n\n**These new results, using full-parameter fine-tuning, resolve the concern about limited performance gains.** Our best model, ATLAS Translator* (D), now establishes a new SOTA across all benchmarks:\n- On **ProofNet**, it boosts pass@1 performance over HERALD by **23 absolute points** (54.99% vs. 31.43%).\n- On **PutnamBench**, it **more than doubles** the pass@1 performance of HERALD (42.49% vs. 20.36%).\n- On **MathQual**, it **more than triples** the pass@1 performance of HERALD (38.92% vs. 10.92%).\n\nFurthermore, the results confirm your intuition: **full-parameter fine-tuning consistently and significantly outperforms LoRA across all three base models**. We have updated the paper to reflect this new SOTA performance.\n\n|Model|ProofNet|||Putnam|||MathQual|||\n|-|-|-|-|-|-|-|-|-|-|\n||pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|\n|HERALD Translator|31.43%|64.85%|78.57%|20.36%|52.56%|71.35%|10.92%|31.83%|45.33%|\n|Kimina-Autoformalizer|-|-|-|-|-|-|19.01%|38.97%|50.71%|\n|ATLAS Translator (L)|39.46%|67.28%|78.71%|23.16%|55.51%|72.93%|22.75%|45.85%|58.23%|\n|ATLAS Translator* (L)|47.98%|74.66%|86.52%|38.54%|73.29%|84.98%|40.22%|65.81%|75.48%|\n|ATLAS Translator (D)|39.51%|69.49%|81.62%|25.64%|59.03%|75.75%|24.30%|49.59%|63.74%|\n|ATLAS Translator* (D)|**54.99%**|**80.86%**|**88.95%**|**42.49%**|**76.93%**|**87.86%**|**38.92%**|**67.31%**|**79.78%**|\n|ATLAS Translator (Q)|40.70%|71.43%|84.10%|29.29%|66.77%|82.25%|28.17%|54.19%|68.17%|\n|ATLAS Translator* (Q)|50.67%|79.51%|86.25%|39.91%|76.93%|87.56%|37.63%|65.59%|76.34%|\n\n\n>**Q2: Additional Evaluation Method**\n\n**A2:** We sincerely thank you for this excellent suggestion to incorporate a more rigorous evaluation method. The three existing methods you mentioned are roughly introduced as follows:\n\n- The first method [1] is **specific to the Isabelle** theorem prover, relying on built-in tactics like `Sledgehammer`, `by presburger` and so on. \n- The second method [2] uses the Lean theorem prover to verify **bidirectional equivalence between the model's output and the ground truth**. It builds upon the heuristic tactic `exact?` by also employing a LLM to find the required proofs.\n- The third method [3], designed for the Lean theorem prover, is **restricted to the domain of Euclidean Geometry**. \n\nGiven the limitations of the other approaches, we adopt the second method (BEq@k, k=1,8) and re-evaluate all models on ProofNet. This results **further corroborate the conclusions from the LLM-as-a-Judge evaluation**, demonstrating that the full-parameter fine-tuned model achieves superior performance over both the LoRA-tuned variant and the HERALD baseline on this more rigorous metric. A detailed breakdown of this analysis will be included in the Appendix.\n\n|Model|BEq@1|BEq@8|\n|-|-|-|\n|HERALD Translator|4.58%|7.55%|\n|Kimina-Autoformalizer|-|-|\n|ATLAS Translator (L)|5.39%|9.16%|\n|ATLAS Translator* (L)|6.47%|9.97%|\n|ATLAS Translator (D)|5.66%|9.16%|\n|ATLAS Translator* (D)|6.74%|9.16%|\n|ATLAS Translator (Q)|5.93%|8.09%|\n|ATLAS Translator* (Q)|7.01%|8.89%|\n\n\n>**Q3: Verification of Theorem Correctness/Provability**\n\n**A3:** Thank you for this excellent suggestion. To address the crucial question of whether the formalized statements are provable, we conduct a preliminary study.\n\nWe **randomly sample 100 propositions** from the ATLAS dataset. To establish a ground truth for their provability, we employ a panel of experts, including DeepSeek-R1, Gemini 2.5 Pro, and human evaluators, to collectively assess the truth value of each proposition. This process results in a set of **60 true and 40 false** propositions by **self-consistency strategy**.\n\nFurthermore, we will expand this into a full discussion in the Appendix, rather than merely listing it as a limitation.\n\n\n>**Q4: Potential for Framework Self-Evolution**\n\n**A4:** This is an insightful question regarding the framework's long-term potential for autonomous improvement. We agree that enabling the system to evolve by tackling progressively more difficult problems is a critical direction for future work.\n\nOur **current framework already includes a foundational mechanism** for this: natural-language statements that the model **fails to formalize are re-introduced into the candidate pool for subsequent attempts**. This process implicitly increases the average task difficulty by exposing the model to its previous failures. \n\nBuilding directly on this principle, we plan to implement a **more explicit curriculum learning strategy for self-evolution** with two primary components:\n\n1. **Compositional Complexity:** We will structure the concept library as a graph or a tree, which allows us to systematically generate a curriculum of increasing difficulty. New theorems will be synthesized by progressively increasing both the conceptual distance between ideas (e.g., path length in the graph) and the total number of concepts required to form a valid statement.\n\n2. **Conceptual Hierarchy:** We will introduce a graded concept repository (e.g., high-school → undergraduate → graduate level). The model would need to demonstrate proficiency at one level before unlocking the next, creating a structured path to mastering more advanced topics.\n\nTogether, these mechanisms would enable the pipeline to autonomously generate a curriculum of increasing difficulty, creating a powerful virtuous cycle of self-improvement that does not depend on new external data or annotations.\n\n\n> **Q5: Discussion about Alternative Framework Designs**\n\n**A5:** Thank you for this excellent question regarding alternative framework designs. We did, in fact, explore a \"formal-first\" synthesis approach similar to what you described during our initial investigations. We ultimately chose our current \"natural-first\" ATLAS framework for two primary, empirically-grounded reasons:\n1. **High Cost and Low Yield of Formal Synthesis:** Our experiments confirm that directly synthesizing formal statements from concepts is highly inefficient. For instance, when we prompt DeepSeek-V3 to generate 300 formal statements, **only 2.3% (7 out of 300) successfully pass verification by the Lean 4 prover**. This extremely low yield makes the \"formal-first\" approach difficult and costly to scale.\n\n2. **LLM Proficiency and Data Scarcity**: This low success rate reflects a broader challenge: current LLMs are generally more proficient at generating fluent, diverse natural language than they are at producing syntactically and logically perfect formal code. This is partly due to the relative scarcity of formal mathematics corpora in their pre-training data compared to the vast amount of natural text. For instance, in the **math-related code corpus AlgebraicStack [4], Lean accounts for only 2.6% (285M/10955M).**\n\nIn contrast, our ATLAS framework strategically leverages the strengths of modern LLMs (their powerful natural language capabilities) and then uses the Lean prover as a targeted, efficient verifier. This design has proven to be a far more cost-effective and scalable method for generating the large, high-quality dataset that powers our SOTA results.\n\n\nOnce again, we sincerely thank you for your detailed and constructive feedback. Your suggestions have been instrumental in improving our work and we hope these revisions have fully addressed your concerns and questions.\n\n---\n\n[1] Li, Zenan, et al. \"Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency.\" The Thirty-eighth Annual Conference on Neural Information Processing Systems. 2024.\n\n[2] Liu, Qi, et al. \"Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach.\" The Thirteenth International Conference on Learning Representations. 2025.\n\n[3] Murphy, Logan, et al. \"Autoformalizing Euclidean Geometry.\" Forty-first International Conference on Machine Learning. 2024.\n\n[4] Azerbayev, Zhangir, et al. \"Llemma: An Open Language Model for Mathematics.\" The Twelfth International Conference on Learning Representations. 2024."}, {"review_id": "1CBrqTzLQO", "reviewer": "Reviewer_QRN1", "summary": "This paper presents ATLAS, a novel framework for autoformalization that aims to generate large-scale, qualitative parallel data in both natural and formal mathematical languages. By combining data lifting, synthesis, and augmentation, ATLAS builds a dataset of 117k undergraduate-level statements without manual annotation. The ATLAS translator performs well on multiple benchmarks, marking a meaningful advance in the automation of formal mathematics.", "questions": "See Weakness", "limitations": "Yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths:\n\nThe paper proposes ATLAS, an autoformalization framework with three core modules. This end-to-end design enables the efficient generation of large-scale parallel corpora in both NL and FL.\n\nBy extracting mathematical concepts directly from Mathlib and synthesizing corresponding NL statements, ATLAS avoids reliance on manual annotation or web-based corpus collection.\n\nWeakness:\n\nWhile ATLAS effectively addresses data scarcity and automates the generation of parallel corpora, its reliance on Mathlib and Lean4 limits its applicability to domains not covered by the library.\n\nThe method depends on backbone LLMs for NL synthesis and FL translation. In comparison to LLaMA, more sophisticated large language models, such as those in the Qwen series, could be investigated for potential improvements.\n\nWhen encountering other out of domain problems, how does the experiment of ATLAS perform? Maybe more analyses are preferred.", "was_revised": false, "final_justification": "", "rebuttal": "We sincerely thank you for your positive evaluation of our work, including the end-to-end design of the ATLAS framework for generating large-scale data and its ability to avoid manual annotation. We also wish to thank you for your insightful questions, which have helped us improve the clarity and scope of our paper. In what follows, we address each of the points you raised in detail.\n\n\n>**Q1: Reliance on Lean4/Mathlib**\n\n**A1:** We thank you for raising this important point. We agree that our current implementation is focused on the Lean/Mathlib ecosystem and would like to elaborate on the rationale for this decision and the broader applicability of our methodology.\n\n**Rationale for Mathlib:** Our choice to build upon Mathlib is strategic. As one of the largest and most comprehensive formal mathematics libraries, it provides an ideal foundation for developing and validating a large-scale autoformalization framework. Furthermore, leveraging established libraries is a standard and practical approach in the theorem-proving domain, as seen in prior work such as STP [1] and Lean Workbook [2]. This approach is necessitated by the fact that formalizing novel mathematical domains from scratch remains a formidable challenge for current large language models.\n\n**Generality beyond Lean:** We wish to clarify that the dependency on Lean is a characteristic of our current implementation, not a fundamental limitation of the ATLAS framework. The core principles of our framework—concept lifting, data synthesis, and data augmentation—are designed to be general. **This principled approach could be adapted to other proof assistants, such as Isabelle/HOL or Coq, provided a sufficiently structured library is available.** We will add a discussion to the paper to clarify this distinction and highlight the potential for future generalization.\n\n\n>**Q2: Choice of the Base Model**\n\n**A2:** We appreciate this insightful point. We **select LLaMA as our base model primarily to validate the effectiveness of our framework**. As stated in lines 216-217 of the paper, our objective is to specialize a general-purpose model into a Lean 4 expert. The underlying rationale is that **if our framework can successfully specialize a foundational model, it is expected to yield even more significant performance gains when applied to more advanced LLMs**.\n\nTo validate this hypothesis, we conduct a preliminary validation, as comprehensive experiments are not feasible during the brief rebuttal period. We fine-tune several different base models on the ATLAS dataset: Llama3.1-8B-Instruct, DeepSeek-Prover-V1.5-7B-Base, and Qwen2.5-Coder-7B-Instruct, denoted as **ATLAS Translator (L), (D), and (Q)**, respectively—using both LoRA and full-parameter **(denoted by * )** fine-tuning methods. As expected, the results indicate that **stronger models, such as the DeepSeek and Qwen series, achieve significant performance gains over the original LLaMA baseline when fine-tuned on ATLAS dataset**.\n\n|Model|ProofNet|||Putnam|||MathQual|||\n|-|-|-|-|-|-|-|-|-|-|\n||pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|\n|HERALD Translator|31.43%|64.85%|78.57%|20.36%|52.56%|71.35%|10.92%|31.83%|45.33%|\n|Kimina-Autoformalizer|-|-|-|-|-|-|19.01%|38.97%|50.71%|\n|ATLAS Translator (L)|39.46%|67.28%|78.71%|23.16%|55.51%|72.93%|22.75%|45.85%|58.23%|\n|ATLAS Translator* (L)|47.98%|74.66%|86.52%|38.54%|73.29%|84.98%|40.22%|65.81%|75.48%|\n|ATLAS Translator (D)|39.51%|69.49%|81.62%|25.64%|59.03%|75.75%|24.30%|49.59%|63.74%|\n|ATLAS Translator* (D)|**54.99%**|**80.86%**|**88.95%**|**42.49%**|**76.93%**|**87.86%**|**38.92%**|**67.31%**|**79.78%**|\n|ATLAS Translator (Q)|40.70%|71.43%|84.10%|29.29%|66.77%|82.25%|28.17%|54.19%|68.17%|\n|ATLAS Translator* (Q)|50.67%|79.51%|86.25%|39.91%|76.93%|87.56%|37.63%|65.59%|76.34%|\n\n\n>**Q3: Out-of-Domain (OOD) Performance**\n\n**A3:** This is a valuable question, and we thank you for raising it. To rigorously evaluate our model's generalization capabilities, we've tested it on a challenging out-of-domain benchmark.\n\nCon-NF [3] is an excellent OOD benchmark, as it's based on the Con(NF) library. Con(NF) is a recently published digitization of Randall Holmes’ proof that Quine’s New Foundations is consistent. The benchmark consists of **961 theorems based on a different theoretical basis from our training data source, Mathlib**, making it a true test of generalization. We evaluate our models and existing baselines on this benchmark and report the results below.\n\n- **vs. HERALD Translator:** To evaluate the effectiveness of ATLAS Translator, we first conduct a direct comparison against the **HERALD Translator, a strong baseline also trained on data derived from Mathlib**. Experimental results show that the **ATLAS Translator also performs better than the HERALD Translator**, even in the OOD benchmark.\n\n- **vs. Kimina-Autoformalizer:** Kimina-Autoformalizer achieves a strong **pass@8 score of 40.89%**. This level of performance is achieved by our ATLAS Translator with a **larger pass@32 budget**. We hypothesize that Kimina's strong performance is due to its training corpus, Numina Math 1.5 [4], which is a broad crawl of mathematical knowledge that may include texts on various set theories, including material related to New Foundations. Consequently, **Con-NF may not be a strictly out-of-domain benchmark for Kimina-Autoformalizer**.\n\nTherefore, we argue that ATLAS's performance is a more rigorous test of generalization capability. The ability to achieve a 40% success rate on a demonstrably unseen and conceptually distinct mathematical domain suggests that our framework learns foundational reasoning skills, not just domain-specific patterns. This stricter and more transparent approach to OOD evaluation is a key contribution of our work. A detailed breakdown of this analysis will be included in the Appendix.\n\n|Model|pass@1|pass@8|pass@32|\n|-|-|-|-|\n|HERALD Translator|3.43%|9.05%|14.26%|\n|Kimina-Autoformalizer|**9.37%**|**40.89%**|**68.16%**|\n|ATLAS Translator (L)|7.49%|22.89%|35.07%|\n|ATLAS Translator* (L)|7.28%|21.85%|37.77%|\n|ATLAS Translator (D)|6.04%|19.67%|33.51%|\n|ATLAS Translator* (D)|5.83%|20.40%|33.40%|\n|ATLAS Translator (Q)|7.70%|24.77%|42.98%|\n|ATLAS Translator* (Q)|6.66%|23.93%|37.25%|\n\nWe once again thank you for your constructive and insightful feedback. These additions will be fully integrated into the final manuscript. We hope our detailed responses have fully addressed your concerns, and we respectfully hope for your support.\n\n---\n\n[1] Dong, Kefan, and Tengyu Ma. \"STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving.\" Forty-second International Conference on Machine Learning. 2025.\n\n[2] Ying, Huaiyuan, et al. \"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems.\" The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track. 2024.\n\n[3] Liu, Qi, et al. \"Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach.\" The Thirteenth International Conference on Learning Representations. 2025.\n\n[4] Li, Jia, et al. \"Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions.\" Hugging Face repository 13.9 (2024): 9."}, {"review_id": "5QvSG3ANLx", "reviewer": "Reviewer_eSpp", "summary": "The paper tackles the problem of autoformalization, which is the process of translating informal mathematical statements into equivalent formal statements. The work primarily focuses on the Lean language, but the pipeline is generalizable to other languages. The main contribution of the paper is a concept-repository-based approach to synthetic data generation with augmentation. The authors also present a new autoformalization model, ATLAS, which achieves higher translation accuracy on a variety of datasets.", "questions": "Based on the Weaknesses section, here are my questions:\n\n- How can we ensure the originality and sufficient diversity of the augmentation-via-proof method?\n- How can we ensure and minimize hallucinations that might occur at various stages of the pipeline?\n- How can we guarantee (to some limited degree) the mathematical correctness of the synthetic data?\n\nand a suggestion:\n- Please provide some preliminary comparisons with HERALD and the Kimina Autoformalizer on the miniF2F dataset.", "limitations": "Please review Strengths/Weaknesses section.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "## **Strengths**\n\n**Scalable synthetic data generation.** The work introduces two augmentation techniques with minimal inference cost, which contribute to more useful data points in training.\n\n**Concept-based synthetic data.** The work introduces a concept repository that leads to a more diverse set of samples across a variety of topics and, more importantly, their intersections.\n\n**Human-labelling-free fine-tuning.** The pipeline does not involve a human in the loop, which makes the proposed method easier to integrate and scale.\n\n## **Weaknesses**\n\n\n**Lack of miniF2F comparison.** HERALD translator reaches a very high accuracy of 93.2% on miniF2F, while this work lacks comparison on this dataset. It would be interesting to see the accuracy of ATLAS with a pass128 sampling budget on miniF2F-test/valid.\n\n**High reliance on LMs to generate, curate, correct, and verify the synthetic data.** I understand that the field of formal mathematics is notorious for its lack of quality data, but the pipeline leans heavily on LMs to do the heavy lifting. In this pipeline, I see numerous points of failure where it may generate faulty or misleading data.\n\nDuring NL statement generation from randomly sampled concepts, LMs may hallucinate, and the final result may omit one of the specified concepts. However, this is a mild weakness that is not a major obstacle, since even incorrect or unsolvable NL statements can be formalized. More importantly, ATLAS uses a teacher model to curate and correct the generated statements. How can we be sure that the teacher model is capable of rewriting and correcting the student model’s mistakes based on compiler feedback, which may also be incomplete (since the compiler stops at the first major error) or misleading (due to the ambiguity of some raised errors)? My main concern is that the teacher model might hallucinate, alter the problem statement, or even trivialize the problem just to pass the compiler check.\n\n**Augmentation via proof.** The authors use prover outputs (such as DSP-v1.5) to augment statements based on the applied tactics. Although this can yield more data through rewriting and the introduction of new hypotheses, it can also clutter the data pool. Provers like DSP-v1.5, as shown in [1], often produce short proofs that rely on built-in solvers, and the applied rewrites are frequently minor or do not substantially affect the NL statements (e.g., $a = b^{-1}$ vs. $a = \\frac{1}{b}$ when using the simp tactic). Consequently, this augmentation method leads to high redundancy. It would be interesting to evaluate to what extent this specific technique contributes novel, sufficiently different data points. I believe that augmentation by proof is not as effective as contraposition augmentation.\n\n**No correctness verification of synthetic data.** I understand the authors’ argument that NL- and FL-correctness is secondary in translation tasks and more relevant to formal theorem proving, and that verifying correctness requires proofs, which are scarce and hard to generate. However, since we cannot verify whether these statements are provable, we potentially have many misleading or unprovable statements in the training pool, which the model then uses to learn. How can we ensure some level of correctness in synthetically generated statements?\n\nIf we deploy ATLAS in an end-to-end informal-to-formal theorem-proving pipeline, the likelihood of hallucination increases, and the translator may inject wrong or unprovable statements it encountered in the training data. Even though this may not hurt the translator itself (in the context of translation tasks), it introduces risks in the theorem-proving process. As discussed in [2], factual inconsistencies in the dataset increase the likelihood of bias, misinformation, and other artifacts of unverified data. We face hallucinations even with clean, curated datasets; an unverified dataset poses even greater risks for downstream tasks and applications. I recommend deploying more safety guards against producing faulty data (e.g., multiple LLM judges to reduce hallucination or other safeguard methods)\n\n[1] R. Yousefzadeh, X. Cao, A. Ospanov. A lean dataset for international math olympiad: Small steps towards writing math proofs for hard problems. Transactions on Machine Learning Research, 2025.\n\n[2] A. Paullada, I. D. Raji, E. M. Bender, E. Denton, A. Hanna. Data and its (dis)contents: A survey of dataset development and use in machine learning research. Patterns, 2021.\n\n## **Minor typo remarks**\n\n- In line 41, “impose” should be changed to “imposes”.\n\n- In line 504, “translat” should be “translate”.", "was_revised": true, "final_justification": "After reviewing the rebuttal and responses to other reviewers, I am more positively inclined toward ATLAS. I especially appreciated the experiment on training different model baselines, such inclusions strengthen the work. My recommendations for the authors:\n\n- Update the empirical results section to include the new results\n- Expand the discussion of the “correctness” of the translation task; I believe it is a critical point that should be carefully addressed\n\nIn light of this, I raise my score to 4.", "rebuttal": "We sincerely thank you for your thorough and detailed review. We appreciate your positive feedback on our scalable, concept-based data generation pipeline and its human-labelling-free design. We have taken your feedback seriously, and in what follows, we provide experimental results and detailed analyses to address each of your concerns.\n\n\n>**Q1: Performance on the miniF2F Benchmark**\n\n**A1:** Thank you for the excellent suggestion to evaluate our model on miniF2F. We agree that this is essential for a thorough comparison to the HERALD Translator baseline. In response, we have now evaluated the ATLAS Translator on it. \n\n**The results show that ATLAS Translator performs comparably to HERALD Translator on miniF2F, and significantly outperforms it on the other three benchmarks.** We also do not report results for Kimina-Autoformalizer as its training set includes the miniF2F benchmark.\n\n|Model|miniF2F|||ProofNet|||Putnam|||MathQual|||\n|-|-|-|-|-|-|-|-|-|-|-|-|-|\n||pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|pass@1|pass@8|pass@32|\n|HERALD Translator|76.02%|93.44%|95.29%|31.43%|64.85%|78.57%|20.36%|52.56%|71.35%|10.92%|31.83%|45.33%|\n|Kimina-Autoformalizer|-|-|-|-|-|-|-|-|-|19.01%|38.97%|50.71%|\n|ATLAS Translator|77.25%|93.65%|95.90%|54.99%|80.86%|88.95%|42.49%|76.93%|87.86%|38.92%|67.31%|79.78%|\n\n**The ATLAS Translator is based on Deepseek-Prover-V1.5-7B-Base, full-parameter fine-tuned on the ATLAS dataset. Accordingly, all results reported throughout the paper have been updated to reflect this change.*\n\n**The latest HERALD's paper shows that the pass@128 results on minif2f-test and minif2f-valid are 96.7% and 96.3% respectively. Considering that the performance of pass@32 has reached 95.29% and the significance of pass@128 in practical use, we do not test pass@128.*\n\n\n>**Q2: Diversity of Augmentation-via-Proof**\n\n**A2:** Thank you for this insightful question. We agree that the diversity of the augmented data is crucial. In our work (lines 206-208), we **conceptualize each proofstep as a transformation. Ideally, a proposition that has undergone more transformations would be maximally different from the original**. And we take the augmented proposition corresponding to the last proofstep.\n\nHowever, you correctly point out a key limitation: this theoretical ideal is constrained by the practical capabilities of current automated theorem provers and some trivial tactics. Following your suggestion, we **conduct a new analysis to measure the diversity generated by each strategy**. We randomly sample 100 statements and calculate the BLEU score between the original and augmented versions. In this context, **a lower BLEU score indicates greater textual diversity**. Our analysis yielded the following results:\n- Augmentation-via-Proof: Average BLEU = **0.6709**\n- Augmentation-via-Contraposition: Average BLEU = **0.6026**\n\nThese results validate your hypothesis: our current implementation of **Augmentation-via-Proof produces less textually diverse data than Augmentation-via-Contraposition**. This is a valuable finding that provides a clear path for improvement and we will enhance this augmentation method. Specifically, we will implement **stricter filtering by disallowing augmentations generated from trivial proof tactics** (such as simple rewrites with `simp`) and **enforcing a diversity threshold using a metric like Levenshtein distance** to ensure only sufficiently novel statements are added to the training pool.\n\nWe thank you for this constructive suggestion. We will incorporate this new analysis and a detailed discussion into the Appendix A to strengthen the paper's discussion of limitations and future work.\n\n\n>**Q3: Concerns about Cheating the Compiler**\n\n**A3:** This is a critical point, and we appreciate you raising it. We agree that the compiler feedback is not always comprehensive and the teacher model may generate hallucinations to cheat the Lean 4 compiler. However, we design our methodology specifically to prevent this type of \"reward hacking.\" To ensure the integrity of our synthetic data, we implement a **two-stage validation process** that all generated data must pass:\n\n1. **Syntactic Check:** First, the modified formal code is verified for correctness by the Lean 4 compiler. This is the stage where simple cheating could occur.\n\n2. **Semantic Check**: Second, a powerful verifier model confirms a strict semantic alignment between the compiled formal statement and the original natural language problem.\n\nThis dual-check process directly mitigates the risk you've identified. Any attempt by the teacher model to **trivialize or alter the problem to pass the syntactic check would be caught and rejected during the subsequent semantic fidelity check**, as the meaning would no longer match the original intent.\n\n\n>**Q4: Correctness Verification of Synthetic Data**\n\n**A4:** It is important to clarify, as stated in Section 3.1 “Correctness” of the paper, that in the field of Statement Autoformalization, the correctness of the mathematical statements themselves is not the most critical factor. Nevertheless, training models on corpora that contain incorrect statements does pose certain risks for downstream tasks, such as automated theorem proving task. To address this issue, the following **two approaches** can be adopted:\n\n1. **Judging from NL:** The correctness of the proposition is judged from the perspective of NL through multiple LLMs, and if false, a counterexample should be given. The comprehensive results of multiple LLMs are called **self-consistency methods**, thereby reducing the likelihood of generating incorrect statements.\n2. **Proving from FL:** Another common practice is to use **automated theorem provers** (such as Deepsee-Prover-V2 and Goedel-Prover-V2) to prove directly from FL. If the statement can be successfully proved, its correctness is thereby ensured. \n\n\nOnce again, we thank you for your time and for the insightful feedback that has helped us to significantly strengthen our paper. We hope these new results and clarifications have addressed your concerns, and we respectfully hope for your support."}]

Author rebuttal:

Meta-review: This paper gives treatment to autoformalization. The authors responded very well to the concerns by the reviewers, and the paper now I believe is ready to be published. The author also did significant additional work during the rebuttal to improve the paper.
Decision: Accept (poster)