Tactic generation model in ONNX format, generated by:

from optimum.onnxruntime import ORTModelForSeq2SeqLM

ORTModelForSeq2SeqLM.from_pretrained(
    "kaiyuy/leandojo-lean4-tacgen-byt5-small", export=True
).save_pretrained("onnx-leandojo-lean4-tacgen-byt5-small")