中国科学院数学与系统科学研究院 发布 CombiBench 数据集, 应用在 组合数学、自动定理证明 领域

中国科学院数学与系统科学研究院 本次发布的数据集 CombiBench, CombiBench是一个包含100个组合数学问题的综合基准测试集，每个问题都使用Lean 4进行了形式化，并配有相应的非正式描述。问题集涵盖了从初中到IMO和大学水平的各种难度，涵盖了十多个组合数学主题。CombiBench旨在解决自动定理证明领域中组合数学缺乏适当基准和定理库的问题。该数据集包含了自2000年以来所有IMO组合数学问题（除了2004年的第3题，因为其陈述包含图像）。此外，我们提供了一个全面的标准评估框架，称为Fine-Eval，用于形式数学的评估。它不仅适用于基于证明的问题，而且首次支持对填空题的评估。使用Fine-Eval作为评估方法，并以Kimina Lean Server为后端，我们在CombiBench上对几个LLM进行了基准测试，并观察到它们在形式化解决组合数学问题方面的能力仍然有限。在所有测试的模型中（没有一个是为这个特定任务训练的），Kimina-Prover取得了最佳结果，在“有解决方案”和“无解决方案”的情况下都解决了7个问题（共100个）。我们开源了基准数据集以及所提出的评估方法的代码。

查看CombiBench

关于 中国科学院数学与系统科学研究院 , 中国科学院数学与系统科学研究院是中国科学院直属科研机构，主要在数学、系统科学及其相关领域开展基础研究和应用研究。

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