기술 요약: 기호적 비형식화 (Symbolic Informalization)

문제 정의

본 논문은 기호적 비형식화(symbolic informalization), 즉 정밀함의 손실 없이 형식 수학(기계 검증된 증명 및 정리)을 유창한 자연어로 신뢰성 있게 변환하는 과제를 다룹니다. 신경망 방식(대규모 언어 모델)이 자동 형식화(informal to formal) 분야에서 발전해 왔으나, 이들은 "환각(hallucination)" 현상을 겪으며 원래 텍스트와 형식화된 정리가 일치함을 보장할 수 없습니다. 반대로, 형식화된 결과는 자동으로 검증될 수 있는 반면, 그 역과정인 비형식화는 기호적으로 자동화하기 어려운 경우가 많습니다.

기존의 기호적 비형식화 시도들은 다음과 같은 세 가지 주요 이유로 비판받아 왔으며, 본 논문은 이를 성공적인 시스템을 위한 핵심 요구사항으로 식별합니다:

1. 유창성(Fluency): 출력물이 자연어의 다양성과 유연성이 부족하여 경직되게 보입니다.
2. 생산성(Productivity): 시스템을 설계하고 구현하기가 어렵습니다.
3. 다국어 지원(Multilinguality): 서로 다른 형식 언어나 자연어 간의 확장이 어렵습니다.

본 논문은 비형식화가 단순히 "쉬운" 번역이 아니라, 의미론적 건전성(semantic soundness, 의미 보존)과 언어적 완결성(linguistic completeness, 수학적 표현의 전체 범위를 포괄함) 사이의 균형을 요구하는 복잡한 연구 문제라고 주장합니다.

방법론: Informath 시스템

본 논문은 유창성, 생산성, 다국어 지원이라는 세 가지 목표를 달려하기 위해 **상호 언어 아키텍처(interlingual architecture)**를 기반으로 구축된 Informath 시스템을 소개합니다.

1. 아키텍처

Informath는 두 단계의 상호 언어 접근 방식을 사용합니다:

• 형식 상호 언어 (Dedukti): 다양한 증명 시스템(Agda, Lean, Rocq) 사이의 허브 역할을 합니다. Dedukti는 의존 타입(dependent types)과 재작성 규칙(rewrite rules)을 가진 미니멀한 논리 프레임워크입니다. 이는 형식적 내용의 진실의 근원(source of truth) 역할을 합니다.
• 언어적 상호 언어 (Grammatical Framework - GF): 자연어 측면을 처리합니다. GF는 다국어 번역을 위해 설계된, Dedukti와 유사한 논리 프레임워크 기반의 문법 형식론입니다.

워크플로우는 다음과 같습니다: 증명 시스템 $\to$ Dedukti $\to$ GF 추상 구문 $\to$ 자연어.

2. 다국어 지원

다국어 지원은 Dedukti 추상 구문을 GF 추상 구사로 매핑한 뒤, 이를 구체적인 자연어로 선형화함으로써 달성됩니다.

• 공유 추상 구문: 핵심 수학 개념은 GF 내의 언어 독립적인 추상 구문 트리(AST)에 정의됩니다.
• 자원 문법 라이브러리 (RGL): Informath는 약 40개 언어에 대해 사전 정의된 언어 구조(굴절, 일치, 통사 규칙)를 제공하는 GF RGL을 활용합니다. 이를 통해 동일한 추상 구상이 영어, 프랑스어, 독일어, 스웨덴어 등에서 문법적 변이(예: 성, 격, 수)를 자동으로 처리하며 올바르게 렌더링될 수 있습니다.

3. 생산성

구현의 어려움을 해결하기 위해, Informath는 최종 사용자가 GF와 Haskell 코드의 복잡성을 추상화할 수 있는 **배포 스택(deployment stack)**을 채택합니다:

• 심볼 테이블 (.dkgf): 가장 높고 접근하기 쉬운 계층입니다. 사용자는 Dedukti 상수를 GF 함수나 문자열 템플릿에 매핑하는 어휘 주석을 정의합니다. 이를 통해 언어학자가 아닌 사용자도 문법 규칙을 직접 작성하지 않고 새로운 수학적 개념을 시스템에 확장할 수 있습니다.
• 스마트 패러다임 (Smart Paradigms): RGL은 기본 단어 형태로부터 굴절 표를 생성하여 수동 어휘 입력을 줄여줍니다.
• 모듈형 코드: 시스템은 의미론적 건전성을 다루는 안정적인 코어(MathCore)와 언어적 완결성을 다루는 확장 가능한 확장 기능(MathExtensions)을 분리합니다.

4. 유창성 및 자연어 생성 (NLG)

유창성을 달성하기 위해, Informath는 기본적인 제어 자연어(CNLs)를 넘어 다단계 NLG 파이프라인을 구현합니다:

