Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

제공된 텍스트를 바탕으로 한 논문 **"Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory"**의 상세 기술 요약입니다:

개요

본 논문은 의존 타입 형식 언어(FL)인 Lean4를 활용하여 대규모 언어 모델(LLM) 에이전트의 워크플로우와 실행 궤적(trajectory)을 일관되게 모델링, 검증 및 정교화하는 최초의 프레임워크인 Lean4Agent를 소개합니다. 저자들은 자연어의 모호함이 종종 환각(hallucination), 논리적 불일치, 실행 실패로 이어지는 다단계 에이전트 시스템의 신뢰성 확보라는 핵심 과제를 다룹니다. 형식 정리 증명(formal theorem proving)의 패러다임을 차용함으로써, Lean4Agent는 에이전트 동작에 대해 수학적으로 증명 가능한 보장을 제공합니다.

핵심 기여

이 프레임워크는 두 가지 주요 구성 요소로 이루어져 있습니다:

1. FormalAgentLib: 에이전트 워크플로우를 형식적으로 모델링하고 검증하기 위한 확장 가능한 Lean4 라이브러리.
2. LeanEvolve: 검증 결과를 사용하여 워크플로우를 자동으로 개선하는 런타임 정교화 방법.

방법론: 3계층 검증 시스템

FormalAgentLib은 세 가지 층위의 정당성(correctness)에 대해 작동합니다:

계층 1: 구조적 검증 (Structural Verification)

• 목표: 컴파일러 체크와 유사하게 워크플로우의 구문적 및 구조적 적절성을 검증합니다.
• 메커니즘: 변수, 실행 노드 및 그래프 전이를 위한 타입 시스템을 정의합니다. 다음 사항을 체크합니다:
  • 노드 도달 가능성(reachability).
  • 엣지 유효성(순차적, 분기형, 루핑).
  • 읽기/쓰기 일관성: 노드가 초기 파라미터이거나 도달 가능한 선행 노드에 의해 생성된 변수만을 읽도록 보장합니다.
• 결과: 특정 단계가 자신의 스코프 내에서 생성되지 않은 데이터에 접근하려고 시도하는 "해결되지 않은 읽기(unresolved reads)"와 같은 구조적 오류를 탐지합니다.

계층 2: 정적 의미론적 검증 (Static Semantic Verification)

• 목표: 명시적인 가정(특히 LLMExec 가정: LLM 단계가 전제 조건을 만족하는 상태에서 시작하면, 사후 조건을 만족하는 상태를 생성한다) 하에 의미론적 자기 일관성을 검증합니다.
• 메커니즘:
  • 서술어 시스템(Predicate System): 모호한 자연어 지침을 구체적이고 결정 가능한 서술어(예: isValidJson, matchesJsonSchema, nameExists)로 변환합니다.
  • Hoare 스타일 로직: 각 에이전트 단계를 전제 조건/사후 조건 쌍으로 모델링합니다.
  • 의미론적 워크플로우 그래프: 이러한 계약(contract)을 워크플로우 그래프를 통해 전파하여, 한 단계의 출력이 다음 단계의 입력 요구 사항을 충족하는지 확인합니다.
  • 암시적 변수(Implicit Variables): 인간이 놓칠 수 있는 오류(예: 병렬 분기에서의 컨텍스트 격리)를 탐지하기 위해 정보 흐름과 컨텍스트 관리를 추적합니다.
• 결과: 실행 전 워크플로우가 의미론적으로 자기 완결적인지 식별합니다.

계층 3: 실행 궤적 검증 (Execution Trajectory Verification)

• 목표: 실제 실행 실행 시 LLMExec 가정을 검증하고 실패 지점을 국소화(localize)합니다.
• 메커니즘:
  • Lean을 사용하여 결정 가능한 서술어를 평가합니다.
  • 외부 도구(예: Python 검증기)를 사용하여 런타임 체크를 수행합니다 (예: URL 연결성).
  • 비결정적 속성에 대해서는 LLM-as-a-Judge를 사용하여 환경 피드백(예: 테스트 케이스 에러)을 활용합니다.
• 결과: 궤적이 예상된 사후 조건에서 벗어나는 정확한 단계를 지목하여 타겟팅된 디버깅을 가능하게 합니다.

LeanEvolve: 형식 기반 정교화 (Formal-Guided Refinement)

워크플로우가 정적 검증을 통과했음에도 실행 중 실패하는 경우, LeanEvolve를 사용하여 이를 정교화합니다:

• 형식 가이드 모드 (Formal-Guided Mode): 계층 3의 진단을 사용하여 위반된 특정 서술어와 실패한 단계를 식별합니다. 그 후 LLM은 이 정밀한 오류 국소화 정보를 바탕으로 워크플로우 명세를 수정하도록 프롬프트됩니다.
• 순수 LLM 모드 (Pure-LLM Mode): 형식적 가이드 없이 더 넓은 탐색과 시행착오 방식의 수정을 수행하는 백업/추가 기능으로, 형식적 피드백이 부족한 작업에 유용합니다.
• 결과: 시스템은 과업을 해결할 때까지 워크플로우를 반복적으로 진화시킵니다.

실험 결과

저자들은 다섯 가지 주요 LLM(GPT-5.2, GLM-5, Kimi-K2.5 포함)을 대상으로 두 가지 도전적인 벤치마크에서 Lean4Agent를 평가했습니다:

1. SWE-Bench-Verified (Hard Subset): 코드 생성 및 디버깅을 포함하는 실제 소프트웨어 엔지니어링 작업.
2. ELAIP-Bench: 복잡한 추론과 증거 검색을 요구하는 AI 논문 이해 작업.

주요 결과:

• 검증의 영향: 계층 2 검증을 통과한 워크플로우는 통과하지 못한 워크플로우보다 평균 11.94%(SWE에서 14.80%, ELAIP에서 9.07%) 더 높은 성능을 보였습니다. 이는 형식 검증이 결함이 있는 워크플로우를 효과적으로 걸러낸다는 것을 입증합니다.
• 정교화의 영향: LeanEvolve를 사용했을 때, 검증된 워크플로우는 SWE 작업에서 평균 **7.47%**의 추가적인 성능 향상을 달 Achieved 했습니다.
• 형식 vs 순수 LLM: 형식 가이드 진화는 순수 LLM 진화보다 초기 실패 사례를 해결하는 데 있어 평균 7.00% 더 우수한 성능을 보였으며, 이는 정밀한 오류 국소화가 맹목적인 시행착오보다 우월함을 증명합니다.
• 모델 민감도: 작은 모델일수록 워크플로우 품질에 대한 민감도가 높았으며, 큰 모델보다 검증을 통해 얻는 이득이 더 컸습니다.

결론

Lean4Agent는 **검증 가능한 AI(verifiable AI)**의 새로운 패러다임을 구축합니다. 의존 타입 형식 언어를 에이전트 시스템에 적용함으로써, 휴리스틱 평가를 넘어 수학적으로 근거 있는 보장을 제공합니다. 이 프레임워크는 작업 성능을 향상시킬 뿐만 아니라, 고위험 영역에서 자가 개선이 가능하고 신뢰할 수 있는 자율 에이전트를 개발하기 위한 토대를 제공합니다. 저자들은 이 분야의 추가 연구를 촉진하기 위해 코드를 오픈 소스로 공개할 계획입니다.