Improve language tag

README.md

@@ -1,23 +1,35 @@
----
-license: apache-2.0
-datasets:
-- SJTULean/LeanStatement_SFT
-language:
-- en
-result:
-  dataset:
-    type: Formalizer Lean
-    name: miniF2F
-  metrics:
-    - name: pass@1
-      type: pass@1
-      value: 0.9406
-      verified: false
-base_model:
-- Qwen/Qwen2.5-7B-Instruct
----
-# LeanFormalizer_SFT
-
-<!-- Provide a quick summary of what the model is/does. -->
-
-Based on Qwen2.5-7b and trained on our LeanStatement_SFT dataset, our model achieves **state-of-the-art** performance in formal mathematics verification, with a **pass@1 compilation success rate** of 94.1% (459/488) on MiniF2F and 75.4% (282/374) on ProofNet benchmarks as of December 2024(while our PPO model achieves 95.3% on MiniF2F and 76.0% on Proofnet). These results demonstrate the effectiveness of scaling laws in mathematical formalization using the Lean theorem prover.
+---
+license: apache-2.0
+datasets:
+- SJTULean/LeanStatement_SFT
+language:
+- zho
+- eng
+- fra
+- spa
+- por
+- deu
+- ita
+- rus
+- jpn
+- kor
+- vie
+- tha
+- ara
+result:
+  dataset:
+    type: Formalizer Lean
+    name: miniF2F
+  metrics:
+  - name: pass@1
+    type: pass@1
+    value: 0.9406
+    verified: false
+base_model:
+- Qwen/Qwen2.5-7B-Instruct
+---
+# LeanFormalizer_SFT
+
+<!-- Provide a quick summary of what the model is/does. -->
+
+Based on Qwen2.5-7b and trained on our LeanStatement_SFT dataset, our model achieves **state-of-the-art** performance in formal mathematics verification, with a **pass@1 compilation success rate** of 94.1% (459/488) on MiniF2F and 75.4% (282/374) on ProofNet benchmarks as of December 2024(while our PPO model achieves 95.3% on MiniF2F and 76.0% on Proofnet). These results demonstrate the effectiveness of scaling laws in mathematical formalization using the Lean theorem prover.