Coqllm FineTuned Experiment Gen0

🚀 CoqLLM-FineTuned-Experiment-Gen0

このモデルは形式的定理証明の分野における実験であり、Coqコードの生成と解釈に特化しています。10,000以上のCoqソースファイルから得られた包括的なデータセットを活用することで、CoqLLM-FineTuned-Experiment-Gen0は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))

✨ 主な機能

• Coqコードの生成: 与えられた命題に対して、Coqの証明コードを生成することができます。
• Coqコードの解釈: Coqコードの構文と意味を理解し、適切な出力を生成することができます。

📦 インストール

このモデルを使用するには、必要なライブラリをインストールする必要があります。以下のコマンドを使用して、必要なライブラリをインストールしてください。

pip install transformers torch peft

📚 ドキュメント

モデルの詳細

モデルのソース

• 論文: 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データセットを使用してファインチューニングされています。ファインチューニングの過程では、許容的なライセンスを持つエントリのみが使用されました。

📄 ライセンス

このモデルは、bigcode-openrail-mライセンスの下で提供されています。

引用

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