haielab
/

STP_model_Lean_0320-conjecture-base-FineTune-new-config

@@ -1,199 +1,104 @@
 ---
 library_name: transformers
-tags: []
 ---
-# Model Card for Model ID
-<!-- Provide a quick summary of what the model is/does. -->
 ## Model Details
-### Model Description
-<!-- Provide a longer summary of what this model is. -->
-This is the model card of a 🤗 transformers model that has been pushed on the Hub. This model card has been automatically generated.
-- **Developed by:** [More Information Needed]
-- **Funded by [optional]:** [More Information Needed]
-- **Shared by [optional]:** [More Information Needed]
-- **Model type:** [More Information Needed]
-- **Language(s) (NLP):** [More Information Needed]
-- **License:** [More Information Needed]
-- **Finetuned from model [optional]:** [More Information Needed]
-### Model Sources [optional]
-<!-- Provide the basic links for the model. -->
-- **Repository:** [More Information Needed]
-- **Paper [optional]:** [More Information Needed]
-- **Demo [optional]:** [More Information Needed]
 ## Uses
-<!-- Address questions around how the model is intended to be used, including the foreseeable users of the model and those affected by the model. -->
-### Direct Use
-<!-- This section is for the model use without fine-tuning or plugging into a larger ecosystem/app. -->
-[More Information Needed]
-### Downstream Use [optional]
-<!-- This section is for the model use when fine-tuned for a task, or when plugged into a larger ecosystem/app -->
-[More Information Needed]
-### Out-of-Scope Use
-<!-- This section addresses misuse, malicious use, and uses that the model will not work well for. -->
-[More Information Needed]
-## Bias, Risks, and Limitations
-<!-- This section is meant to convey both technical and sociotechnical limitations. -->
-[More Information Needed]
-### Recommendations
-<!-- This section is meant to convey recommendations with respect to the bias, risk, and technical limitations. -->
-Users (both direct and downstream) should be made aware of the risks, biases and limitations of the model. More information needed for further recommendations.
-## How to Get Started with the Model
-Use the code below to get started with the model.
-[More Information Needed]
-## Training Details
-### Training Data
-<!-- This should link to a Dataset Card, perhaps with a short stub of information on what the training data is all about as well as documentation related to data pre-processing or additional filtering. -->
-[More Information Needed]
-### Training Procedure
-<!-- This relates heavily to the Technical Specifications. Content here should link to that section when it is relevant to the training procedure. -->
-#### Preprocessing [optional]
-[More Information Needed]
-#### Training Hyperparameters
-- **Training regime:** [More Information Needed] <!--fp32, fp16 mixed precision, bf16 mixed precision, bf16 non-mixed precision, fp16 non-mixed precision, fp8 mixed precision -->
-#### Speeds, Sizes, Times [optional]
-<!-- This section provides information about throughput, start/end time, checkpoint size if relevant, etc. -->
-[More Information Needed]
-## Evaluation
-<!-- This section describes the evaluation protocols and provides the results. -->
-### Testing Data, Factors & Metrics
-#### Testing Data
-<!-- This should link to a Dataset Card if possible. -->
-[More Information Needed]
-#### Factors
-<!-- These are the things the evaluation is disaggregating by, e.g., subpopulations or domains. -->
-[More Information Needed]
-#### Metrics
-<!-- These are the evaluation metrics being used, ideally with a description of why. -->
-[More Information Needed]
-### Results
-[More Information Needed]
-#### Summary
-## Model Examination [optional]
-<!-- Relevant interpretability work for the model goes here -->
-[More Information Needed]
-## Environmental Impact
-<!-- Total emissions (in grams of CO2eq) and additional considerations, such as electricity usage, go here. Edit the suggested text below accordingly -->
-Carbon emissions can be estimated using the [Machine Learning Impact calculator](https://mlco2.github.io/impact#compute) presented in [Lacoste et al. (2019)](https://arxiv.org/abs/1910.09700).
-- **Hardware Type:** [More Information Needed]
-- **Hours used:** [More Information Needed]
-- **Cloud Provider:** [More Information Needed]
-- **Compute Region:** [More Information Needed]
-- **Carbon Emitted:** [More Information Needed]
-## Technical Specifications [optional]
-### Model Architecture and Objective
-[More Information Needed]
-### Compute Infrastructure
-[More Information Needed]
-#### Hardware
-[More Information Needed]
-#### Software
-[More Information Needed]
-## Citation [optional]
-<!-- If there is a paper or blog post introducing the model, the APA and Bibtex information for that should go in this section. -->
-**BibTeX:**
-[More Information Needed]
-**APA:**
-[More Information Needed]
-## Glossary [optional]
-<!-- If relevant, include terms and calculations in this section that can help readers understand the model or model card. -->
-[More Information Needed]
-## More Information [optional]
-[More Information Needed]
-## Model Card Authors [optional]
-[More Information Needed]
-## Model Card Contact
-[More Information Needed]

 ---
 library_name: transformers
+pipeline_tag: text-generation          # causal-LM generation
+language:
+  - en                                 # natural language comments
+  - code                               # Lean proof language (= non-natural)
+base_model: kfdong/STP_model_Lean_0320
+datasets:
+  - stp_lean_theorems                  # rename if your JSON file differs
+metrics:
+  - train_loss
+  - eval_loss
+tags:
+  - lora
+  - peft
+  - causal-lm
+  - theorem-proving
+  - stp
+  - flash-attn-2
+  - bf16
+new_version: v1.0
 ---
+# STP-Lean-7B LoRA (v1)
+LoRA rank-16 adapter fine-tuned from **`kfdong/STP_model_Lean_0320`** to assist with Lean theorem proving.
+---
 ## Model Details
+| Field | Value |
+|-------|-------|
+| **Developed by** | HAIE Lab |
+| **Model type** | 7 B-parameter causal-LM + LoRA r 16 α 32 |
+| **Languages** | Lean syntax & English commentary |
+| **Finetuned from** | `kfdong/STP_model_Lean_0320` |
+| **Precision** | BF16 · Flash-Attention v2 |
+| **Context length** | 1792 tokens |
+| **Hardware** | 1 × H100 80 GB |
+---
+### Results  (1 epoch, STP Lean corpus)
+| Metric                    | Value |
+|---------------------------|-------|
+| Final **train loss**      | **1.1593** |
+| Final **train accuracy**  | **0.713 token-level** |
+| First-step loss (warm-up) | 1.6084 |
+| Tokens processed          | 168 856 138 |
+| Grad-norm (final)         | 0.265 |
+---
 ## Uses
+### Direct Use
+Interactive Lean-proof suggestions, theorem exploration, education.
+### Downstream Use
+Research on automated theorem proving.
+### Out-of-Scope
+Open-domain advice, legal/medical claims, guaranteed proof correctness.
+---
+## Bias, Risks & Limitations
+Model may hallucinate or output invalid Lean code; inherits errors in the STP dataset.
+---
+## How to Get Started
+```python
+from transformers import AutoTokenizer, AutoModelForCausalLM
+model_id = "haielab/STP_model_Lean_0320-conjecture-base-FineTune-new-config"
+# 1️⃣  Tokenizer ─ leave default right padding for STP
+tok = AutoTokenizer.from_pretrained(model_id, trust_remote_code=True)
+tok.pad_token = tok.eos_token         # STP uses </s> as PAD
+# 2️⃣  Load base-plus-LoRA adapter on GPU (BF16)
+model = AutoModelForCausalLM.from_pretrained(
+    model_id,
+    torch_dtype="bfloat16",
+    device_map="auto"                 # auto-dispatch to available GPU(s)
+)
+# 3️⃣  Build a Lean-style prompt
+prompt = "<user>Theorem foo …</user><assistant>"
+inputs = tok(prompt, return_tensors="pt").to(model.device)
+# 4️⃣  Generate the next proof steps
+out = model.generate(
+        **inputs,
+        max_new_tokens=256,
+        temperature=0.7,
+        top_p=0.9,
+)
+print(tok.decode(out[0], skip_special_tokens=True))