💻 computer science

Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4

이 논문은 검증 가능한 알고리즘 작곡을 가능하게 하고, 평균율 조율을 넘어 일반화하며, 대위법을 모델링하고, 커스텀 DSL 및 MusicXML 내보내기를 통해 표준 음악 소프트웨어와 상호 운용할 수 있도록 음악 이론을 정형화한 Lean 4 라이브러리인 Prismriver를 소개한다.

원저자: Leni Aniva, Claire Wang

게시일 2026-07-14

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Leni Aniva, Claire Wang

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

음악 이론을 단순히 "이것을 하라, 저것을 하지 마라"는 식의 먼지 쌓인 규칙 책이 아니라, 수학적 도형들로 이루어진 거대하고 보이지 않는 놀이터라고 상상해 보십시오. 수 세기 동안 음악가들은 직관적으로 이러한 도형들을 가지고 놀아왔지만, 그 도형들이 완벽하다는 것을 증명할 수 있는 로봇을 만들어내지는 못했습니다. 바로 그 지점에서 Prismriver가 등장합니다. Prismriver는 Lean 4라는 초지능형 컴퓨터 프로그램 내부에 구축된 새로운 디지털 도구 상자로, 음악 이론을 검증 가능한 논리 게임으로 바꾸기 위해 설계되었습니다.

Prismriver를 음악을 위한 보편적인 번역기라고 생각하십시오. 이 전까지 대부분의 컴퓨터 음악 도구들은 세상에 악기를 조율하는 방법이 표준적인 "평균율"(피아노에서 볼 수 있는 12개의 음) 하나뿐이라고 가정했습니다. 이는 마치 세상의 모든 언어가 오직 26개의 알파벳만을 가지고 있다고 가정하는 것과 같습니다. Prismriver는 이 규칙을 깨뜨립니다. 이를 통해 여러분은 "쿼터 톤"(피아노 건반 사이의 미세한 음)이나 "옥타브"가 주요 반복 패턴이 아닌 스케일 등, 여러분이 원하는 어떠한 스케일이라도 발명할 수 있습니다. 이는 작곡가에게 건반의 간격을 늘리거나 줄이거나 혹은 사라지게 할 수 있는 키보드를 주는 것과 같으며, 컴퓨터는 여전히 그 뒤에 숨겨진 수학을 이해할 수 있습니다.

"증명" 놀이터

Prismriver의 가장 멋진 점은 음악 규칙을 다루는 방식입니다. 보통 작곡가가 곡을 쓰면, 우리는 그저 듣고 "그래, 좋다"라고 말합니다. 하지만 Prismriver를 사용하면, 곡을 쓰고 나서 컴퓨터에게 그 곡이 규칙을 따르고 있는지 증명해달라고 요청할 수 있습니다.

여러분이 블록 탑을 쌓고 있다고 상상해 보십시오. 옛날 방식이라면 그냥 블록을 쌓으며 무너지지 않기를 바랐을 것입니다. 하지만 Prismriver를 사용하면, 마법 같은 검사관이 여러분이 다음 블록을 떨어뜨리기도 전에 물리 법칙에 따라 모든 블록의 배치를 확인합니다. 만약 여러분이 "협화음"이 필요한 곳에 "불협화음" 블록(충돌하는 음)을 놓으려 한다면, 컴퓨터는 단순히 "앗" 하고 넘어가는 것이 아니라, 동작을 멈추고 "이 증명은 불완전합니다"라고 말할 것입니다.

저자들은 이를 대위법(counterpoint), 즉 둘 이상의 멜로디를 엮어내는 고대의 예술을 다루는 데 사용했습니다. 그들은 "제1종 대위법"(특정 초보자용 멜로디 엮기 스타일)에 대한 엄격한 규칙 세트를 작성했습니다. 그들은 단순히 음악을 만드는 코드를 쓴 것이 아니라, 자신들이 만든 음악이 규칙을 따른다는 것을 증명하는 코드를 썼습니다. 이는 마치 플롯의 구멍(설정 오류)이 수학적으로 존재할 수 없도록 설계된 이야기를 쓰는 것과 같습니다.

"시간 여행" 시계

