IndiMathBench: 用人类触感实现数学推理问题的自动形式化
IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
AI总结：
IndiMathBench通过人机协作管道形式化数学问题，提供具有挑战性的数学推理测试环境。
摘要：
在大语言模型时代，可靠的自动形式化仍然具有挑战性。高质量训练数据的稀缺是主要瓶颈。专家标注需要大量时间和对数学和定理证明的深入专业知识。我们介绍了IndiMathBench，一个经过人类验证的基准，用于评估数学定理证明，通过一个由AI驱动的人机协作管道来形式化自然语言问题。IndiMathBench由312个形式化的Lean 4定理及其对应的非正式问题陈述组成，这些内容来自印度数学奥林匹克竞赛。通过基于类别的检索、迭代编译器反馈和多模型集合，我们的管道生成候选形式化，专家通过带有自动质量摘要的交互式仪表板高效验证。在多个前沿模型上的评估表明，自动形式化仍然具有挑战性，语法正确性与语义正确性之间存在显著差距，而即使经过迭代优化，定理证明的成功率仍然很低，表明该基准为数学推理提供了具有挑战性的测试环境。IndiMathBench可在https://github.com/prmbiy/IndiMathBench上获取。
英文摘要：
Reliable autoformalization remains challenging even in the era of large language models (LLMs). The scarcity of high-quality training data is a major bottleneck. Expert annotation requires substantial time and deep expertise in both mathematics and theorem proving. We introduce IndiMathBench, a human-verified benchmark designed to evaluate mathematical theorem proving, curated using an AI-powered human-assisted pipeline for formalizing natural language problems in Lean. IndiMathBench is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads. Through category-based retrieval, iterative compiler feedback, and multi-model ensembles, our pipeline generates candidate formalizations that experts efficiently validate via an interactive dashboard with automated quality summaries. Evaluation across multiple frontier models demonstrates that autoformalization remains challenging, with substantial gaps between syntactic validity and semantic correctness, while theorem proving success rates remain low even with iterative refinement, demonstrating that \benchmark~presents a challenging testbed for mathematical reasoning. IndiMathBench is available at https://github.com/prmbiy/IndiMathBench.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
