XiaoyangLiu-sjtu/ATLAS_Translator_L

Overview

ATLAS_Translator_L is an 8 billion parameter model, fine-tuned from Llama-3.1-8B-Instruct by XiaoyangLiu-sjtu. Its primary function is to translate natural language mathematical theorems into precise Lean4 formal statements. This model was developed using full-parameter fine-tuning on the ATLAS dataset, specifically designed for this translation task.

Key Capabilities

• Natural Language to Lean4 Translation: Translates mathematical theorems expressed in natural language into their formal Lean4 equivalents.
• Lean4 Syntax Adherence: Generates syntactically correct Lean4 code, including appropriate use of quantifiers, implications, and mathematical symbols.
• Mathematical Concept Preservation: Accurately captures mathematical concepts and relationships from the natural language input.
• Instruction-Following: Designed to follow a specific instruction format for translation, ensuring consistent and precise output for Lean4 theorem proving.

Good For

• Formal Verification: Assisting mathematicians and developers in formalizing theorems for use with the Lean4 theorem prover.
• Educational Tools: Aiding students and researchers in understanding and generating Lean4 formalizations from natural language descriptions.
• Automated Theorem Proving Workflows: Integrating into systems that require automated translation of mathematical statements into a formal language like Lean4.