Leandojo Lean4 Tacgen Byt5 Small

🚀 LeanDojo: 検索拡張言語モデルによる定理証明

LeanDojoは、検索拡張言語モデルを用いた定理証明に関するプロジェクトです。この技術は、定理証明の分野に新たなアプローチを提供します。

🚀 クイックスタート

LeanDojoの詳細については、LeanDojoのウェブサイトをご覧ください。

📄 ライセンス

このプロジェクトはMITライセンスの下で公開されています。

論文情報

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
NeurIPS (Datasets and Benchmarks Track), 2023
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala,
Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar

@inproceedings{yang2023leandojo,
    title={{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
    author={Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
    booktitle={Neural Information Processing Systems (NeurIPS)},
    year={2023}
}

推論パラメータ

ウィジェットの例

• テキスト: "a b : ℕ\n⊢ a + b = b + a"
• 例のタイトル: "Example"