MASA: 자동형식화를 위한 LLM 기반 다중에이전트 시스템

기본 정보

• 논문 ID: 2510.08988
• 제목: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
• 저자: Lan Zhang (맨체스터 대학교), Marco Valentino (셰필드 대학교), André Freitas (맨체스터 대학교, Idiap 연구소, 국립 바이오마커 센터)
• 분류: cs.CL (계산언어학), cs.FL (형식언어)
• 발표 시간: 2025년 10월 10일 (arXiv 사전인쇄본)
• 논문 링크: https://arxiv.org/abs/2510.08988

초록

자동형식화는 자연언어와 형식추론을 연결하는 데 있어 핵심적인 역할을 한다. 본 논문은 자동형식화 작업을 위한 대규모언어모델(LLM) 기반 다중에이전트 시스템 구축 프레임워크인 MASA를 제안한다. MASA는 협력하는 에이전트들을 활용하여 자연언어 명제를 형식 표현으로 변환한다. MASA의 아키텍처 설계는 모듈성, 유연성 및 확장성을 강조하며, 빠르게 발전하는 분야에 적응하기 위해 새로운 에이전트와 도구의 원활한 통합을 가능하게 한다. 저자들은 실제 수학 정의의 사용 사례와 형식수학 데이터셋에 대한 실험을 통해 MASA의 효과성을 입증한다. 본 연구는 LLM과 정리증명기 상호작용에 의해 주도되는 다중에이전트 시스템이 자동형식화의 효율성과 신뢰성 향상에 있어 가지는 잠재력을 강조한다.

연구 배경 및 동기

문제 정의

자동형식화(Autoformalization)는 자연언어 수학 명제를 기계 검증 가능한 형식논리 공식으로 자동 변환하는 작업이다. 이 문제의 핵심 과제는 다음과 같다:

1. 의미론적 간극: 자연언어의 모호성과 형식언어의 엄격성 사이의 거대한 차이
2. 복잡성: 실제 수학 명제는 종종 복잡한 개념과 추론 연쇄를 포함
3. 정확성 요구사항: 형식화 결과는 구문론적으로나 의미론적으로 모두 정확해야 함

문제의 중요성

자동형식화는 다음과 같은 중요한 의의를 가진다:

• 수학 검증: 정리증명과 수학 검증을 위한 기초 제공
• 추론 투명성: 자연언어 추론에 비해 형식추론은 더욱 체계적, 투명하고 엄격함
• 자동화 필요성: 수동 형식화는 대량의 전문 지식과 시간 비용 필요

기존 방법의 한계

기존 LLM 기반 자동형식화 시스템의 문제점:

1. 단일체 아키텍처 제한: 단일 LLM은 복잡한 실제 자동형식화 문제 처리 어려움
2. 모듈성 부족: 기존 구현은 모듈성, 유연성 및 확장성 부족
3. 컴포넌트 상호작용 불충분: 여러 상호작용 컴포넌트를 효과적으로 통합 불가

연구 동기

저자들이 MASA 프레임워크를 제안한 동기:

• 자동형식화의 복잡성을 해결하기 위한 모듈화된 다중에이전트 시스템 구축
• 연구자들이 시스템을 빠르게 개발하고 확장할 수 있도록 지원하는 유연하고 확장 가능한 프레임워크 제공
• 에이전트 협력을 통해 자동형식화의 효율성과 신뢰성 향상

핵심 기여

1. 모듈화된 다중에이전트 프레임워크 제안: MASA는 자동형식화 다중에이전트 시스템 구축을 위한 모듈화 프레임워크를 제공하며, 우수한 유연성과 확장성을 갖춤
2. 실제 응용 사례 제시: 에이전트를 통해 실제 수학 정의를 형식화하여 프레임워크의 실용적 잠재력을 강조
3. 체계적 평가: 세 가지 다중에이전트 설정 하에서 프레임워크를 평가하여 효과성을 입증하고 가치 있는 통찰력 제공. 최종 반복적 자기개선 시스템은 Qwen2.5-7B와 GPT-4.1-mini에서 각각 35.25%와 61.89%의 구문론적으로 정확하고 의미론적으로 정렬된 형식화율 달성
4. 오픈소스 구현: 완전한 코드와 데이터 제공으로 연구 진입 장벽 낮춤

방법론 상세 설명

작업 정의

자동형식화는 자연언어 명제 s를 형식 표현 φ = A(s)로 매핑하는 변환 함수 A로 정의할 수 있다. 기존 방법은 LLM 프롬프트를 통해 구현: A = LLM(prompt). MASA는 이 정의를 확장하여 다중에이전트 시스템을 통해 더욱 복잡한 변환 과정을 구현한다.

모델 아키텍처

