본 논문은 비공식 수학을 기계적으로 검증 가능한 정리로 공식화하는 데 있어 유망한 발전을 보이는 최신 대규모 언어 모델(LLM)의 한계를 다룹니다. 다국어 병렬 말뭉치의 양과 질이 제한적이라는 점이 주된 병목 현상입니다. 이를 해결하기 위해, 본 논문에서는 새로운 신경 기호 프레임워크인 KELPS(Knowledge-Equation based Logical Processing System)를 제안합니다. KELPS는 비공식 데이터를 Lean, Coq, Isabelle과 같은 여러 공식 언어로 번역, 합성 및 필터링하는 반복적인 프레임워크입니다. 먼저 자연어를 주장 논리에 이론적으로 기반을 둔 새로운 언어인 지식 방정식(KEs)으로 번역한 후, 구문 구조와 의미를 모두 보존하는 엄격하게 정의된 규칙을 통해 목표 언어로 변환합니다. 이 과정을 통해 60,000개가 넘는 문제의 병렬 말뭉치를 생성했습니다. 본 프레임워크는 MiniF2F에서 88.9%의 구문 정확도(pass@1)를 달성하여 Deepseek-V3(81%) 및 Herald(81.3%)와 같은 최첨단 모델을 여러 데이터 세트에서 능가합니다. 모든 데이터 세트와 코드는 보충 자료에서 확인할 수 있습니다.
