SATNet: 딥 러닝과 논리적 추론을 연결하는 미분 가능한 만족성 해소기 사용

현대 AI 시스템의 주요 목표 중 하나는 딥 러닝 아키텍처 내에 논리적 추론을 통합하는 것이다. 본 논문에서는 이 목표를 달성하기 위한 새로운 방향으로, 큰 딥 러닝 시스템의 루프에 통합될 수 있는 미분 가능한 (부드러운) 최대 만족성 문제 (MAXSAT) 솔버를 소개한다. 우리의 (근사) 솔버는 MAXSAT 문제와 관련된 반정부호 프로그램 (SDP, Semidefinite Program)을 해결하기 위한 빠른 좌표 하강법을 기반으로 한다. 우리는 이 SDP의 해를 통해 해석적으로 미분하는 방법과 효율적으로 역전파 문제를 해결하는 방법을 설명한다. 우리는 이 솔버를 엔드투엔드 학습 시스템에 통합함으로써, 최소한의 감독 하에서 어려운 문제들의 논리 구조를 학습할 수 있음을 보여준다. 특히, 싱글 비트 감독(딥 네트워크에서 전통적으로 어려운 작업)을 사용하여 패리티 함수를 학습하고, 예제만으로 9x9 스도쿠 게임을 플레이하는 방법을 학습할 수 있음을 보여준다. 또한, 우리의 MAXSAT 솔버와 전통적인 컨볼루션 아키텍처를 결합하여 스도쿠 퍼즐 이미지를 해당 논리적 해로 매핑하는 "시각적 스도쿠" 문제를 해결하였다. 따라서 우리의 접근 방식은 딥 러닝 내에 논리 구조를 통합하는 데 있어 잠재력을 보여주고 있다.