자연어 수학의 형식화
사람이 읽는 수학 문장을 증명 도구가 다룰 수 있는 명제로 바꾸는 문제를 다룬다. 형식화한 명제를 만드는 작업과 그 명제의 증명을 찾는 작업을 함께 연구할 평가로 제안됐다.
세 가지 자료의 연결
각 예제에는 Lean 3의 형식 명제와 자연어 명제, 자연어 증명이 포함된다. 서로 대응하는 표현을 통해 수학적 내용과 형식 언어 사이의 연결을 살필 수 있다.
대학 수학의 범위
초기 문제는 주로 학부 순수 수학 교재에서 얻었고 실해석과 복소해석, 선형대수와 추상대수 및 위상수학을 포함했다. 수학 경시만으로 구성한 평가와는 문제의 배경이 다르다.
명제 변환의 기준 방법
소개 연구는 문맥 내 학습으로 명제를 형식화하는 기준 결과를 보고했다. 프롬프트 검색과 증류된 역번역이라는 두 형식화 방법도 제안해 변환 능력을 비교했다.