Papers·1주 전
UIUC, Lean4 기반 정형 검증 에이전트 프레임워크 공개 — SWE-Bench 11.94% 차이
UIUC ScaleML Lab이 Lean4라는 의존 타입 형식 언어를 활용해 LLM 에이전트의 워크플로를 정형 검증하는 프레임워크 Lean4Agent를 공개했습니다. FormalAgentLib 라이브러리로 워크플로의 의미적 일관성을 검증하고, LeanEvolve로 검증 실패 워크플로를 자동 수정합니다. SWE-Bench-Verified 난이도 높은 부분집합에서 검증 통과 워크플로가 실패 워크플로보다 평균 11.94% 높은 성능을 보였고, LeanEvolve 적용 시 추가로 7.47% 개선되었습니다. 다만 5개 LLM에 대한 실험 결과이며, Lean4 자체의 학습 곡선이 필요하다는 점은 고려할 만합니다.
UIUC 팀이 Lean4 기반 정형 검증으로 LLM 에이전트 워크플로의 신뢰성을 높이는 프레임워크를 제안했습니다.
핵심 결론
- 벤치 — SWE-Bench-Verified 난이도 높은 부분집합에서 검증 통과 워크플로가 실패 워크플로보다 평균 11.94% 높은 성능.
- 개선 — LeanEvolve로 검증 실패 워크플로를 수정 시 SWE 성능이 평균 7.47% 추가 향상.
- 범위 — 5개 LLM(GPT-4, Claude 3 등)에 대해 실험, 일관된 추세 확인.
방법
- 정형 검증 — Lean4의 의존 타입을 활용해 워크플로의 사전/사후 조건을 명시하고, 실행 궤적의 의미적 일관성을 검증.
- 라이브러리 — FormalAgentLib은 확장 가능한 Lean4 라이브러리로, 에이전트 행동을 형식적으로 모델링하고 검증 실패 지점을 특정.
- 자동 수정 — LeanEvolve는 검증 결과를 바탕으로 워크플로를 자동으로 수정해 성능을 개선.
한계·조건
- 학습 곡선 — Lean4 자체의 진입 장벽이 있어 실제 적용 시 추가 교육이 필요할 수 있습니다.
- 벤치 범위 — SWE-Bench-Verified의 일부 문제와 ELAIP-Bench 일부만 사용, 전체 벤치마크에 대한 일반화는 추가 검증 필요.
- 코드 — GitHub에 공개 예정 — 현재는 논문과 부록만 열람 가능.
편집자 한 줄
정형 검증을 에이전트 워크플로에 적용한 첫 시도라는 점에서 의미가 있습니다. 다만 Lean4 의존성과 벤치 규모를 감안하면 실용성은 좀 더 지켜봐야 할 듯합니다.
- #lean4
- #formal-verification
- #agent
- #swe-bench
- #uiuc
UIUC ScaleML Lab