기술 요약: ARIA – 의존성 그래프를 통한 검색 및 반복적 자동 형식화 에이전트

1. 문제 정의

정리(theorem) 문장을 수학적 텍스트에서 Lean 4와 같은 형식 언어로 번역하는 정확한 자동 형식화(auto-formalization)는 연구 수준의 수학에서 자동 발견 및 검증을 진전시키기 위한 핵심적인 병목 구간이다. 대규모 언어 모델(LLM)은 학부 수준의 과업에서는 유망한 성과를 보여주었으나, 다음과 같은 세 가지 주요 실패 모드로 인해 추측(conjecture) 수준의 문장에서는 상당한 어려움을 겪는다:

1. 환각(Hallucations) 및 의미론적 불일치: LLM은 라이브러리(Mathlib)에 존재하지 않는 함수나 정의를 사용하여 코드를 생성하거나, 수학적 개념의 의미론적 의도를 오해하는 경우가 빈번하다.
2. 새로운 정의 합성 능력의 부재: 연구 수준의 수학은 기존 라이브러리에 없는 새로운 객체를 정의해야 하는 경우가 많다. 정적인 단판 생성 방식은 이러한 정의를 자발적으로 합성할 수 없기 때문에 실패한다.
3. 의미론적 검증의 한계: 기존의 의미론적 검사기들은 표면적인 텍스트 유사성이나 역번역(back-translation)에 의존하는 경우가 많아, 비형식적 개념과 그에 대응하는 Lean의 형식적 표현 사이의 미묘한 불일치(예: 잘못된 타입 코어션 또는 매개변수 순서 역전)를 감지하지 못한다.

이러한 문제들은 불충실한 번역을 초래하여 대규모 데이터 생성 파이프라인을 저해하고, 열린 수학적 문제에 대한 자율적 탐색을 가로막는다.

2. 방법론

본 논문은 인간 전문가의 추론 과정을 모방하도록 설계된 2단계 그래프-오브-소트(Graph-of-Thought, GoT) 프로세스를 갖춘 ARIA(Agent for Retrieval and Iterative Auto-Formalization) 시스템을 소개한다. 파이프라인은 다음과 같이 구성된다:

2.1 GoT 파이프라인 (Graph-of-Thought Pipeline)

직접적인 단일 단계 생성과 달리, ARIA는 형식화 과업을 구조화된 의존성 그래프로 분해한다:

• 1단계: GoT 분해 (Top-Down): 에이전트는 비형식적 문장을 받아 이를 개념의 의존성 그래프로 재귀적으로 분해한다. 각 노드는 정의, 구조 또는 클래스를 나타낸다.
  • 그라운딩(Grounding): 각 개념에 대해, 에이전트는 최신 Mathlib을 인덱싱하는 검색 엔진인 LeanSearch를 쿼리하여 표준적인 정의를 찾는다.
  • 추론: LLM은 검색된 후보들을 분석하여 최적의 표준 매칭을 식별한다. 만약 일치하는 것이 없다면, 해당 노드는 합성을 위한 대상으로 표시된다.
• 2단계: GoT 합성 (Bottom-Up): 에이전트는 리프 노드(그라운딩된 개념들)로부터 루트 노드(메인 정리)까지 형식을 합성한다.
  • 컴파일러-인-더-루프(Compiler-in-the-Loop): 모든 합성 단계에서 생성된 코드는 즉시 컴파일된다. 만약 컴파일에 실패하면, 에러 메시지가 자기 성찰(self-reflection)을 위해 LLM에 다시 전달된다.
  • 새로운 개념의 합성: 그라운딩되지 않은 노드의 경우, 에이전트는 의존성들의 검증된 코드를 컨텍스트로 사용하여 새로운 정의를 생성한다.

2.2 AriaScorer: 용어 수준의 그라운딩된 의미론적 검사기

형식적 문법 준수를 넘어 의미론적 정확성을 보장하기 위해, 저자들은 AriaScorer를 도입한다.

• 용어 수준 검색: 형식적 문장을 평가하기 전, AriaScorer는 정적 분석기(jixia)를 사용하여 코드에서 참조된 모든 Lean 용어를 추출한다. 이후 큐레이션된 Mathlib 데이터셋을 쿼리하여 이 용어들의 권위 있는 정의, 타입 및 비형식적 설명을 검색한다.
• 하위 과업 분해: 비형식적 문장은 원자적인 가정과 결론으로 분해된다.
• 그라운딩된 평가: LLM은 비형식적 하위 과업과 형식적 코드 간의 일치 여부를 평가하는데, 이때 결정적으로 검색된 형식적 정의가 컨텍스트로 제공된다. 이를 통해 검사기는 단순한 텍스트 유사성에 의존하는 대신, Lean 용어의 실제 의미에 대해 추론할 수 있다.
• 점수 산출: 하위 과업은 "완벽히 일치(Perfectly Match)", "경미한 불일치(Minor Inconsistency)", "중대한 불일치(Major Inconsistency)"로 라벨링된다. 이들은 퍼지 적분(fuzzy integral)을 통해 최종 점수(0~1)로 집계되며, 이 점수는 이진 수락/거절 결정을 내리기 위한 임계값으로 사용된다.

