수학 문장을 Lean 4 코드로 바꿀 때, 정답 라이브러리를 찾아주고 컴파일러가 틀린 곳을 짚어주면 8B짜리 작은 모델도 32B급을 이긴다
arXiv:2608.142212026-08-14
MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
수학 문장을 Lean 4 코드로 바꿀 때, 정답 라이브러리를 찾아주고 컴파일러가 틀린 곳을 짚어주면 8B짜리 작은 모델도 32B급을 이긴다
자연어로 쓰인 수학 문제를 컴퓨터가 검증할 수 있는 Lean 4 코드로 자동 변환하는 작업(오토포멀라이제이션)은 단순 번역이 아니라 Mathlib이라는 방대한 수학 라이브러리의 정의와 규칙을 정확히 매핑해야 하는 문제다. 이 논문은 생성 전에 관련 라이브러리 지식을 검색해 주고, 생성 후에는 컴파일 오류와 의미 일치 여부를 확인해 반복적으로 고쳐나가는 MathForm 파이프라인을 만들어 약 36만7천 개의 검증된 데이터셋 FormalVerse를 구축했다. 이 데이터로 학습한 MathForm-8B는 6개 벤치마크에서 평균 문법통과율 88.06%, 의미일치통과율 72.37%를 기록하며 여러 32B급 전문 모델을 앞섰다.
METAL MEDIA 해설 도표
수학 문장을 Lean 4 코드로 바꿀 때, 정답 라이브러리를 찾아주고 컴파일러가 틀린 곳을 짚어주면 8B짜리 작은 모델도 32B급을 이긴다
01기존 방식은 모델이 외운 지식에만 의존해 존재하지 않는 정리를 인용하거나 라이브러리 관례에 어긋나는 코드를 만드는 문제가 있었고, 데이터 구축도 대량 생성 후 걸러내는 방식이라 실패 원인을 알려주지 못했다
02MathForm은 생성 전 Mathlib에서 관련 정의·정리를 검색해주는 계획자와, 컴파일 진단 및 의미일치 판정(QwQ-32B가 심사)을 받아 최대 3라운드까지 고쳐나가는 반복 정제 구조를 갖췄고, 최종적으로 GPT류 판정 모델(gpt-oss-120b)로 다시 검증했다
03이렇게 만든 FormalVerse 데이터로 Qwen3-8B를 지도학습(SFT) 후 강화학습(DAPO)까지 거쳐 MathForm-8B를 학습시켰다
04결과적으로 어려운 FATE-H, FATE-X 벤치마크에서 의미일치통과율 63%, 37%를 기록해 기존 최강 전문 모델보다 각각 10, 12포인트 높았고, 추상 대수처럼 라이브러리 지식이 많이 필요한 영역일수록 격차가 커졌다
05동일 데이터 규모(10만 개)로 비교했을 때 FormalVerse로 학습한 모델이 다른 공개 Lean 4 데이터셋보다 의미일치통과율에서 최대 18.83포인트 앞섰다
METAL MEDIA이 원문을 바탕으로 재구성한 해설 도표이며, 논문 저자의 원문 figure가 아닙니다.
무엇을 했나
기존 방식은 모델이 외운 지식에만 의존해 존재하지 않는 정리를 인용하거나 라이브러리 관례에 어긋나는 코드를 만드는 문제가 있었고, 데이터 구축도 대량 생성 후 걸러내는 방식이라 실패 원인을 알려주지 못했다
MathForm은 생성 전 Mathlib에서 관련 정의·정리를 검색해주는 계획자와, 컴파일 진단 및 의미일치 판정(QwQ-32B가 심사)을 받아 최대 3라운드까지 고쳐나가는 반복 정제 구조를 갖췄고, 최종적으로 GPT류 판정 모델(gpt-oss-120b)로 다시 검증했다
이렇게 만든 FormalVerse 데이터로 Qwen3-8B를 지도학습(SFT) 후 강화학습(DAPO)까지 거쳐 MathForm-8B를 학습시켰다
결과적으로 어려운 FATE-H, FATE-X 벤치마크에서 의미일치통과율 63%, 37%를 기록해 기존 최강 전문 모델보다 각각 10, 12포인트 높았고, 추상 대수처럼 라이브러리 지식이 많이 필요한 영역일수록 격차가 커졌다
동일 데이터 규모(10만 개)로 비교했을 때 FormalVerse로 학습한 모델이 다른 공개 Lean 4 데이터셋보다 의미일치통과율에서 최대 18.83포인트 앞섰다
Figure 1: Macro-average Pass@8 (%) across six benchmarks among specialized autoformalizers. MathForm-8B achieves the strongest overall performance within this category despite its smaller model size.
Table 1: Pass@8 pass rates (%) under Syntax Check (SC) and Consistency Check (CC) for specialized autoformalizers on six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. For each column, the best result is shown in bold and the second best is underlined.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Model
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
Specialized Autoformalizers
Herald Translator-7B
64.12
27.63
95.29
47.76
78.74
37.36
77.00
5.00
70.67
54.67
42.00
15.00
21.00
6.00
Kimina-Autoformalizer-7B
73.20
34.37
99.29
76.24
96.55
56.32
95.00
16.00
77.33
44.67
43.00
8.00
28.00
5.00
Mathesis-HPO-7B
76.20
34.96
99.06
79.29
97.13
59.77
96.00
15.00
84.00
48.67
50.00
4.00
31.00
3.00
StepFun-Formalizer-7B
58.12
39.55
97.41
81.41
89.66
59.20
79.00
28.00
60.67
52.67
17.00
12.00
5.00
4.00
StepFun-Formalizer-32B
63.65
44.47
99.06
85.88
92.53
64.94
86.00
32.00
71.33
60.00
23.00
17.00
10.00
7.00
Goedel-Formalizer-V2-8B
78.24
60.08
98.82
94.12
98.28
89.66
89.00
42.00
87.33
82.67
62.00
44.00
34.00
8.00
Goedel-Formalizer-V2-32B
78.28
63.74
99.06
94.59
98.28
92.53
91.00
49.00
89.33
85.33
63.00
48.00
29.00
13.00
ReForm-8B
81.76
66.21
99.06
94.12
98.85
90.80
86.00
47.00
94.67
91.33
67.00
53.00
45.00
21.00
ReForm-32B
81.61
68.41
99.06
95.53
98.28
94.25
93.00
55.00
91.33
88.67
69.00
52.00
39.00
25.00
Ours
MathForm-8B-SFT
84.38
66.53
99.29
91.06
100.00
90.80
83.00
43.00
98.00
91.33
80.00
58.00
46.00
25.00
MathForm-8B
88.06
72.37
100.00
95.06
100.00
94.83
93.00
47.00
99.33
97.33
82.00
63.00
54.00
37.00
Figure 2: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm-8B.
Table 2: Ablation results for SC and CC pass rates (%) of the refinement pipeline with two generators on the FATE series. Single denotes single-pass generation; BoN denotes Best-of-N; Feedback denotes feedback-only iteration; and Retrieval denotes retrieval-only single-pass generation. AVG is the equally weighted average over FATE-M, FATE-H, and FATE-X.
AVG
FATE-M
FATE-H
FATE-X
Method
SC
CC
SC
CC
SC
CC
SC
CC
gpt-oss-120b
Single
27.33
26.43
52.00
51.30
21.00
19.00
9.00
9.00
BoN
42.67
41.10
70.00
69.30
40.00
37.00
18.00
17.00
Feedback
42.57
40.77
68.70
67.30
41.00
38.00
18.00
17.00
Retrieval
32.23
29.00
56.70
52.00
27.00
26.00
13.00
9.00
MathForm
49.67
48.00
76.00
74.00
46.00
44.00
27.00
26.00
Qwen3-235B-A22B-Thinking-2507
Single
7.43
7.43
13.30
13.30
5.00
5.00
4.00
4.00
BoN
18.77
18.77
33.30
33.30
14.00
14.00
9.00
9.00
Feedback
28.77
28.77
51.30
51.30
22.00
22.00
13.00
13.00
Retrieval
9.90
8.57
16.70
16.70
8.00
6.00
5.00
3.00
MathForm
37.57
36.23
60.70
58.70
32.00
31.00
20.00
19.00
Figure 3: Distribution of natural-language problem sources in FormalVerse.
Table 3: Pass@8 SC and CC pass rates (%) of models trained on different datasets across six benchmarks. All models are initialized from Qwen3-8B and trained on 100K examples under the same trajectory reconstruction and training configuration. AVG is the equally weighted macro-average across all six benchmarks. The best result in each column is shown in bold and the second best is underlined.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Training Dataset
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
NuminaMath-LEAN
66.24
41.49
99.53
85.18
96.55
72.41
87.00
25.00
69.33
49.33
35.00
16.00
10.00
1.00
FineLeanCorpus
78.25
46.53
100.00
84.47
98.85
74.71
96.00
29.00
90.67
68.00
53.00
17.00
31.00
6.00
FormalVerse
77.17
60.32
98.82
90.59
98.85
89.66
78.00
36.00
95.33
84.67
62.00
46.00
30.00
15.00
Figure 4: Numbers of natural-language-to-formal-language pairs accepted in successive refinement rounds. Later rounds contribute an additional 31.0% of all retained pairs.
Table 4: Judge-model reliability on the human-annotated semantic-consistency test set (Mean@3).
Judge Model
Accuracy
Precision
Recall
F1
gpt-oss-120b
0.8917
0.8755
0.9133
0.8940
QwQ-32B
0.8567
0.8367
0.8867
0.8609
gpt-oss-20b
0.8500
0.8142
0.9067
0.8579
Figure 5: Training dynamics during reinforcement learning. The left panel shows the training reward and its exponential moving average (EMA), while the right panel reports the Mean@3 pass rate on FATE-H over the course of training.
Table 5: Supervised fine-tuning hyperparameters.
Hyperparameter
Value
Maximum sequence length
16,384
Global batch size
128
Learning rate
2.0×10−5
Epochs
3
LR scheduler
Cosine
Warmup ratio
0.1
Precision
bf16
Figure 6: Category distribution of the natural-language mathematical problems in FormalVerse.
Table 7: Pass@8 SC and CC pass rates (%) of general-purpose LLMs and MathForm-8B across six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. The best result in each column is shown in bold and the second best is underlined.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Model
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
General-Purpose LLMs
DeepSeek-V4-Pro
78.34
76.54
97.88
96.24
94.83
93.68
85.00
81.00
87.33
87.33
70.00
68.00
35.00
33.00
Qwen3.7-Plus
86.33
83.38
99.29
98.59
100.00
97.70
92.00
87.00
94.67
92.00
78.00
77.00
54.00
48.00
Qwen3-235B-A22B-Thinking-2507
58.94
55.37
91.29
88.24
81.03
75.29
59.00
50.00
71.33
70.67
32.00
30.00
19.00
18.00
Qwen3-32B
43.07
36.55
80.94
72.94
61.49
50.00
43.00
27.00
46.00
43.33
20.00
19.00
7.00
7.00
DeepSeek-R1-0528-Qwen3-8B
47.28
37.65
72.24
61.18
52.30
40.23
36.00
15.00
36.00
30.00
4.00
4.00
4.00
1.00
Qwen3-8B
27.25
17.06
61.88
42.12
37.93
27.59
29.00
7.00
26.67
22.67
4.00
3.00
4.00
0.00
Ours
MathForm-8B
88.06
72.37
100.00
95.06
100.00
94.83
93.00
47.00
99.33
97.33
82.00
63.00
54.00
37.00
Table 8: Human-evaluation results (%) on FATE-M and FATE-H, based on one randomly sampled candidate per problem. The best result in each column is shown in bold.
FATE-M
FATE-H
Model
SC
CC
SC
CC
StepFun-Formalizer-32B
42.67
36.00
16.00
12.00
Goedel-Formalizer-V2-32B
75.33
68.00
38.00
27.00
ReForm-32B
78.67
74.00
50.00
41.00
MathForm-8B
86.67
76.67
54.00
42.00
왜 중요한가
수학 정리증명 AI를 키우려면 사람이 손으로 만들기 힘든 대량의 검증된 형식 언어 데이터가 필요한데, 이 연구는 그 데이터를 자동으로, 더 정확하게 만드는 방법을 보여준다. 작은 모델도 좋은 데이터와 검증 파이프라인만 있으면 훨씬 큰 모델을 능가할 수 있다는 점은 비용 효율적인 AI 개발에 시사하는 바가 크다.
이 논문의 용어
오토포멀라이제이션(Autoformalization) · 자연어로 된 수학 문장을 Lean 같은 컴퓨터 검증 가능한 형식 언어로 자동 변환하는 작업
Lean 4 / Mathlib · 수학 정리를 컴퓨터가 검증할 수 있게 코드로 표현하는 증명 보조 언어(Lean)와 그 안의 방대한 정의·정리 라이브러리(Mathlib)
Syntax Check / Consistency Check · 생성된 코드가 문법적으로 컴파일되는지 확인하는 검사(SC)와, 원래 자연어 문장의 의미를 제대로 담고 있는지 확인하는 검사(CC)
Pass@8 · 한 문제당 8번 시도해서 몇 번이나 성공하는지를 비율로 나타낸 평가 지표
DAPO / 강화학습(RL) · 모델이 만든 여러 후보 답을 비교해 더 나은 답을 만들도록 보상 신호로 학습을 조정하는 방법
