MathForm, 검색과 검증으로 수학 자동 형식화를 반복 개선

들어가며

“모든 실수에 대해”와 같은 수학 문장을 Lean 4로 표현하는 일은 단순한 번역이 아니다. 모델은 Mathlib에 있는 복잡한 타입과 정의, 기존 형식화 사례를 찾아 적절히 연결해야 한다. 동시에 만들어진 명제가 자연어 원문의 수학적 의미를 그대로 유지하는지도 확인해야 한다. MathForm은 검색과 검증을 생성 과정 안에 포함해 이 문제를 다룬다.

핵심 방식

기존 접근법은 모델 파라미터에 저장된 라이브러리 지식에 크게 의존하는 경우가 많았다. 또한 한 번 생성한 결과를 컴파일 가능 여부로만 필터링하는 데이터 구축 방식도 흔했다. 그러나 컴파일 성공만으로는 잘못된 정의 선택이나 의미 변화까지 충분히 걸러내기 어렵다. MathForm은 다음과 같은 피드백 절차를 도입한다.

• 생성 전 검색: 검색 플래너가 Mathlib에서 관련 정의, 타입 정보, 기존 형식화 표현을 수집해 생성기에 제공한다.
• 컴파일 진단 기반 수정: 생성된 Lean 4 문장을 컴파일하고, 컴파일러의 오류와 진단 정보를 다음 수정 단계에 반영한다.
• 의미 일관성 피드백: 코드가 통과하는지만 보지 않고, 형식화된 명제가 자연어 원문의 의미를 유지하는지도 확인한다.
• 검증 데이터 구축: 수정과 검증을 마친 예제를 FormalVerse 데이터셋으로 모은다.

연구진은 FormalVerse가 여러 수학 분야와 출처를 아우르는 약 367K개의 검증된 Lean 4 예제를 포함한다고 설명한다. 이후 이 데이터로 지도학습 미세 조정을 수행하고 강화학습을 적용해 MathForm-8B를 학습했다.

결과와 의미

6개 벤치마크에서 MathForm-8B의 평균 Pass@8은 Syntax Check 기준 88.06%, Consistency Check 기준 72.37%였다. 논문은 이 결과가 여러 전용 32B 자동 형식화 모델을 능가한다고 보고한다. 더 어려운 FATE-H와 FATE-X 하위 집합에서는 Consistency Check 통과율이 각각 63%와 37%였으며, 두 평가 모두에서 가장 강한 전용 기준선을 넘어섰다.

이 연구의 핵심은 단순히 더 작은 모델이 높은 점수를 냈다는 데 있지 않다. 라이브러리 지식 확보, 컴파일 가능한 형식 코드 생성, 원래 명제의 의미 보존을 하나의 작업 흐름으로 묶었다는 점이 중요하다. 형식 수학에서 컴파일 성공은 필요조건이지만 충분조건은 아니다. 증명 보조기가 받아들이는 문장이라도 원문의 주장을 정확히 표현하지 못할 수 있기 때문이다. 검색과 반복 수정은 이 간극을 줄이기 위한 현실적인 방법을 제시한다.

제공된 자료에는 전체 실험 설정, 기준선 모델의 구성, 의미 일관성 평가의 세부 절차가 포함되어 있지 않다. 따라서 수치 비교는 논문 전문과 함께 검토할 필요가 있다. 다만 코드, 모델, 데이터셋이 공개되어 있어 재현 실험과 후속 연구를 시작할 수 있는 기반은 마련됐다. MathForm은 모델의 내부 기억에만 의존하지 않고, 형식 라이브러리와 검증기의 제약 속에서 수학 데이터를 개선하는 방향을 보여준다.

출처: Hugging Face Daily Papers