에너지 기반 모델(EBM) 쉽게 이해하기 — 제약 만족으로 추론하는 AI와 형식 검증의 결합

핵심 메시지

• 스도쿠 데모는 도구 사용을 막았을 때 드러난다. 코드 실행이 허용되면 대형 언어모델은 퍼즐을 추론으로 푸는 대신 파이썬 완전 탐색 코드를 짜서 돌린다.
• 에너지 기반 모델은 '다음에 올 단어'를 묻지 않고 '이 답 전체가 조건을 얼마나 잘 만족하는가'를 묻는다. 조건에 맞으면 에너지가 낮고, 규칙을 어기면 높다.
• 추론이 생성이 아니라 최적화가 된다. 좋은 상태를 제약과 목표로 정의한 뒤, 에너지가 더 낮은 상태를 찾아 옮겨 가는 방식이다.
• Logical Intelligence는 에너지 기반 추론 모델 Kona와 형식 검증 시스템 Aleph을 내놨다. Aleph은 PutnamBench 672문제 중 668개, 99.4%에 대해 Lean 증명을 생성했고 Verina에서 100%를 기록했다고 발표했다.
• 이는 기업이 스스로 발표한 수치라 더 많은 기술적 공개가 필요하다. 다만 출력이 Lean 컴파일러로 검사 가능하다는 점에서 일반적인 벤치마크 점수와 성격이 다르다.

쉽게 이해하기

영상은 스도쿠 한 판으로 시작한다. 한 모델은 0.4초 만에 풀었고, 다른 두 모델은 틀렸으며, 나머지는 10분 뒤 시간이 초과됐다. 진행자가 평소 쓰는 프런티어 모델들로 같은 문제를 던졌을 때는 모두 풀었지만, 데모 페이지 하단의 작은 글씨에 답이 있었다. 비교 실험에서는 코드 실행이 막혀 있었던 것이다. 도구를 열어 주면 모델들은 퍼즐을 규칙으로 풀지 않고 파이썬 완전 탐색 코드를 작성해 실행한다. 유용하지만, 사람이 직접 푸는 것과 사람이 '잠깐만요, 푸는 기계를 하나 만들게요'라고 말하는 것은 다른 능력이라는 지적이다.

이 구분이 중요한 이유는 AI가 마주하는 많은 문제가 언어 문제가 아니라 제약 문제이기 때문이다. 스도쿠는 규칙을 한 문장으로 적을 수 있지만, 규칙을 설명하는 것과 실제로 푸는 것은 다르다. 모든 선택이 다른 모든 선택과 맞아떨어져야 하기 때문이다. 여기서 질문이 갈린다. 추론은 다음 토큰을 생성하는 일인가, 아니면 제약을 만족하는 상태를 찾는 일인가.

에너지 기반 모델의 발상은 이름과 달리 단순하다. 가능한 답 하나하나에 점수를 매기고, 잘 맞으면 낮은 에너지, 어딘가 어긋나면 높은 에너지를 준다. 스도쿠라면 완성된 격자 전체를 보고 규칙 위반 여부로 점수를 매긴다. 그래서 모델은 다음에 무엇을 말할지가 아니라 더 나은 배치로 옮겨 가는 일을 한다. 추론이 최적화가 되는 것이다. 증명의 논리적 타당성, 칩 설계의 물리·타이밍 제약, 로봇의 안전 제약, 전력망의 수급 균형처럼 '그럴듯한 설명'으로는 부족한 영역이 여기에 해당한다.

구체적 사례로 Logical Intelligence가 등장한다. 에너지 기반 추론 모델 Kona와 함께, 기계가 검사할 수 있는 증명을 만들어 내는 형식 검증 시스템 Aleph을 내놨다. 회사 발표에 따르면 Aleph은 북미에서 가장 어려운 학부 수학 경시대회 문제를 형식화한 PutnamBench에서 672문제 중 668개, 99.4%에 대해 Lean 증명을 생성했고 외부 Lean 컴파일러로 검증받았다. 형식 문장 15개에서는 반례를 찾아 수정안을 제시하고 고친 명제를 다시 증명했다고도 밝혔다. 진행자는 이것이 증명 패턴을 흉내 내는 수준을 넘어선다는 점을 인정하면서도, 성능 중 얼마가 오케스트레이션·기반 언어모델·탐색·Lean 환경에서 왔는지 공개 자료가 더 필요하다고 선을 긋는다.

마지막으로 얀 르쿤이 왜 이 방향을 지지해 왔는지가 연결된다. 에너지 지형이라는 개념은 1980년대 홉필드 네트워크와 볼츠만 머신에서 이미 쓰였고, 시스템이 더 안정적인 저에너지 상태로 이동한다는 발상도 그때 나왔다. 르쿤이 밀어 온 JEPA는 다음 단어나 모든 픽셀을 예측하는 대신 추상적인 표현 공간에서 예측을 학습한다. 세계의 구조를 배우는 쪽이 JEPA라면, 어떤 상태가 그 구조와 제약에 맞는지 점수를 매기는 쪽이 에너지 기반 모델이라는 정리다. 결론은 하나의 거대한 챗봇이 시와 원자로 제어를 모두 담당하는 그림이 아니라, 소통은 언어모델이, 제약이 많은 추론은 에너지 기반 모델이, 검증은 형식 시스템이 맡는 계층화된 스택이다.

주요 인사이트

• 벤치마크 결과를 볼 때는 도구 사용 허용 여부부터 확인해야 한다. 같은 문제라도 코드 실행을 열어 주면 측정하려던 능력이 아니라 코드 작성 능력을 재게 된다.
• 형식 증명 벤치마크는 최종 답만 맞으면 되는 일반 벤치마크와 성격이 다르다. 증명이 컴파일돼야 하므로 과정이 엉성하면 통과하지 못한다.
• Lean이 검증해 주는 것은 형식화된 명제이지 현실의 요구사항이 아니다. 요구사항을 잘못 형식화하면 시스템은 엉뚱한 명제를 완벽한 확신으로 증명해 낸다. 번역 단계에 사람이 남아 있어야 하는 이유다.
• 에너지 기반 모델은 새로 발명된 것이 아니라 신경망 초기의 아이디어가 돌아온 것에 가깝다. 챗봇의 한계가 드러난 시점에 다시 주목받는다는 점이 이 흐름의 성격을 보여 준다.
• 반도체, 항공우주, 자동차, 금융, 의료, 산업 제어처럼 '아마 맞을 것'으로는 부족한 분야에서는 요구사항을 형식 명제로 옮기고, 증명을 제안하고, 검증기로 확인하는 파이프라인이 실질적 의미를 가진다.

자주 묻는 질문

관련 AI 소식