Coqllm FineTuned Experiment Gen0

🚀 CoqLLM-FineTuned-Experiment-Gen0

CoqLLM-FineTuned-Experiment-Gen0 is an experiment in formal theorem proving, designed to generate and interpret Coq code. Leveraging a dataset from over 10,000 Coq source files, it shows improved proficiency in Coq's syntax and semantics, advancing automated theorem proving.

✨ Features

• Specialized in formal theorem proving with Coq code.
• Enhanced understanding of Coq syntax and semantics through fine - tuning.
• Capable of generating and interpreting Coq code for theorem - proving tasks.

📦 Installation

No specific installation steps are provided in the original document.

💻 Usage Examples

Basic Usage

No special prompt format is needed. The model was fine - tuned with Coq source code. Just provide a proposal to let the model generate a proof, like:

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

Advanced Usage

Here is a code snippet using the fine - tuned model. The shown setup should work using GPUs with <= 24GByte RAM. You might want to adapt and experiment with different settings, like different temperatures.

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))

📚 Documentation

Model Details

Model Sources

• Paper: Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
• Dataset: florath/coq-facts-props-proofs-gen0-v1

Uses

Prompt Format

No special prompt format is required. The model was fine - tuned with Coq source code. Just providing a proposition allows the model to generate a proof.

Direct Use

CoqLLM-FineTuned-Experiment-Gen0 is an experiment to demonstrate the usefulness of the fine - tuning dataset. It can be used to check if short proofs can be automatically generated and to curate and generate new Coq source code.

Out - of - Scope Use

The model is not intended for general - purpose language tasks outside theorem proving and formal verification. Misuse includes non - Coq programming tasks, natural language processing outside technical documentation, or deployment in critical systems without adequate supervision and validation.

Bias, Risks, and Limitations

The model inherits biases from its base model and training data, potentially reflecting the diversity or lack thereof in the collected Coq files. Users should be aware of these limitations, especially when applying the model in new or underserved areas of theorem proving.

Recommendations

To mitigate risks and biases, it is recommended to use human oversight or an environment where the generated Coq source code can be automatically verified. Continuous monitoring for unexpected behaviors or outputs is advised, along with efforts to diversify and expand the training dataset to cover a broader range of Coq use cases.

Training Details

The model was fine - tuned with the florath/coq-facts-props-proofs-gen0-v1 dataset. Only entries with permissive licenses were used during the fine - tuning process.

Cite

@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}
}

📄 License

The model is licensed under bigcode - openrail - m.