Coqllm FineTuned Experiment Gen0

🚀 CoqLLM 微調實驗初代模型卡片

CoqLLM-FineTuned-Experiment-Gen0 是一個專注於形式定理證明領域的實驗模型，專門用於生成和解釋 Coq 代碼。該模型藉助從 10000 多個 Coq 源文件中提取的綜合數據集，在理解 Coq 獨特的語法和語義方面表現出更高的熟練度，從而推動了自動定理證明的重要進展。

✨ 主要特性

• 基於大規模 Coq 代碼數據集進行微調，對 Coq 語法和語義理解能力強。
• 可用於生成和解釋 Coq 代碼，助力自動定理證明。

📦 安裝指南

文檔未提供具體安裝步驟，故跳過此章節。

💻 使用示例

基礎用法

import torch
from transformers import AutoTokenizer, AutoModelForCausalLM, BitsAndBytesConfig
import sys
from peft import PeftModel

base_model_id = "mistralai/Mistral-7B-v0.1"
bnb_config = BitsAndBytesConfig(
    load_in_4bit=True, bnb_4bit_use_double_quant=True,
    bnb_4bit_quant_type="nf4", bnb_4bit_compute_dtype=torch.bfloat16
)

base_model = AutoModelForCausalLM.from_pretrained(
    base_model_id, quantization_config=bnb_config,
    device_map="auto", trust_remote_code=True,
)

eval_tokenizer = AutoTokenizer.from_pretrained(
    base_model_id, add_bos_token=True, trust_remote_code=True)

ft_model = PeftModel.from_pretrained(
    base_model, "florath/CoqLLM-FineTuned-Experiment-Gen0")

eval_prompt = "Lemma plus_n_O : forall n:nat, n = n + 0."

model_input = eval_tokenizer(eval_prompt, return_tensors="pt").to("cuda")

ft_model.eval()
with torch.no_grad():

    for idx in range(10):
    
        res = eval_tokenizer.decode(
            ft_model.generate(
                **model_input,
                max_new_tokens=50,
                do_sample=True,
                temperature=0.4,
                pad_token_id=eval_tokenizer.eos_token_id,
                repetition_penalty=1.15)[0], skip_special_tokens=False)
				
	    print("Result [%2d] [%s]" % (idx, res))

高級用法

文檔未提供高級用法示例，故跳過此部分。

📚 詳細文檔

模型詳情

模型來源

• 論文：Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
• 數據集：florath/coq-facts-props-proofs-gen0-v1

使用說明

提示格式

無需特殊提示格式。模型使用 Coq 源代碼進行微調，只需提供命題，模型即可生成證明，例如：

Lemma plus_n_O : forall n:nat, n = n + 0.

無需特殊字符或分隔符。

直接使用

CoqLLM-FineTuned-Experiment-Gen0 是一個展示微調數據集有效性的實驗模型。該模型可用於檢查是否能自動生成簡短證明，也可用於整理現有 Coq 源代碼並生成新的 Coq 源代碼。

適用範圍外使用

該模型不適用於定理證明和形式驗證領域之外的通用語言任務。濫用情況包括但不限於非 Coq 編程任務、技術文檔之外的自然語言處理，或在關鍵系統中未經充分監督和驗證的任何形式部署。

偏差、風險和侷限性

該模型繼承了其基礎模型和訓練數據的偏差，可能反映出所收集 Coq 文件的多樣性不足。用戶在將模型應用於定理證明的新領域或服務不足的領域時，應警惕這些侷限性。

建議

為降低風險和偏差，建議在使用模型時輔以人工監督，或在可自動驗證生成的 Coq 源代碼的環境中使用。建議持續監控意外行為或輸出，並努力使訓練數據集多樣化和擴展，以涵蓋更廣泛的 Coq 使用場景。

訓練詳情

該模型使用 florath/coq-facts-props-proofs-gen0-v1 數據集進行微調。微調過程僅使用了具有寬鬆許可證的條目。

引用

@misc{florath2024enhancing,
      title={Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code}, 
      author={Andreas Florath},
      year={2024},
      eprint={2403.12627},
      archivePrefix={arXiv},
      primaryClass={cs.AI}
}

📄 許可證

本模型使用的許可證為 bigcode-openrail-m。