비선형 동역학 시스템에 대한 유효한 Lyapunov 함수를 찾는 것은 여전히 어려운 문제이다. 기존의 신경망 기반 접근 방식은 확장 가능한 검증 및 해석 가능성의 제한이라는 두 가지 주요 문제점을 갖는다. 본 논문에서는 이러한 문제점을 해결하기 위해, 해석적 Lyapunov 함수(local)를 구성하는 트랜스포머 기반의 end-to-end 프레임워크를 제안한다. 이 프레임워크는 후보 Lyapunov 함수를 생성하는 트랜스포머 기반 트레이너와 후보 표현식을 검증하고 위험 추구 정책 경사도를 통해 모델을 개선하는 falsifier로 구성된다. 본 모델은 사전 훈련을 사용하지 않고 강화 학습(RL)을 통해 처음부터 훈련되며, 고차원 및 비다항 시스템에 대한 지역 Lyapunov 함수를 찾는 데 성공한다. 후보의 해석적 특성을 고려하여, 훈련 중에는 효율적인 최적화 방법을, 최종 검증에는 형식적 검증 도구를 사용한다. 최대 10차원의 다양한 비선형 동역학 시스템에서 접근 방식의 효율성을 보여주고, 이전에는 제어 분야에서 확인되지 않았던 Lyapunov 함수를 발견할 수 있음을 보여준다. 전체 구현은 Github에서 확인 가능하다.