3. 주요 기여

1. Aria 에이전트: 검색 증강 생성(RAG), 그래프-오브-소트 계획, 컴파일러 가이드 기반 자기 성찰을 통합한 새로운 자동 형식화 에이전트이다. 이는 추측 수준의 형식화에 필요한 복잡하고 새로운 정의를 자율적으로 합성할 수 있는 최초의 시스템이다.
2. AriaScorer: 수학적 정확성을 검증하기 위해 권위 있는 Mathlib 정의를 검색하는 용어 수준의 그라운딩된 의미론적 검사기로, 의미론적 환각으로 인한 거짓 양성을 크게 줄인다.
3. 최첨단 성능(SOTA): 본 시스템은 다양한 벤치마크에서 기존 방식보다 유의미한 개선을 달성했으며, 특히 기존 모델들이 완전히 실패했던 연구 수준의 문제에서 탁월한 성과를 보였다.

4. 실험 결과

저자들은 다양한 벤치마크에서 최종 정확도(컴파일과 의미론적 검사를 모두 통과한 비율)를 측정하여 ARIA를 평가하였다.

• ProofNet (학부 수준): ARIA는 91.6%의 컴파일 성공률과 68.5%의 최종 정확도를 달성하여 이전 방식들을 능가했다.
• FATE-H (대수학 기말고사): ARIA는 71.0%의 최종 정확도를 기록하며, 43.0%를 기록한 최상의 베이스라인(Goedel-V2 pass@128)을 앞질렀다.
• FATE-X (박사/연구 수준): ARIA는 44.0%의 최종 정확도를 달성하였으며, 이는 최상의 베이스라인인 24.0%와 대비된다.
• 호몰로지 추측(Homological Conjectures, 실제 연구): 가환 대수의 14가지 도전적인 추측 데이터셋에서, ARIA는 42.9%의 성공률을 기록한 반면, 다른 모든 베이스라인 모델(Goedel-V2 및 Gemini-2.5-Pro 포함)은 **0%**를 기록했다.

절제 연구(Ablation Studies):

• 성찰(Reflection) 메커니즘을 제거하면 성능이 붕괴되었다 (추측 데이터셋에서 성공률 0%).
• GoT 플래너를 제거하면 추측 데이터셋에서의 성공 횟수가 6/14에서 1/14로 감소했다.
• RAG 모듈을 비활성화하면 추측 데이터셋에서 0%의 성공률을 보였으며, 이는 정적인 사전 학습 지식만으로는 불충분함을 확인시켜 준다.

의미론적 검사기 검증:
FATE-X 벤치마크에서 AriaScorer는 $\alpha=0$에서 89.9%의 정확도를, $\alpha=0.9$에서 95.5%의 정밀도를 달성하여, LeanScorer 및 역번역 베이스라인을 크게 상회했다. 사례 연구들은 "정의 불일치"(예: 사원수 대수의 곱셈 규칙에서의 미묘한 차이)를 감지하고, 실제 라이브러리 정의에 근거하여 환각을 억제하는 능력을 입증했다.

5. 의의 및 주장

본 논문은 ARIA가 자율적 수학적 발견을 향한 기초적인 단계라고 주장한다. 환각과 새로운 정의 합성 능력의 부재라는 "기초적인 병목 현상"을 해결함으로써, ARIA는 추측 수준의 문제를 신뢰성 있게 형식화할 수 있게 한다.

저자들은 정확한 정리 문장(statement)의 형식화가 정리 증명(theorem proving)의 전제 조건임을 강조한다. 호몰로지 추측 데이터셋에 대한 ARIA의 성공은, 기존의 자동화 시스템이 접근할 수 없었던 활발한 연구 문제를 다룰 수 있는 독보적인 능력을 보여준다. 용어 수준의 그 grounding을 의미론적 검사에 통합한 것(AriaScorer)은 텍스트 유사성 지표를 넘어선 필연적인 진화로 제시되며, AI가 생성한 형식화의 수학적 충실도를 검증하는 엄격한 기준을 제공한다.

이 연구는 미래의 자동화된 수학적 증명 시스템이 현대 수학 라이브러리와 연구 최전선을 탐색하기 위해 이와 같은 구조화되고, 검색 증강되며, 자기 성찰적인 에이전트에 의존해야 함을 시사한다.