본 논문은 수학적 정리 증명을 평가하기 위해 설계된 인간 검증 벤치마크인 IndiMathBench를 소개한다. 이 벤치마크는 인도 수학 올림피아드에서 출제된 자연어 문제를 Lean 형식으로 공식화하는 AI 기반 인간 지원 파이프라인을 사용하여 큐레이션되었다. IndiMathBench는 312개의 형식적인 Lean 4 정리와 해당 비공식 문제 설명으로 구성되어 있다. 파이프라인은 범주 기반 검색, 반복적인 컴파일러 피드백 및 다중 모델 앙상블을 통해 전문가가 자동 품질 요약과 함께 상호 작용 대시보드를 통해 효율적으로 검증하는 후보 공식화를 생성한다. 여러 최첨단 모델에 대한 평가는 자동 형식화가 여전히 어려우며, 구문적 유효성과 의미적 정확성 간의 상당한 격차가 존재함을 보여준다. 정리 증명 성공률은 반복적인 개선에도 불구하고 여전히 낮아 IndiMathBench가 수학적 추론에 대한 어려운 테스트베드를 제시함을 보여준다.