음악은 시간 속에서 일어납니다. Prismriver는 이를 처리하기 위한 영리한 방법을 가지고 있습니다. 우주의 시작부터 모든 비트를 일일이 세는 대신(이는 매우 복잡해집니다), Prismriver는 "마디와 오프셋(offset)" 시스템을 사용합니다. 이는 지하철 노선도를 생각하면 쉽습니다. 여러분은 어느 역(마디)에 있는지, 그리고 플랫폼의 어느 지점(오프셋)에 있는지를 알 수 있습니다. 덕분에 노래 전체를 앞뒤로 이동할 때 모든 초 단위의 시간을 다시 계산할 필요 없이 매우 쉽게 옮길 수 있습니다. 또한 "음수 오프셋(negative offsets)"을 허용하는데, 이는 작곡가들이 즐겨 사용하는 기법으로, 공식적인 다운비트(강박)가 시작되기 전에 시작되는 음악적 픽업 노트를 구현할 수 있게 해줍니다.

"레고" 언어

접근성을 높이기 위해, Prismriver는 텍-기반 방식인 LilyPond와 유사한 특별한 언어를 포함하고 있습니다. 여러분이 c'4(특정 옥타브의 C 음)와 같이 입력하면 컴퓨터는 즉시 이를 이해합니다. 하지만 핵심은 이것입니다. Prismriver는 여러분의 텍스트를 가져와 수학적 검증을 거친 후, MusicXML이라는 보편적인 파일 형식으로 결과물을 내보낼(export) 수 있다는 점입니다. 즉, 여러분은 이 고도의 수학적 언어로 곡을 작곡하고, 그 완벽함을 증명한 뒤, MuseScore나 LilyPond 같은 표준 음악 소프트웨어에서 열어 실제 악기로 연주할 수 있습니다. 이는 비디오 게임에서 우주선을 만들고 엔진이 작동함을 증명한 뒤, 그 설계도를 실제 공장으로 보내는 것과 같습니다.

이것이 아닌 것 (그리고 아직 되지 않은 것)

기대가 너무 높아지지 않도록 Prismriver가 하지 않는 일을 아는 것도 중요합니다.

마법 같은 곡 생성기가 아닙니다: 이 논문은 Prismriver가 스스로 히트곡을 쓸 수 있다고 주장하지 않습니다. 이것은 알고리즘 작곡을 위한 도구입니다. 즉, 노래의 규칙을 쓰는 것을 도와주지만, 멜로디를 결정하는 것은 여전히 여러분(또는 여러분이 설계한 특정 알고리즘)의 몫입니다.
아직 시각적 기능을 제공하지 않습니다: 음악을 재생할 수는 있지만, 논문은 음악에 어울리는 시각 예술을 생성하는 것은 "향후 과제"라고 명시했습니다. 따라서 아직 춤추는 레이저는 없습니다.
서양 음악에 국한되지 않습니다: 서양 클래식 음악을 훌륭하게 다루지만, 저자들은 이 도구가 Bohlen-Pierce 스케일처럼 주요 반복 간격이 옥타브가 아닌 '트리타브(tritave, 3:1 주파수 비율)'인 "엑소하모닉(xenharmonic, 비표준)" 스케일에도 유연하게 대응하도록 설계되었다고 신중하게 밝히고 있습니다.

결론

Prismriver는 **정형화 라이브러리(formalization library)**입니다. 이는 검증된 수학적 도구들의 모음이라는 뜻입니다. 저자들은 기존의 "이면군(dihedral group)" 수학(코드가 어떻게 회전하고 뒤집히는지 설명하는 복잡한 방식)이 표준 12음 음악에 완벽하게 작동함을 입증했으며, 이를 여러분이 상상할 수 있는 어떠한 조율 시스템에서도 작동하도록 일반화하는 데 성공했습니다.

그들은 "무엇이 노래를 아름답게 만드는가"라는 미스터리를 해결한 것이 아니라, 음악 이론을 위한 **증명 검사기(proof-checker)**를 구축한 것입니다. 만약 여러분이 모든 음이 대위법의 규칙을 수학적으로 반드시 따르도록 보장되는 곡을 쓰고 싶다면, Prismriver는 "네, 수학적 검증을 마쳤으며 이 곡은 유효합니다"라고 실제로 말할 수 있는 최초의 도구입니다. 이는 음악 작곡을 '추측과 확인'의 게임에서 '검증된 논리'의 게임으로 바꾸어 놓으며, 컴퓨터가 단순히 들리는 음악을 넘어 증명된 음악을 함께 작곡할 수 있는 미래의 문을 열어줍니다.

기술 요약: Prismriver

문제 정의

