arXiv:2501.16207v2 公告类型：替换 摘要：基于AI的形式数学推理研究展现出了不可阻挡的增长趋势。这些研究在国际数学奥林匹克(IMO)等数学竞赛中表现出色，并取得显著进展。本文集中于形式验证，这是形式推理的直接应用场景，并将其分解为子任务。我们通过提炼gpt-4o，构建了跨五种形式规范语言（Coq、Lean4、Dafny、ACSL和TLA+）的18000个高质量指令-响应对，并针对包括最近流行的DeepSeek-R1在内的十个开源LLMs进行了评估。我们还微调了几种7-8B的小模型，使其在性能上与Deepseek-R1-671B相当。有趣的是，我们观察到，使用形式数据进行微调也增强了数学、推理和编码能力。微调后的模型可在以下地址发布：https://huggingface.co/fm-universe。