核心概念
이 논문은 Lean 정리 증명기를 사용하여 수학 명제를 자동으로 형식화하는 GFLean 프레임워크를 소개한다.
摘要
이 논문은 수학 명제를 자동으로 형식화하는 GFLean 프레임워크를 소개한다. GFLean은 Grammatical Framework(GF)라는 고수준 문법 작성 도구를 사용하여 구현되었다.
GFLean의 주요 기능은 다음과 같다:
- Simplified ForTheL이라는 간단한 통제 자연어로 작성된 수학 명제를 입력받아 파싱한다.
- 파싱된 추상 구문 트리(AST)를 단순화하는 일련의 변환 과정을 거친다.
- 단순화된 AST를 Lean 표현식의 AST로 변환한다.
- Lean 표현식의 AST를 GF를 사용하여 Lean 코드로 선형화한다.
GFLean은 수학 교과서 "Mathematical Proofs"의 3장에 나오는 62개 명제 중 42개를 성공적으로 형식화할 수 있었다. 하지만 Simplified ForTheL은 수학 언어의 일부 구문을 지원하지 않아 한계가 있다. 향후 ForTheL과 같은 더 강력한 통제 자연어로 확장하고, Lean 내부에서 동적으로 어휘를 확장할 수 있는 방법을 모색할 계획이다.
統計資料
n이 정수일 때, n^2 - 3n + 9는 홀수이다.
n이 정수일 때, (n + 1)^2 - 1이 짝수이면 n은 홀수이다.
a와 b가 정수일 때, a*b가 짝수이면 a 또는 b가 짝수이다.
引述
"GFLean은 Simplified ForTheL 표현식을 Lean 표현식으로 변환한다."
"GFLean은 수학 교과서 'Mathematical Proofs'의 3장에 나오는 62개 명제 중 42개를 성공적으로 형식화할 수 있었다."
"Simplified ForTheL은 수학 언어의 일부 구문을 지원하지 않아 한계가 있다."