Insights
AI가 자동으로 큐레이션·번역·정리하는 기술 동향 피드입니다.
AoA는 언어의 추상 구문 트리(AST)를 기반으로 설계된 새로운 정리 증명 에이전트입니다. 기존의 텍스트 기반 방식에서 발생하는 높은 토큰 비용과 상태 관리 문제를 해결하기 위해 증명 과정을 JSON 형태의 AST로 처리합니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 arXiv cs.PL (Programming Languages)의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기대화형 정리 증명 (Interactive theorem proving, ITP)은 프로그램 검증과 형식화된 수학의 근간을 이루지만, 수동 작업의 부담으로 인해 확장성에 한계가 있습니다. LLM 기반 증명 에이전트는 이러한 노력을 완화할 것으로 기대되지만, 과도한 토큰 소비와 API 비용이 주요 장애물로 남아 있습니다. 우리는 이 비용의 원인이 공통된 근본 문제에 있음을 추적했습니다. 현재의 에이전트들은 직렬화된 구체적 구문 (concrete syntax) 위에서 동작하며, 증명을 소스 텍스트로 출력하고 별도의 줄 번호 기반 쿼리를 통해 증명 상태를 복구합니다. 이로 인해 모든 수정 사항이 이후의 줄들을 밀어내게 되어, 오류와 상태의 위치를 반복적으로 재조정해야 하는 상황이 발생합니다. 이러한 구체적 구문에 대한 의존성은 최근 LLM 기반 증명에서 SOTA (State-of-the-Art)에 도달했으나 LLM의 학습 코퍼스에는 너무 생소한 최신 증명 언어인 Minilang의 채택을 가로막기도 합니다. 우리는 에이전트를 소스 텍스트에서 추상 구문 트리 (Abstract Syntax Tree, AST)로 격상시킴으로써 두 가지 문제를 모두 해결합니다. 모델은 도구 호출 (tool-calling) LLM에 친숙한 Minilang AST의 JSON 표현 방식으로 증명을 제공하며, 증명 작업과 상태를 하나의 증명 트리로 융합하는 트리 편집 모델 (tree-edit model)을 통해 증명기를 구동합니다. 이를 통해 각 작업은 자체적인 하위 목표 (subgoal) 상태를 보유하게 되며, 트리를 통해 직접 읽을 수 있습니다. 우리는 이러한 설계를 \emph{Agent over AST} (AoA)로 구현했습니다. miniF2F 및 NTP4VC-Pearl 공통 성공 세트에 대해 Amazon의 Isabelle Agent와 비교했을 때, AoA는 API 비용을 2.3--4.7배 절감하고 (입력 캐시를 고려한 정규화 기준), 토큰 사용량을 2.9--6.9배, 도구 호출을 3.9--8.9배 줄였으며, 수행 속도는 1.4--2.0배 더 빨랐습니다. 동시에 더 어려운 검증 벤치마크에서 훨씬 더 많은 문제를 해결했습니다.