• 내용 결정 및 텍스트 계획: 무엇을 말할 것인지와 그 순서를 결정합니다.
• 통합 (Aggregation): 원자적 사실들을 병합합니다 (예: "x는 짝수이고 x는 소수이다"를 "x는 짝수이자 소수이다"로 변환).
• 어휘 선택 (Lexical Choice): 심볼 테이블을 통해 적절한 단어를 선택합니다.
• 표면 실현 (Surface Realization): GF 선형화를 사용하여 최종 문자열을 생성합니다.
• 순위 지정 (Ranking): 시스템은 단일 형식 문장에 대해 수천 개의 변형 표현을 생성합니다. 이들은 트리 크기, 깊이, 토큰 수 및 스타일 규칙(예: 기호로 시작하는 문장 지양)에 기반한 페널티 함수를 사용하여 순위가 매겨집니다. 이는 출력이 압축적이고 자연스럽게 들리도록 보장합니다.

문법은 MathCore(모든 Dedukti 구성을 다루는 최소한의 CNL)와 MathExtensions(수학 언어 전체를 근사함)로 나뉩니다. 시스템은 다음과 같은 복잡한 기능을 지원합니다:

• 변수 바인딩 상수: 고차 추상 구문(Higher-Order Abstract Syntax, HOAS)을 통해 양화사와 적분을 처리합니다.
• 내재적 양화 (In situ quantification): 술어 내에 양화사를 배치합니다 (예: "모든 자연수는 짝수이다").
• 기호 표기 (Symbolic Notation): 언어적 부분은 자연스럽게 유지하면서 기호적 부분에 대해서는 LaTeX 매크로를 생성합니다.

주요 기여

1. Informath 시스템: 기호적 비형식화가 유창하고, 생산적이며, 다국어 지원이 가능하다는 것을 보여주는 작동하는 구현체입니다.
2. 상호 언어 아키텍처: 형식 논리와 언어적 변이를 분리하기 위해 Dedukti와 GF를 이중 상호 언어로 사용하는 참신한 방식입니다.
3. 로우 코드 확장 (Low-Code Extension): 핵심 문법이나 컴파일러 코드를 수정하지 않고도 사용자가 새로운 수학 영역으로 시스템을 확장할 수 있게 하는 심볼 테이블 기반 메커니즘입니다.
4. 모호성 처리: 자연어의 내재적 모호성(예: 양화사의 범위, 접속사)을 관리하기 위해, 엄격하고 모호하지 않은 규칙을 강요하여 유창성을 희생하는 대신, 여러 변형을 생성하고 유형 검사나 순위 지정을 통해 이를 해결하는 전략을 사용합니다.

결과

논문은 Informath의 현재 상태를 보고합니다:

• 범위: 시스템은 학부 수학(산술, 집합론, 대수학, 위상수학)을 다루며, "100개 정리(100 theorems)" 프로젝트에서 테스트되었습니다.
• 다국어 출력: 동일한 Dedukti 소스로부터 영어, 프랑스어, 독일어, 스웨덴어의 유창한 텍스트를 성공적으로 생성합니다.
• 사례 연구:
  • 호모토피 유형론 (Homotopy Type Theory): HoTT 책에 대한 사례 연구에서 제3자 번역기(Agda $\to$ Dedukti)가 유니버스 레벨로 인해 코드 복잡성을 폭발시키는 문제를 발견했습니다. 그러나 일단 변환되면, Informath는 복잡한 "명제로서의 타입(propositions as types)" 시나리오를 포함하여 성공적으로 비형식화를 수행했습니다.
  • 합성 데이터: Informath는 LLM(Qwen2.5-7B-Instruct)을 미세 조정하기 위한 합성 데이터를 생성하는 데 사용되었으며, 그 결과 베이스라인 대비 향상된 자동 형식화 성능을 얻었습니다.
• 한계점: 시스템은 아직 언어적으로 완전하지 않으며(모든 일반적인 수학 언어를 다루지는 못함), 증명 비형식화는 특히 단계의 순서 및 생략과 관련하여 여전히 진행 중인 과제로 남아 있습니다.

의의 및 주장

본 논문은 기호적 비형식화가 신경망 기반 자동 형식화의 필수적인 보완재라고 주장합니다. LLM은 형식 코드를 생성할 수는 있지만 정확성을 보장할 수는 없습니다. 반면, 기호적 비형식화는 신뢰할 수 있고 설명 가능한 가교 역할을 하여, 인간 사용자가 하부 코드를 보지 않고도 자연어로 형식 시스템과 상호작용할 수 있게 합니다.

저자들은 Informath가 기본적인 CNL 이상의 유창성을 달라는 점을 인정하면서도, 일반적인 수학 언어 전체를 포괄하는 것은 여전히 먼 목표라고 겸허히 결론짓습니다. 주요 남은 과제는 생성되는 변형의 수를 순위 매기는 것과 증명의 비형식화입니다. 본 논문은 자동 형식이 검증될 수 있는 것과 달리, 비형식화는 내재적인 신뢰성과 전문가의 지식을 요구하며, 따라서 이러한 도구의 개발이 인간이 읽을 수 있는 기계 검증 수학의 미래를 위한 중요하고도 필수적인 과업임을 강조합니다.