AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

기술 요약: 재설계된 언어의 추상 구문 트리(AST) 기반 정형 증명 에이전트

문제 정의
대화형 정형 증명(ITP)은 프로그램 검증과 형식적 수학에 필수적이지만, 높은 수동 노동 비용과 제한된 확장성 문제를 안고 있다. 대규모 언어 모델(LLM) 에이전트는 이 과정을 자동화할 가능성을 제시하지만, 현재의 구현 방식은 과도한 API 비용과 토큰 소비 문제에 직면해 있다. 본 논문은 이러한 비효율성의 두 가지 근본 원인을 식별한다:

1. 구체적 구문(Concrete Syntax)에 대한 의존: 현재의 에이전트들은 직렬화된 소스 텍스트 상에서 작동한다. 이들은 증명을 평문(plain text)으로 생성하며, 별도의 줄 번호 기반 쿼리를 통해 증명 상태를 복구한다. 이는 편집 시 줄 번호가 바뀔 때마다 오류와 상태를 반복적으로 재탐색하게 만들며, 결과적으로 과도한 도구 호출과 토큰 사용을 초래한다.
2. 새로운 언어와의 불일치: 최근의 증명 언어인 Minilang는 세밀한 추론을 고전적 자동 정리 증명기(ATP)에 위임하고, 구문을 자연어 추론과 일치시키도록 설계되어 LLM의 효율성을 높이도록 고안되었다. 그러나 Minilang는 신규 언어(2025년 말 코퍼스 공개 예정)이기 때문에, 범용 LLM은 그 구체적 구문을 숙달하기 위한 학습 데이터가 부족하며, 데이터 희소성과 비용 문제로 인해 미세 조정(fine-tuning)을 수행하는 것도 실질적으로 어렵다.

방법론: AST 기반 에이전트 (AoA)
저자들은 상호작용 계층을 소스 텍스트에서 Minilang의 **추상 구문 트리(AST)**로 격상시킨 **Agent over AST (AoA)**를 제안한다. 이 방법론은 세 가지 핵심 구성 요소로 이루어진다:

1. AST 중심 표현:

   • 에이전트는 소스 코드를 생성하는 대신, Minilang AST의 JSON 표현식을 출력한다. 이 형식은 도구 호출(tool-calling) 기능이 있는 LLM에 친화적이며, 특정 구체적 구문에 대한 의존성을 제거한다.
   • AST는 JSON Schema를 사용하여 정형화되며, 이를 통해 LLM이 구문적 철자(spelling)가 아닌 증명의 의미론적 구축에 집중할 수 있도록 한다.

2. 트리 편집 증명 모델 (Tree-Edit Proof Model):

   • 에이전트는 증명 연산과 증명 상태를 하나의 진화하는 증명 트리로 융합하는 트리 편집 모델을 통해 증명기와 상호작용한다.
   • 상태 융합 (State Fusion): 상태를 별도로 검색하는 기존 에이전트와 달리, 증명 트리의 모든 노드는 해당 서브골(subgoal)의 상태를 보유한다. 연산이 적용되면, 증명기는 결과 상태(목표, 가설, 오류)를 계산하여 이를 연산 노드에 직접 부착한다.
   • 편집 연산: 에이전트는 트리를 조작하기 위해 도구(READ, EDIT, QUERY, SUBAGENT)를 사용한다. EDIT 도구는 슬롯 채우기, 노드 삽입, 연산 수정 또는 서브트리 삭제를 지원한다.
   • 점진적 동기화: 편집 시 시스템은 전체 트리가 아닌, 변경된 상태와 메시지만을 보여주는 압축된 뷰를 반환한다. 이를 통해 LLM이 전체 컨텍스트를 다시 읽거나 취약한 줄 번호를 통해 탐색할 필요를 없앤다.

3. 모델 수정 없는 시스템 설계:

   • AoA는 범용 LLM이 미세 조정 없이도 Minilang에서 증명을 구축할 수 있게 한다. 구체적 구문을 추상화하고 JSON을 통해 의미론적 구조를 노출함으로써, Minilang 코퍼스에 대한 사전 경험이 없는 모델도 효과적으로 작동할 수 있도록 한다.

주요 기여

• 트리 편집 증명 모델: 소스 파일 패칭(patching)을 증명 트리 편집으로 대체하여, 별도의 줄 번호 기반 증명 상태 쿼리가 필요 없도록 하는 새로운 상호작용 모델을 제시한다.
• AoA 에이전트: 범용 LLM이 (코퍼스 규모의 노출이나 미세 조정 없이) 시스템 설계를 통해 새로운 언어(Minilang)에서 정식 증명을 구축할 수 있음을 입증하는 구체적인 구현체를 제시한다.
• 실증적 평가: miniF2F(수학) 및 NTP4VC-Pearl(프로그램 검증) 벤치마크에서 Amazon의 Isabelle Agent를 대상으로 종합적인 평가를 수행했다.

결과
miniF2F와 NTP4VC-Pearl의 공통 성공 세트에서 평가된 결과, AoA는 Amazon의 Isabelle Agent 대비 유의미한 효율성 향상을 보여주었다:

• 비용 절감: (입력 캐시 재사용을 기준으로 정규화했을 때) 2.3~4.7배 낮은 API 비용을 달성했다.
• 토큰 효율성: 2.9~6.9배 적은 총 토큰을 사용하며, 3.9~8.9배 적은 도구 호출을 기록했다.
• 속도: 케이스 완료 속도가 1.4~2.0배 빠르다.
• 성능:
  • miniF2F: **99.6%**의 통과율을 달성하여 최첨단 모델인 SeedProver와 대등한 성능을 보였다.
  • NTP4VC-Pearl: **89.2%**의 통과율을 달성하여 검증 조건 증명(verification-condition proving) 분야의 새로운 SOTA(State-of-the-art)를 기록했다.
• 일반화 능력: (Minilang 코퍼스 공개 전 출시된) Claude Opus 4.5를 대상으로 테스트했을 때, AoA는 **98.6%**의 통과율을 유지하며 언어에 대한 사전 코퍼스 규모의 노출 없이도 작동함을 확인했다.

의의 및 주장
본 논문은 현재 증명 에이전트의 높은 비용이 직렬화된 구체적 구문 위에서 작동하기 때문이라고 주장한다. 증명 언어(Minilang)를 재설계하고 트리 편집 모델 내에서 AST를 노출함으로써 다음을 달성할 수 있다:

1. 증명 에이전트의 API 비용과 토큰 소비를 획기적으로 줄인다.
2. 범용 LLM이 값비싼 미세 조정이나 방대한 학습 코퍼스 없이도 새로운 형식 언어에서 작동할 수 있게 한다.

저자들은 이 접근 방식이 증명 언어의 의미론적 정보를 추상화하고 이를 LLM에 친화적인 형식(JSON/AST)으로 재표현함으로써, 에이전트가 구문적 탐색이 아닌 증명 구축 로직에 집중할 수 있게 한다고 강조한다. 결론적으로 본 논문은 이 방법론이 LLM을 형식 검증에 통합하는 확장 가능한 경로를 제공하며, 유사한 AST 기반 접근 방식이 새로 설계된 프로그래밍 언어를 위한 코딩 에이전트에도 이익이 될 수 있음을 시사한다.