Luogu-Llama-3-8B-Prover

Model Description

Luogu-Llama-3-8B-Prover is a large language model developed by luogu-llm-research, built upon Meta AI's Llama 3 8B Instruct model through continued pre-training or fine-tuning. This model is optimized for mathematical reasoning, natural language to formal mathematical representations, and math-related text generation. It excels at transforming natural language descriptions of mathematical concepts into structured formats, such as equations, formal definitions, or proof outlines, making it a powerful tool for mathematical exploration and formalization.

The model was trained on a diverse dataset, including mathematical texts, problem descriptions, formal proofs, and aligned natural language-to-mathematical code pairs. Notably, the Lean-related data used for training was distilled from Lumen Inspector, a specialized system designed for high-quality Lean code generation and verification. This distillation process enhances the model’s ability to produce precise and syntactically correct Lean code when formal mathematical outputs are required.

Carbon Neutrality Commitment

luogu-llm-research is committed to environmental sustainability. The training and deployment of Luogu-Llama-3-8B-Prover were conducted with energy-efficient hardware and optimized training pipelines to minimize carbon emissions. Carbon emissions associated with model training were offset through certified carbon credits, ensuring carbon-neutral development. We continue to explore greener computing practices to support sustainable AI development.

Intended Use

Luogu-Llama-3-8B-Prover is designed for a variety of mathematical applications, including but not limited to:

• Natural Language to Mathematical Formalization: Converting natural language descriptions of mathematical problems, theorems, or concepts into structured formats, such as equations, formal definitions, or proof outlines (e.g., translating "Prove that for any real number ( x ), ( x^2 ) is non-negative" into a formal proof structure).
• Mathematical Code Generation: Generating code for mathematical computations or formal systems, including definitions, theorems, or proof sketches compatible with formal environments like Lean.
• Math-Related Text Generation: Producing clear, accurate explanations, examples, or descriptions of mathematical concepts, theorems, or problem-solving strategies.
• Educational Support: Serving as an intelligent assistant for students, educators, and researchers learning or teaching mathematical reasoning and formalization.
• Problem-Solving Assistance: Aiding users in breaking down complex mathematical problems into manageable steps or suggesting approaches to proofs and computations.

Limitations and Risks

While Luogu-Llama-3-8B-Prover is highly capable, it has limitations that users should be aware of:

• No Guarantee of Mathematical Correctness: As a language model, it generates outputs based on patterns in training data, not formal logical reasoning. Generated proofs, equations, or code may contain errors, omissions, or logical inconsistencies.
• Challenges with Advanced Mathematics: The model may struggle with highly abstract, specialized, or cutting-edge mathematical topics not well-represented in its training data.
• Ambiguity in Natural Language: Ambiguous or poorly specified inputs may lead to misinterpretations, resulting in incorrect or irrelevant outputs.
• Training Data Bias: Performance may vary across mathematical domains depending on the coverage and quality of the training data, including the Lean data distilled from Lumen Inspector. Certain areas or problem styles may be over- or under-represented.
• Inherited Limitations: The model inherits potential biases, hallucinations, or limitations from the Llama 3 8B Instruct base model, which may affect output quality.
• Safety Considerations: While primarily designed for mathematical tasks, misuse of the model to generate misleading or incorrect mathematical content is possible. Responsible use and verification are essential.

Model Information

• Base Model: Meta AI Llama 3 8B Instruct
• Model Size: 8 billion parameters
• Developer: luogu-llm-research
• Training Data: A curated dataset including:
  • Mathematical texts (e.g., problem statements, theorems, proofs, textbooks)
  • Natural language descriptions paired with formal mathematical representations
  • Code snippets from formal mathematical environments, with Lean-related data distilled from Lumen Inspector to ensure high-quality, syntactically correct Lean code
  • General mathematical discourse from forums, tutorials, and documentation
• Carbon Footprint: Training was conducted on energy-efficient infrastructure, with carbon emissions offset through certified carbon credits to achieve carbon neutrality.

How to Get Started

Luogu-Llama-3-8B-Prover can be used via the Hugging Face transformers library with PyTorch or other compatible frameworks. Below is an example of how to load and use the model for mathematical tasks:

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch

model_id = "luogu-llm-research/Luogu-Llama-3-8B-Prover"

tokenizer = AutoTokenizer.from_pretrained(model_id)

model = AutoModelForCausalLM.from_pretrained(
    model_id,
    torch_dtype=torch.bfloat16,
    device_map="auto",
)

messages_math = [
    {"role": "system", "content": "You are an assistant that converts natural language mathematical statements into formal representations or proofs."},
    {"role": "user", "content": "Prove that for any real number \( x \), \( x^2 \) is non-negative."}
]

messages_code = [
    {"role": "system", "content": "You are an assistant that generates mathematical code or formal definitions."},
    {"role": "user", "content": "Define a function to compute the factorial of a natural number."}
]

messages_explain = [
    {"role": "system", "content": "You are a mathematical assistant that explains concepts clearly."},
    {"role": "user", "content": "Explain the difference between a field and a ring in algebra."}
]

# Select a task (e.g., math formalization)
messages = messages_math

# Prepare input using chat template
input_ids = tokenizer.apply_chat_template(
    messages,
    add_generation_prompt=True,
    return_tensors="pt"
).to(model.device)

# Define termination tokens
terminators = [
    tokenizer.eos_token_id,
    tokenizer.convert_tokens_to_ids("<|eot_id|>")
]

# Generate response
outputs = model.generate(
    input_ids,
    max_new_tokens=1024, # Adjust based on output length
    eos_token_id=terminators,
    do_sample=True,
    temperature=0.7, # Controls randomness
    top_p=0.9,      # Controls sampling diversity
)

# Decode and print response
response = outputs[0][input_ids.shape[-1]:]
decoded_response = tokenizer.decode(response, skip_special_tokens=True)

print("Generated Output:")
print(decoded_response)

Adjust generation parameters (max_new_tokens, temperature, top_p, etc.) based on your specific needs and hardware constraints.

License

This model is based on Meta AI's Llama 3 and is subject to the Llama 3 License. Please review and comply with the official Llama 3 license terms before using this model.