许可证: mit
推理参数:
最大长度: 1024
示例输入:

• 文本: "a b : ℕ\n⊢ a + b = b + a"
  示例标题: "示例"

LeanDojo: 基于检索增强语言模型的定理证明
NeurIPS（数据集与基准测试赛道），2023年
杨开宇、Aidan Swope、Alex Gu、Rahul Chalamala、
宋培阳、余世兴、Saad Godil、Ryan Prenger、Anima Anandkumar

@inproceedings{yang2023leandojo,
    title={{LeanDojo}: 基于检索增强语言模型的定理证明},
    author={杨开宇 and Swope, Aidan and Gu, Alex and Chalamala, Rahul and 宋培阳 and 余世兴 and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
    booktitle={Neural Information Processing Systems (NeurIPS)},
    year={2023}
}

详情请访问LeanDojo官方网站。