MUSTARDSAUCE 수학 정리 문제 데이터 세트

홍콩시립대학교, 중산대학교, 화웨이 노아의 방주 연구소 및 기타 기관의 연구진은 정확하고, 사람이 읽고 이해할 수 있는 대량의 고품질 수학적 추론 데이터를 생성할 수 있는 통합 수학적 추론 데이터 합성 프레임워크인 MUSTARD를 제안했습니다.이 데이터 세트는 연구를 위한 오픈 소스 MUSTARDSAUCE 데이터 세트입니다.이러한 각 데이터에는 자연어로 된 문제 설명과 다단계 솔루션, 그리고 이중 형식 언어인 Lean 3으로 된 문제 설명과 다단계 솔루션이 포함되어 있습니다. MUSTARDSAUCE 데이터에는 초등학교에서 고등 교육까지의 난이도 수준을 포괄하는 수학 단어 문제와 정리 증명 문제가 포함되어 있습니다. 문제의 추론 단계 수는 문제의 난이도가 높아질수록 증가합니다. 가장 어려운 문제를 해결하려면 약 30단계가 필요하고, 린 3 전략은 약 20가지가 필요합니다.