Leandojo Lean4 Tacgen Byt5 Small

🚀 LeanDojo：檢索增強語言模型的定理證明

LeanDojo是一個利用檢索增強語言模型進行定理證明的項目，它在定理證明領域具有重要價值，能有效提升定理證明的效率和準確性。

🚀 快速開始

請訪問 LeanDojo 官網 以獲取詳細信息。

📄 許可證

本項目採用 MIT 許可證。

📚 詳細文檔

推理參數

示例

以下是一個示例：

• 文本："a b : ℕ\n⊢ a + b = b + a"
• 示例標題："Example"

引用信息

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