음악 이론은 정밀한 수학적 언어로 표현될 수 있는 풍부한 수학적 규칙과 대칭성에 의해 지배됩니다. 그러나 전통적인 수학적 음악 이론은 자연어 증명에 의존하며, 이는 인간의 오류에 취약하고, 기계적 검증이 불가능하며, 계산적 맥락에서 결과를 재사용할 수 없다는 단점이 있습니다. 기존의 음악 이론 형식화 모델들이 존재하기는 하지만, 많은 경우 특정 조율 체계(예: 12평균율)에 국한되어 있거나, 통합된 프레임워크 내에서 알고리즘 작곡 및 입출력을 수행하는 능력이 부족합니다. 따라서 임의의 조율 체계를 지원하고, 음악적 속성에 대한 기계 검증된 증명을 허용하며, 이러한 증명을 알고리즘 작곡 및 입출력 기능과 통합할 수 있는 형식화가 필요합니다.

방법론

저자들은 Lean 4로 구축된 음악 이론 및 알고리즘 작곡을 위한 형식화 라이브러리인 Prismriver를 제시합니다. Lean은 함수형 프로그래밍 언어인 동시에 대화형 정리 증명기 역할을 수행하여, 라이브러리가 음악적 구조를 정의하고, 이에 대한 정리를 증명하며, 음악을 생성할 수 있게 합니다.

핵심 표현

추상적 음계와 조율:
- Prismriver는 PseudoScale을 제한이 없는 일반적인 피치 타입 $P$ 로 정의하여, 실수 형태의 주파수와 같은 표현을 가능하게 합니다.
- Scale은 피치 타입 $P$ 와 인터벌(간격) 타입 $I$ 로 구성된 것으로 정의되며, 여기서 $I$ 는 $P$ 에 작용하는 아벨 가법 군(abelian additive group)( $I$ -torsor)을 형성합니다. 이는 표준 12음 체계를 넘어선 음계 개념을 일반화합니다.
- Xenharmonic(이음계) 지원: 이 라이브러리는 비평균율 조율, 쿼터톤(quartertones), 그리고 옥타브 이외의 기본 간격을 가진 음계(예: 트리타브를 가진 보렌-피어스 음계)를 수용합니다. 이는 12평균율에서 음향적으로 동일하더라도 $C\sharp$ 와 $D\flat$ 처럼 이음적(enharmonic)으로 다른 피치를 구분하도록 하며, 이는 피타고라스 조율과 같은 비평균율 체계를 분석하는 데 매우 중요합니다.
시간과 음표:
- 시간은 순서가 있는 아벨 가법 군 $T$ 로 모델링됩니다.
- 음표는 피치와 지속 시간을 갖는 쌍 $(P, T)$ 로 정의됩니다.
- MeasuredTime 타입은 정수(마디 번호)와 유리수(마디 내 오프셋)의 곱으로 구현되어, 전체 비트 수를 다시 계산하지 않고도 픽업(pickups) 및 음악의 이동을 분석할 수 있도록 합니다.
이조 액션과 이면체 군(Dihedral Groups):
- 라이브러리는 이조(transposition)와 전위(inversion)의 개념을 일반화합니다. 저자들은 임의의 음계에 작용하는 평행 이동( $r_i$ ) 및 반사( $sr_{a,i}$ ) 연산을 포함하는 TransposeAction을 정의합니다.
- 저자들은 12평균율 하에서 이러한 일반화된 이조 액션이 삼화음에 작용하는 이면체 군 $D_{12}$ 의 작용과 동치임을 증명합니다. 이는 추상적인 군론과 기존 문헌(예: [19])에서 발견되는 특정 서양 음악 이론 모델 사이의 간극을 메워줍니다.
모나딕 작곡(Monadic Composition):
- 알고리즘 작곡은 CompositionT 모나드를 통해 처리됩니다. 이 모나드는 "현재 시간" 커서를 추적하며, 커서를 이동시키고, 이벤트(아티큘레이션)를 추가하며, 음표를 추가하는 프리미티브(primitives)를 제공합니다.
- Score.foldlM 모나드는 진행 중인 이벤트 리스트를 폴딩(folding)함으로써 스코어를 분석할 수 있게 합니다.
- 이러한 모나딕 구조를 통해, Lean의 LawfulMonad 클래스를 사용하여 생성된 대위법이 특정 규칙을 준수하는지(예: 생성된 대위법이 특정 규칙을 따르는지) 검증하는 작곡 알고리즘을 검증할 수 있습니다.
입출력:
- DSL: 사용자가 텍스트 기반 구문을 사용하여 음악을 입력할 수 있는 LilyPond 스타일의 도메인 특화 언어(DSL)를 제공합니다. 이 DSL은 변동성을 줄이기 위해 상대적 표기법 대신 고정 피치 표기법을 사용합니다.
- 내보내기: 스코어는 MusicXML(시간 중심 포맷)로 내보내지며, 이후 LilyPond나 MuseScore와 같은 도구와의 호환성을 위해 파트별(part-wise) 포맷으로 변환됩니다.
- 재생: #play 디렉티브는 표현식을 구체화하고 대화형 재생을 위해 Alda 프로세스를 실행합니다.

