SYNTEXIS：大模型数学推理自动形式化与执行的新基准

SYNTEXIS是一个专注于评估大语言模型（LLM）数学推理自动形式化能力的基准测试框架。它通过思维链方法验证模型将自然语言描述的数学问题转换为可在定理证明器（如Lean、Coq）中执行的形式化代码的能力，强调端到端评估（验证代码可执行性）和多维度指标，为该领域提供标准化测量工具。

数学推理的形式化过程门槛极高，需多年专业训练。随着LLM崛起，核心问题浮现：AI能否自动将自然语言数学问题转为严格形式化代码？这是自动化数学推理的关键一步，SYNTEXIS项目由此诞生，旨在解决该问题并提供评估基准。

SYNTEXIS的设计遵循三大原则：

1. 端到端评估：不仅检查代码语法，还验证其在定理证明器中的执行与验证结果，避免虚假成功；
2. 思维链方法：鼓励模型先进行逐步数学推理，再生成形式化代码，模拟人类解决问题的过程；
3. 多样化数学领域：涵盖代数、几何、数论等分支，反映模型在不同领域的表现差异。

SYNTEXIS的技术架构包括：

• 数据集构建：由数学专家和形式化专家合作，包含自然语言描述、参考形式化代码及元数据（难度、领域等）；
• 执行环境：容器化部署隔离依赖，设超时机制和资源限制确保可重复性；
• 评估流水线：自动化接收输入、提取代码、执行验证、收集结果并生成报告。

SYNTEXIS提供三大评估维度：

1. 形式化成功率：检查代码语法正确性、类型匹配、证明完整性；
2. 推理质量：分析思维链的步骤合理性、策略适当性及错误恢复能力；
3. 跨语言泛化：评估模型在不同定理证明器（如Lean与Coq）间的泛化能力。

应用场景：

• 模型开发者：标准化评估基准衡量技术进步；
• 形式化社区：AI辅助加速证明开发；
• 教育系统：帮助学生理解数学严谨性。

局限性：

• 形式化多样性：同一概念的多种形式化需灵活评估标准；
• 证明器差异：不同工具的库生态和写法需独立评估标准；
• 计算资源：形式化代码执行密集，限制大规模评估扩展性。

SYNTEXIS是重要里程碑，未来方向包括：

1. 更强模型能力：提升自动形式化能力，主动发现证明策略；
2. 交互式形式化：人机协作交替贡献证明步骤；
3. 反向转换：将形式化证明转为自然语言解释，提升可访问性。