MASA 프레임워크는 다섯 가지 핵심 컴포넌트를 포함한다:

1. 에이전트(Agent)

특정 기능을 수행하는 기본 요소로, 다음을 포함한다:

• AutoformalizationAgent: 소수샷 자동형식화 수행
• HardCritiqueAgent: 정리증명기 기반 구문론적 비판 제공
• SoftCritiqueAgent: LLM 기반 의미론적 비판 제공
• FormalRefinementAgent: 하드 비판에 기반한 형식화 코드 개선
• InformalRefinementAgent: 소프트 비판에 기반한 형식화 코드 개선
• DenoisingAgent: 노이즈 제거 도구 에이전트
• ImportRetrievalAgent: 임포트 검색 도구 에이전트

2. 대규모언어모델(Large Language Model)

LLM은 에이전트에 추론 및 언어 능력을 제공하며, 다음을 지원한다:

• OpenAI 모델 (예: GPT-4.1-mini)
• HuggingFace 로컬 모델 (예: Qwen2.5-7B, DeepSeek-Math)

3. 지식베이스(Knowledge Base)

형식언어 라이브러리의 정보를 저장하며, 관련 지식 검색을 지원한다. 현재 구현은 Isabelle/HOL 형식 명제 및 증명의 지식베이스를 포함한다.

4. 검색기(Retriever)

수학 라이브러리의 데이터 포인트에 대한 관련성 순위를 매기며, 현재 구현은 BM25 방법 기반이다.

5. 정리증명기(Theorem Prover)

형식화의 구문론적 정확성과 논리성을 검증하며 오류 정보를 제공한다. 다음을 지원한다:

• Isabelle (전용 서버를 통해)
• Lean4 (REPL을 통해)

기술 혁신점

1. 모듈화 설계: 추상 기본 클래스 설계를 채택하여 새로운 에이전트와 도구 확장 용이
2. 다층 비판 메커니즘: 하드 비판(구문론)과 소프트 비판(의미론) 결합
3. 반복적 개선 프로세스: 다중 라운드 자기개선 에이전트 협력 지원
4. 도구 에이전트 통합: 노이즈 제거 및 임포트 검색 등 실용적 도구 통합

실험 설정

데이터셋

1. miniF2F: Isabelle/HOL 및 Lean4의 실제 형식화 제공, 벤치마크 테스트용
2. ProofNet: Lean4 코드의 실제 형식화 제공

평가 지표

구문론적 정확성

• Pass Rate: 구문론적으로 정확한 형식화의 백분율

의미론적 평가

• BLEU-4: 실제 형식화와의 n-gram 중복도
• ChrF: 문자 수준 F-score
• RUBY: 코드 이식 평가 지표

에이전트 평가

• Alignment Faithfulness (AF): 형식화 코드가 자연언어 의미론을 정확히 정렬하는지 여부
• Formalization Correctness (FC): 형식화 코드 자체가 유효하고 자연스러우며 형식이 잘 맞는지 여부

비교 방법

• 영샷 프롬프팅(ZS): LLM을 직접 사용한 형식화
• 소수샷 프롬프팅(FS): 3개 예제를 사용한 형식화
• 다양한 LLM 조합: GPT-4.1-mini, DeepSeek-Math-7B, Qwen2.5-7B

구현 세부사항

• 소프트 비판 에이전트의 백엔드 LLM으로 GPT-4.1-mini 사용
• Isabelle/HOL 및 Lean4 두 가지 형식언어 지원
• 완전한 Python 구현 및 Jupyter Notebook 예제 제공

실험 결과

주요 결과

하드 비판 형식 개선 시스템 (표1)

miniF2F-Test (Isabelle/HOL):

• GPT-4.1-mini 영샷: Pass Rate 65.57% → 77.05% (+11.48%)
• GPT-4.1-mini 소수샷: Pass Rate 76.23% → 86.48% (+10.25%)
• DeepSeek-Math 소수샷: Pass Rate 29.10% → 36.48% (+7.38%)

ProofNet-Test (Lean4):

• GPT-4.1-mini 영샷: Pass Rate 3.30% → 3.85% (+0.55%)
• GPT-4.1-mini 소수샷: Pass Rate 12.09% → 14.84% (+2.75%)

소프트 비판 비형식 개선 시스템 (표2)

miniF2F (Lean4):

• DeepSeek-Math + GPT-4.1-mini 개선: AF 38.52% → 90.57%, FC 47.54% → 79.92%
• Qwen2.5-7B + GPT-4.1-mini 개선: AF 54.51% → 93.44%, FC 62.70% → 85.25%

반복적 자기개선 실험

그림2 결과:

• Qwen2.5-7B: 4라운드 반복 후, 구문론적으로 정확하고 의미론적으로 정렬된 비율 35.25% 달성
• GPT-4.1-mini: 4라운드 반복 후, 구문론적으로 정확하고 의미론적으로 정렬된 비율 61.89% 달성

