본 논문은 자연어 수학을 기계가 검증 가능한 형식으로 변환하는 자동 형식화(autoformalization)의 과제를 다룹니다. 기존의 의미론적 일관성만으로는 기계 증명기의 효율성을 보장하기 어렵다는 문제에 착안하여, 예산 제약 하에서 의미론적으로 일관된 형식화 집합을 탐색하는 방법론을 제안합니다. 이를 위해 LLM 기반 변이 및 교차 연산, AST 재작성 규칙을 활용한 신경-기호 진화 프레임워크인 FormalEvolve를 개발하여 다양한 후보를 생성하고 증명 효율성을 개선했습니다.
