FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

[기술 요약] FormalScience: 과학 분야의 확장 가능한 인간 참여형 자동 형식화(Autoformalisation)

1. 문제 정의 (Problem Statement)

• 자동 형식화(Autoformalisation)의 한계: 비형식적 수학적 추론(LaTeX 등)을 형식적 언어(Lean, Isabelle 등)로 변환하는 것은 LLM에게 매우 어려운 과제입니다.
• 과학 분야의 특수성: 물리학과 같은 과학 분야는 디락 표기법(Dirac notation), 벡터 미적분학 등 도메인 특화된 표기법을 사용합니다. 현재의 LLM과 에이전트 방식은 이러한 도메인 지식을 형식 언어로 변환할 때 의미적 드리프트(Semantic Drift)—즉, 코드는 컴파일되지만 원래의 물리적 의미를 잃어버리는 현상—를 해결하지 못하고 있습니다.
• 도구의 불일치: Lean4와 같은 형식 검증 도구는 물리학의 핵심인 미적분이나 비가환 연산자(non-commutative operators)에 대한 라이브러리 지원이 부족하여, 형식화 과정에서 물리적 맥락이 단순한 대수학적 구조로 축소되는 문제가 발생합니다.

2. 연구 방법론 (Methodology)

본 논문은 FormalScience라는 도메인 불가지론적(domain-agnostic)인 인간 참여형(Human-in-the-loop) 에이전트 파이프라인을 제안합니다.

• FormalScience 파이프라인 (Alg. 1):
  1. 비형식적 QA 생성: 소수의 골드 표준(Gold-standard) 예시를 바탕으로, LLM이 풍부한 문맥을 가진 비형식적 문제(Statement)와 풀이(Proof) 쌍을 생성합니다.
  2. 에이전트 기반 코드 생성: Lean4 컴파일러(L)를 도구로 사용하는 에이전트가 코드를 생성하고, 컴파일 에러 메시지를 피드백 삼아 반복적으로 수정(Iterative correction)합니다.
  3. 인간 참여형 정렬(Alignment): 코드가 컴파일되더라도, 물리 전문가가 해당 코드가 원래의 비형식적 추론과 의미적으로 일치하는지 확인(Binary classification)하고, 불일치 시 개선을 명령합니다.
• FormalPhysics 데이터셋 구축: 위 파이프라인을 물리학에 적용하여 대학 수준의 양자역학 및 전자기학 문제 200개, LaTeX 풀이, 그리고 Lean4 형식 코드로 구성된 고품질 데이터셋을 구축했습니다.
• 에이전트 기반 코드 생성 (Alg. 2): 구조적 에러(Syntax 등)는 전체 재생성을 통해, 의미적 에러(Type mismatch 등)는 패치 에이전트(Patch agent)를 통한 최소 단위 수정(Unified diff)을 통해 해결하는 신경-기호적(Neuro-symbolic) 접근법을 사용합니다.

3. 주요 기여 (Key Contributions)

1. FormalScience 프레임워크: 전문가가 깊은 형식 언어 지식 없이도 저비용으로 고품질의 형식화된 과학 데이터셋을 생성할 수 있는 확장 가능한 파이프라인을 제시했습니다.
2. FormalPhysics 데이터셋: 기존 수학 벤치마크보다 복잡도가 높고, 형식적 유효성(Formal validity)과 품질이 검증된 물리학 특화 데이터셋을 공개했습니다.
3. 의미적 드리프트(Semantic Drift)의 체계적 분류: 형식화 과정에서 발생하는 오류를 네 가지 범주로 정의했습니다.
   • Notational Collapse (표기법 붕괴): 복잡한 연산자(예: 양자 상태 벡터)를 단순 스칼라로 축소.
   • Abstraction Elevation (추상화 상승): 물리적 계산을 단순한 대수적 성질로 대체.
   • Proof Strategy Substitution (증명 전략 교체): 원래의 풀이와 다른 방식으로 결론 도출.
   • Implicit Premise Selection (암묵적 전제 선택): 명시되지 않은 논리적 전제를 도입하여 증명을 단순화(유일하게 긍정적인 드리프트).

4. 실험 결과 (Results)

• 데이터셋 성능: FormalPhysics는 기존 벤치마크(miniF2F, ProofNet 등)와 비교했을 때 훨씬 높은 객체/공식 복잡도를 가지며, **형식적 유효성(Formal Validity) 100%**를 달성했습니다.
• LLM 성능 비교:
  • Zero-shot 및 Self-refinement 방식은 물리학 자동 형식화에서 낮은 성공률을 보였습니다.
  • 에이전트 방식(GPT-OSS-20B 기반): 형식적 유효성을 31%까지 끌어올리며 오픈소스 모델의 한계를 극복했습니다.
  • Alignment-Validity Trade-off: 형식적 유효성(컴파일 성공률)을 높이려 할수록 의미적 정렬(Alignment)이 낮아지는 경향이 확인되었습니다. 이는 물리적 맥락을 무시하고 컴파일 가능한 단순 수학 문제로 변환하기 때문입니다.

5. 의의 및 결론 (Significance)

• 과학적 검증의 자동화: 본 연구는 물리학과 같은 복잡한 과학 분야에서 AI가 생성한 추론을 엄밀하게 검증하기 위한 기초를 마련했습니다.
• 설명 가능한 검증(Explainable Verification): 단순히 "코드가 맞다"를 넘어, "무엇이 어떻게 변형되어 검증되었는가"를 분석함으로써 형식화 과정의 신뢰성을 평가하는 방법론을 제시했습니다.
• 향후 과제: Lean4의 Mathlib에 물리학 라이브러리(벡터 미적분, 디락 표기법 등)를 확장하는 것이 자동 형식화의 성능을 높이는 핵심 과제임을 시사합니다.