🚀 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。