실험 발견

1. 소수샷이 영샷 우수: 모든 설정에서 소수샷 학습이 성능을 현저히 향상
2. 모델 능력의 영향: 강력한 모델(GPT-4.1-mini)이 형식 개선에서 더 우수한 성능 발휘
3. 반복적 개선의 효과: 다중 라운드 반복이 형식화 품질을 지속적으로 향상
4. 교차 모델 개선: 강력한 모델이 약한 모델의 출력을 개선 가능

관련 연구

자동형식화 연구

• 프롬프팅 방법: Wu et al. (2022) 등이 LLM 프롬프팅을 사용한 자동형식화 수행
• 데이터 생성: Jiang et al. (2024)와 Liu et al. (2025b)가 대규모 병렬 말뭉치 개발
• 시스템 구현: 기존 시스템은 모듈성과 확장성 부족

다중에이전트 시스템

• 응용 분야: 운영체제, 의학 교육, 답변 검증 등
• 추론 작업: 산술 추론 및 일반 추론
• 자동형식화 응용: 자동형식화 분야의 다중에이전트 시스템 연구는 제한적

결론 및 논의

주요 결론

1. 프레임워크 효과성: MASA는 모듈화된 다중에이전트 자동형식화 시스템을 성공적으로 구축
2. 성능 향상: 다중에이전트 협력이 자동형식화 정확성을 현저히 향상
3. 실용적 가치: 프레임워크는 연구자에게 유연한 개발 플랫폼 제공

한계

1. 중앙 제어 부재: 시스템은 다양한 에이전트를 할당하고 제어하는 중앙 에이전트 부재
2. 의미론적 평가 제한: 의미론적 평가는 고수준 판단에만 제한되며, 더욱 세밀한 평가 기준 필요
3. 모델 의존성: 시스템 성능은 기저 LLM의 능력에 크게 의존

향후 방향

1. 중앙 제어 강화: 더욱 고급 다중에이전트 시스템 제어 메커니즘 개발
2. 평가 세분화: 더욱 정교한 의미론적 평가 기준 수립
3. 응용 확대: 프레임워크를 더욱 광범위한 형식화 작업에 적용

심층 평가

장점

1. 높은 혁신성: 최초의 체계적 다중에이전트 자동형식화 프레임워크
2. 합리적 설계: 모듈화 아키텍처 설계가 우아하고 확장 용이
3. 충분한 실험: 다양한 설정과 평가 지표 포함
4. 높은 실용적 가치: 오픈소스 구현으로 연구 진입 장벽 낮춤
5. 강한 설득력의 결과: 다양한 데이터셋에서 방법의 효과성 검증

부족한 점

1. 이론적 분석 부족: 다중에이전트 협력 메커니즘에 대한 이론적 분석 부족
2. 계산 비용: 다중에이전트 시스템의 계산 오버헤드 분석 불충분
3. 오류 전파: 에이전트 간 오류 전파 문제에 대한 심층 분석 부족
4. 평가 한계: 의미론적 평가는 여전히 LLM 판단에 의존하여 편향 가능성 존재

영향력

1. 학술적 기여: 자동형식화 연구에 새로운 패러다임 제공
2. 실용적 가치: 프레임워크를 실제 응용 개발에 직접 활용 가능
3. 재현성: 완전한 오픈소스 구현으로 재현성 보장
4. 발전 추진: 다중에이전트의 형식화 분야 응용 추진 예상

적용 시나리오

1. 수학 형식화: 복잡한 수학 정리 및 정의의 자동형식화에 적합
2. 교육 응용: 수학 교육에서 형식화 훈련에 활용 가능
3. 연구 도구: 자동형식화 연구를 위한 기초 플랫폼 제공
4. 산업 응용: 형식 검증이 필요한 소프트웨어 시스템에 통합 가능

참고문헌

주요 참고문헌:

• Wu et al. (2022): Autoformalization with large language models
• Zheng et al. (2022): miniF2F: a cross-system benchmark for formal olympiad-level mathematics
• Azerbayev et al. (2023): ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
• Jiang et al. (2023): Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

요약: MASA는 모듈화 설계와 에이전트 협력을 통해 자동형식화의 효과를 현저히 향상시키는 혁신적인 다중에이전트 자동형식화 프레임워크이다. 본 연구는 기술 혁신, 실험 검증 및 실용적 가치 측면에서 모두 우수한 성능을 보이며, 자동형식화 연구에 새로운 방향을 개척한다. 일부 한계가 있음에도 불구하고, 오픈소스 구현과 우수한 확장성으로 인해 본 연구는 해당 분야의 중요한 기여가 된다.