香港中文大学 本次发布的数据集 FormalMATH, FormalMATH是一个包含5560个经过形式化验证的数学问题的数据集，涵盖从高中奥赛挑战到大学水平的定理，涉及代数、应用数学、微积分、数论和离散数学等多个领域。为了减少人工形式化的效率低下，我们引入了一种新颖的自动化形式化流程，该流程集成了：（1）用于自动形式化的特定大型语言模型（LLM），（2）多LLM语义验证，（3）基于否定的反驳过滤策略，使用现成的基于LLM的证明者。这种方法在手动验证之前保留了72.09%的陈述，同时确保了对原始自然语言问题的忠实性。我们对最先进的基于LLM的定理证明者的评估揭示了重大局限性：即使在实用的采样预算下，最强的模型也只能达到16.46%的成功率，表现出明显的领域偏见（例如，在代数中表现出色，但在微积分中失败）和对简化自动化策略的过度依赖。值得注意的是，我们发现在思维链推理场景中，自然语言解决方案指导与证明成功之间存在反直觉的负相关关系，这表明人类编写的非正式推理在形式推理环境中引入了噪声而不是清晰度。我们相信，FormalMATH为形式数学推理提供了一个强大的基准。
关于 香港中文大学 , 香港中文大学是一所位于中国香港的公立研究型大学，成立于1963年，是香港成立的第二所大学。大学以“结合传统与现代，融会中西文化”为使命，提供多样化的本科及研究生课程。
关于 arXiv , arXiv 是一个免费分发服务和开放获取的学术文章档案库，涵盖了物理学、数学、计算机科学、定量生物学、定量金融、统计学、电气工程和系统科学以及经济学等领域。该网站上的材料并未经过 arXiv 的同行评审。
_1769672084863.jpg)