LLM이 설계한 진화 알고리즘, Lean으로 검증

ai.euno.news 자동 뉴스 요약

대규모 언어 모델(LLM)이 진화 알고리즘을 직접 제안하고, 예상 실행시간 경계를 정리증명기 Lean으로 형식화해 증명하는 에이전트형 설계 파이프라인이 공개됐다. 10월 26일 arXiv에 제출된 논문은 열린 형태의 알고리즘 탐색에서 실험 평가를 쓰지 않고도 설계의 효율성을 기계 검증할 수 있음을 보였다고 주장한다.¹

기존 접근은 역할이 갈렸다. AlphaEvolve 같은 LLM 기반 최적화 휴리스틱 설계는 경험적 성능 측정에 의존하고, LLM을 결합한 자동 정리 증명은 이미 주어진 명제를 증명하는 데 초점을 맞췄다. 이번 파이프라인은 진화 알고리즘 연구의 설계·분석 절차를 여러 단계로 나눠 두 작업을 연결했다. 에이전트가 블랙박스 최적화 알고리즘을 제안하면 Lean으로 작성한 검증 장치가 잘못된 설계를 걸러낸다. 이어 에이전트가 잠재 함수를 정의하고 드리프트 경계를 증명해, 기준 알고리즘보다 예상 실행시간이 개선됨을 보인다.

성과는 문제별 실행시간 차이로 드러난다. CycleUncover 문제에서 파이프라인이 만든 알고리즘의 예상 실행시간은 (O(n^2))였다. 반면 고전적인 (1+1) 진화 알고리즘(EA)은 같은 문제에서 (e^{\Omega(n)})이 필요하다. 정숫값 부분모듈러 최소화 문제에서는 (O(n^{2+2c})), LeadingOnes에서는 최적 차수와 같은 (O(n^2)) 경계를 얻었다. 논문에 따르면 8개 문제군을 대상으로 프런티어 모델을 실행한 15회 가운데 12회가 기계 검증된 예상 실행시간 경계까지 전체 절차를 마쳤다.

단계화 자체도 핵심 요소였다. 이를 제거하고 알고리즘과 실행시간 보장을 한 번에 생성하도록 한 제거 실험에서는, 에이전트가 초기 기준으로 제공된 무작위 탐색을 복제하거나 증명을 완성하지 못했다. 즉 LLM의 단발성 제안보다 제안, 형식화, 검증, 분석을 차례로 수행하는 구조가 결과를 좌우했다.

다만 논문은 알고리즘끼리 경험적으로 비교하지 않았다. 따라서 제시된 결과가 보장하는 것은 Lean이 확인한 이론적 예상 실행시간 경계이며, 실제 구현의 속도나 상수 계수까지 입증한 것은 아니다. 또한 “Lean 명세가 경험적 평가를 대체할 수 있다”는 해석과 최초 사례라는 설명은 저자들의 주장이다. 현재 자료는 1차 arXiv 제출본이어서 후속 검토 결과도 아직 제시되지 않았다.¹

읽기 목록은 이 브라우저에 저장됩니다.