주요 기여

음악 이론의 형식화: 피치, 악센트, 음계, 화음, 지속 시간 및 파트를 Lean 4로 형식화한 포괄적인 라이브러리 구축.
일반화된 조율 호환성: 12평균율의 한계를 넘어 비평균율 음계 및 옥타브 이외의 기본 간격을 가진 음계를 포함한 xenharmonic 음계 지원.
증명 가능한 축소(Provable Reduction): 12평균율 하에서 일반화된 이조 액션이 삼화음에 대한 $D_{12}$ 이면체 군 작용과 동치임을 보여주는 공식적인 증명.
모나딕 알고리즘 작곡: 모나딕 프리미티브를 사용하여 음악을 작곡하고 분석하는 프레임워크를 제공하여, 작곡 알고리즘(예: 1종 대위법)의 검증을 가능하게 함.
상호 운용성: 외부 음악 소프트웨어와의 호환성을 위한 MusicXML 내보내기 및 직접 재생을 위한 Alda와의 연동을 포함한 커스텀 DSL 통합.

결과 및 구현

논문은 다음과 같은 구현을 통해 Prismriver의 유용성을 입증합니다:

대위법 작곡: 저자들은 1종 대위법(first species counterpoint) 규칙의 일부를 구현했습니다. 이들은 화성적 및 선율적 간격, 협화음, 그리고 특정 제약 조건(예: 트리톤 전환점 금지)에 대한 술어(predicates)를 정의했습니다. 이러한 술어를 사용하여 프로그래밍 방식으로 대위법을 구성하고, 결과물로 생성된 작곡이 1종 대위법의 규칙을 만족함을 증명했습니다.
화성 진행 분석: 라이브러리는 이조 액션과 화음 전위의 관점에서 파헬벨의 *캐논 D장조(Canon in D)*의 화성 진행을 분석하는 데 사용되었으며, 이를 통해 일반화된 이면체 군 모델을 검증했습니다.
코드 예시: 논문에는 간격(interval)의 정의, 삼화음에 대한 이면체 군 작용의 구현, 그리고 멜로디(Necrofantasia 기반)를 생성하기 위한 작곡 모나드의 사용을 보여주는 코드 스니펫이 포함되어 있습니다.

의의

본 논문은 Prismriver가 검증 가능한 알고리즘 작곡 및 반주 생성의 문을 열었다고 주장합니다. 음악 이론을 증명 보조기에 형식화함으로써 저자들은 다음을 가능하게 합니다:

기계적 검증: 음악적 증명의 오류를 컴퓨터가 감지할 수 있어, 수기로 작성된 증명의 비효ist를 제거합니다.
재사용성: 결과와 프리미티브를 향후의 증명 및 작곡에 기계적으로 재사용할 수 있습니다.
유연성: 사용자가 커스텀 조율 체계와 음악적 프리미티브를 정의할 수 있게 하여, 성장하고 재사용 가능한 음악 형식화 라이브러리를 육성합니다.
통합: 이론적 음악 분석과 실제 작곡 도구 사이의 간극을 메워, 표준 소프트웨어에서 연주 가능한 MusicXML을 생성할 수 있게 합니다.

저자들은 Prismriver를 (일반화된 조율 프리미티브가 부족한) Lulu나 (특정 타입 시스템 인코딩 또는 조율 체계에 국한된) HarmTrace 또는 Mezzo보다 진보된 단계로 위치시킵니다. Lean의 표현력을 활용함으로써, Prismriver는 음악 이론이 증명됨과 동시에 실행될 수 있는 다재다능한 환경을 제공합니다.