arXiv·· 13 天前AI 评分41
AIProver：用证书驱动演化框架实现数学研究的智能体自动形式化
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
AI 导读
AIProver 通过证书驱动的演化框架实现数学研究的智能体自动形式化，将自然语言定理与证明翻译为 Lean 等形式语言并做机械验证。该工作针对研究级证明常依赖 Mathlib 缺失概念、编译成功不等于语义保真、NL-FL 对齐数据稀缺以及现有智能体依赖昂贵前沿模型和手工框架等问题提出解决方案。
来源：arXiv · arxiv.org