7B级形式化推理与验证小模型，媲美满血版DeepSeek-R1，全面开源！

文章预览

MLNLP 社区是国内外知名的机器学习与自然语言处理社区，受众覆盖国内外NLP硕博生、高校老师以及企业研究人员。 社区的愿景 是促进国内外自然语言处理，机器学习学术界、产业界和广大爱好者之间的交流和进步，特别是初学者同学们的进步。 来源 |机器之心 研究团队构成：香港科技大学、中国科学院软件研究所、西安电子科技大学和重庆大学。团队核心成员：香港科技大学的研究助理教授曹嘉伦，主要研究领域包括 AI 、人工智能测试、形式化验证等；中国科学院软件研究所副研究员陆垚杰，主要研究领域包括大语言模型及其应用。 随着 DeepSeek-R1 的流行与 AI4Math 研究的深入，大模型在 辅助形式化证明写作 方面的需求日益增长。作为数学推理最直接的应用场景， 形式化推理与验证（formal reasoning and verification） ，也获得持续关注。 然而，近期 ………………………………