腾讯 发布 HUNYUANPROVER数据集 数据集, 应用在 自动定理证明、自然语言处理 领域

腾讯 本次发布的数据集 HUNYUANPROVER数据集, HUNYUANPROVER数据集由腾讯混元团队创建，旨在解决自动定理证明中的数据稀缺问题。该数据集包含30,000条数据实例，每条实例包括自然语言中的原始问题、自动形式化转换后的陈述以及由HunyuanProver生成的证明。数据集的生成过程涉及从130,000条高质量的自然语言到LEAN格式的陈述对开始，通过自动形式化模型将3000万条内部数学问题转换为形式化陈述，并经过多轮迭代生成证明数据。该数据集的应用领域主要集中在自动定理证明，旨在通过大规模数据生成和迭代优化提升定理证明模型的性能。

查看HUNYUANPROVER数据集

关于 腾讯 , 腾讯是一家全球领先的互联网科技公司，提供多种互联网增值服务、网络广告服务以及金融科技服务。其产品和服务包括社交平台、数字内容、在线游戏、云计算等，广泛应用于全球用户。

关于 arXiv , arXiv 是一个免费分发服务和开放获取的学术文章档案库，涵盖了物理学、数学、计算机科学、定量生物学、定量金融、统计学、电气工程和系统科学以及经济学等领域。该网站上的材料并未经过 arXiv 的同行评审。