kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small

Model

0

stars

5

commits

1

linked in READMEs

Jul 16, 2024

updated

endpoints_compatible

transformers

README

Tactic generation model in CTranslate2 format, generated by:

pip install ctranslate2
ct2-transformers-converter --model kaiyuy/leandojo-lean4-tacgen-byt5-small --output_dir ct2-leandojo-lean4-tacgen-byt5-small

Contributors

4 commits

KY

1 commits

Similar repos

kaiyuy/ct2-leandojo-lean4-retriever-byt5-small

1

kaiyuy/ct2-byt5-small

0

Yale-LILY/a2cu-generator

0

jadohu/LlamaGen-T2I-2

2

emozilla/NTK-Llama-2-7b-8k

0

HuggingFaceH4/tiny-random-LlamaForCausalLM

2

jadohu/LlamaGen-T2I

0

uer/t5-small-chinese-cluecorpussmall

21

Linked in READMEs

lean-dojo/LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

1,322

kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small

Model

0

stars

5

commits

1

linked in READMEs

Jul 16, 2024

updated

endpoints_compatible

transformers

README

Tactic generation model in CTranslate2 format, generated by:

pip install ctranslate2
ct2-transformers-converter --model kaiyuy/leandojo-lean4-tacgen-byt5-small --output_dir ct2-leandojo-lean4-tacgen-byt5-small

Similar repos

kaiyuy/ct2-leandojo-lean4-retriever-byt5-small

1

kaiyuy/ct2-byt5-small

0

Yale-LILY/a2cu-generator

0

jadohu/LlamaGen-T2I-2

2

emozilla/NTK-Llama-2-7b-8k

0

HuggingFaceH4/tiny-random-LlamaForCausalLM

2

jadohu/LlamaGen-T2I

0

uer/t5-small-chinese-cluecorpussmall

21

Linked in READMEs

lean-dojo/LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

1,322

Contributors

4 commits

KY

1 commits