💻 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

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Leni Aniva, Claire Wang

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

音楽理論を、単なる「こうすべき、こうしてはいけない」という古臭いルールブックとしてではなく、数学的な形が織りなす巨大で目に見えない遊び場として想像してみてください。何世紀もの間、音楽家たちは直感的にこれらの形に従って演奏してきましたが、その形が完璧であることを「証明」できるロボットを作ることはできませんでした。そこで登場するのがPrismriverです。これは、Lean 4と呼ばれる超スマートなコンピュータプログラムの中に構築された新しいデジタル・ツールボックスであり、音楽理論を検証可能な論理のゲームへと変えるために設計されています。

Prismriverを、音楽のためのユニバーサル・トランスレーター（万能翻訳機）だと考えてください。これまでは、ほとんどのコンピュータ音楽ツールは、世界には楽器のチューニング方法が一つしかない（ピアノにあるような12音の「平均律」だけである）と想定していました。それは、世界のあらゆる言語が26文字のアルファベットだけで構成されていると決めつけるようなものです。Prismriverはこのルールを打ち破ります。これにより、あなたはどんな音階でも発明できるようになります。例えば、「クォーター・トーン（ピアノの鍵盤の間にある極めて微細な音）」を持つ音階や、「オクターブ」が主要な反復パターンではない音階さえも可能です。それは、作曲家に、鍵盤が伸び縮みしたり、あるいは消えてしまったりするキーボードを与え、それでもコンピュータがその背後にある数学を理解できるようにするようなものです。

「証明」の遊び場

Prismriverの最も素晴らしい点は、音楽のルールを扱う方法です。通常、作曲家が曲を書いたとき、私たちはただそれを聴いて「うん、いい感じだ」と言うだけです。しかし、Prismriverを使えば、曲を書き、コンピュータにそれがルールに従っていることを証明させることができます。

ブロックの塔を組み立てている場面を想像してください。昔は、ただ積み上げて、崩れないことを祈るしかありませんでした。しかしPrismriverがあれば、魔法の検査官が、次のブロックを置く前に、すべてのブロックの配置が物理法則に適合しているかをチェックしてくれます。もしあなたが、協和的な（調和のとれた）ブロックが必要な場所に、不協和的な（ぶつかり合う）ブロックを置こうとした場合、コンピュータは単に「おっと」と言うのではなく、「この証明は不完全です」とあなたを止めます。

著者らはこれを用いて、対位法（カウンターポイント）という、二つ以上のメロディを編み合わせる古来の技術に取り組みました。彼らは「第一種対位法」（特定の、初心者向けの編み合わせスタイル）のための厳格なルールを記述しました。彼らは単に音楽を作るためのコードを書いたのではありません。作った音楽がルールに従っていることを証明するためのコードを書いたのです。それは、プロットの穴が存在することを数学的に不可能にする物語を書くようなものです。

「タイムトラベル」クロック

音楽は時間の中で展開されます。Prismriverは、時間を扱うための巧妙な方法を持っています。宇宙の始まりからすべてのビートを数える代わりに（それは非常に煩雑になります）、Prismriverは「小節とオフセット」システムを使用します。これは地下鉄の路線図のようなものです。どの駅（小節）にいて、プラットフォームのどのあたり（オフセット）にいるのかを知っています。これにより、曲全体を前後にシフトさせる際も、すべての秒数を再計算する必要がなくなり、非常に簡単になります。また、「ネガティブ・オフセット」も可能であり、これは公式なダウンビートの「前」から始まる音楽的なピックアップ・ノート（アウフタクト）のようなもので、作曲家が好んで使うテクニックです。

「レゴ」のような言語

アクセシビリティを高めるため、PrismriverにはLilyPond（音楽をテキストベースで記述する方法）に似た特別な言語が含まれています。例えば c'4（特定のオクターブのC音）のように入力すれば、コンピュータは即座に理解します。しかし、ここからが真骨頂です。Prismriverはあなたのテキストを受け取り、数学的な整合性をチェックした上で、その結果をMusicXMLというユニバーサルなファイル形式にエクスポートできます。つまり、このハイテクな数学言語で曲を構成し、その完璧さを証明した後、MuseScoreやLilyPondのような標準的な音楽ソフトウェアで開いて、実際の楽器で演奏できるのです。これは、ビデオゲームの中で宇宙船を組み立て、エンジンが作動することを証明してから、その設計図を実際の工場へ送るようなものです。

それが「できないこと」（および、まだできていないこと）

期待を上げすぎないように、Primriverができないことを知っておくことも重要です。

それは魔法の曲生成器ではありません： この論文は、Prismriverが自律的にヒット曲を書けると主張しているわけではありません。これはアルゴリズム作曲のためのツールです。つまり、曲のルールを書く手助けはしてくれますが、メロディを決定するのは依然としてあなた（またはあなたが設計した特定のアルゴリズム）です。
視覚化機能はまだありません： 音楽を再生することはできますが、論文では、音楽に合わせた視覚芸術の生成は「将来の研究課題」であると明記されています。ですから、まだ踊るレーザー光線などは出せません。
西洋音楽に限定されません： 西洋古典音楽を美しく扱いますが、著者らはこれが「ゼナハーモニック（非標準的）」な音階、例えばオクターブの代わりに「トリターブ（3:1の周波数比）」を主要な反復間隔とするボーレン・ピアース音階のようなものにも対応できる柔軟性を持っていると注意深く述べています。

結論

Prismriverは**形式化ライブラリ（formalization library）**です。これは、検証済みの音楽用数学ツールが集まったものであるという、少し専門的な言い方です。著者らは、伝統的な「二面体群（dihedral group）」の数学（和音の回転や反転を記述する複雑な数学）が標準的な12音音楽において完璧に機能することを証明し、それをあなたが想像できるあらゆるチューニングシステムで機能するように一般化することに成功しました。

彼らは「何が歌を美しいのか」という謎を解いたわけではありませんが、音楽理論の証明チェッカーを構築しました。もしあなたが、すべての音が数学的に保証された形で対位法のルールに従う曲を作りたいのであれば、Prismriverは「はい、数学的なチェックを行いました。この曲は有効です」と実際に言える最初のツールなのです。それは、音楽の構成を「推測と試行錯誤のゲーム」から「検証可能な論理のゲーム」へと変え、コンピュータが単に聴かれるだけでなく、「証明される」音楽を作るのを手助けする未来への扉を開いています。

技術要約: Prismriver

問題提起

音楽理論は、精密な数学的言語で表現可能な、豊かな数学的規則と対称性に支配されています。しかし、従来の数学的音楽理論は自然言語による証明に依存しており、それらは人間の誤りに左右されやすく、機械的な検証が不可能であり、計算的な文脈において結果を再利用することもできません。既存の形式化された音楽理論も存在しますが、その多くは特定の調律体系（12平均律など）に限定されているか、あるいは統一されたフレームワーク内でのアルゴリズム作曲や分析を行う能力を欠いています。任意の調律体系をサポートし、音楽的特性の機械検証された証明を可能にし、かつこれらの証明をアルゴリズム作曲および入出力機能と統合できる形式化が求められています。

手法

著者らは、Lean 4で構築された、音楽理論とアルゴリズム作曲のための形式化ライブラリであるPrismriverを提案しています。Leanは関数型プログラミング言語であると同時にインタラクティブな定理証明器でもあり、これにより音楽構造の定義、定理の証明、および音楽の生成が可能になります。

コアとなる表現

抽象的な音階と調律:
- Prismriverは、制限のない汎用的なピッチ型 $P$ としてPseudoScaleを定義します。これにより、実数周波数のような表現が可能になります。
- Scaleは、ピッチ型 $P$ と、 $P$ に作用するアーベル加法群 $I$ （ $I$ -トースター）を備えたインターバル型 $I$ として定義されます。これは、標準的な12音体系を超えたピッチクラスの概念を一般化するものです。
- ゼナハーモニック（異種調律）への対応: 本ライブラリは、非平均律の調律、四分音、およびオクターブ以外の基本間隔（例：ボヘン・ピアスのトリタヴ）を持つ音階に対応しています。12平均律において音響的に等価であっても、エンハーモニック（異名同音）なピッチ（例： $C\sharp$ と $D\flat$ ）を区別します。これは、ピタゴラス音階のような非平均律のシステムを分析する上で極めて重要です。
時間と音符:
- 時間は、順序付きアーベル加法群 $T$ としてモデル化されます。
- 音符は、ピッチと持続時間のペア $(P, T)$ として定義されます。
- MeasuredTime型は、整数（小節番号）と有理数（小節内のオフセット）の積として実装されており、総拍数を再計算することなく、アニクル（前置拍）やシフトする音楽の分析を容易にします。
移調アクションと二面体群:
- ライブラリは、移調と反転の概念を一般化します。TransposeActionは、任意の音階に作用する平行移動（ $r_i$ ）および鏡映（ $sr_{a,i}$ ）を含む操作を定義します。
- 著者らは、12平均律の下では、これらの一般化された移調アクションが、三和音に対する二面体群 $D_{12}$ の作用と等価であることを証明しています。これにより、抽象的な群論と、先行文献（例：[19]）に見られる特定の西洋音楽理論モデルとの間の架け橋となります。
モナドによる作曲:
- アルゴリズム作曲は、CompositionTモナドによって処理されます。このモナドは「現在の時刻」カーソルを追跡し、カーソルの移動、イベント（アーティキュレーション）の追加、および音符の追加を行うプリミティブを提供します。
- Score.foldlMモナドは、進行中のイベントのリストを畳み込む（fold）ことで、スコアの分析を可能にします。
- これらのモナド構造により、LeanのLawfulMonadクラスを用いて、作曲アルゴリズム（例：生成された対位法が特定の規則に従っていることの証明）を検証することができます。
入出力:
- DSL: ユーザーがテキストベースの構文を用いて音楽を入力できる、LilyPondに似たドメイン固有言語（DSL）を提供します。このDSLは、揮発性を抑えるために相対表記ではなく固定ピッチ表記を使用しています。
- エクスポート: スコアは、LilyPondやMuseScoreなどのツールとの互換性のために、時間軸形式からパート形式に変換されたMusicXMLとしてエクスポートされます。
- 再生: #playディレクティブは、式を展開し、インタラクティブな再生のためにAldaプロセスを起動します。

主な貢献

音楽理論の形式化: ピッチ、臨時記号、音階、和音、持続時間、およびパートをLean 4で包括的に形式化したライブラリ。
一般化された調律の互換性: 非平均律のシステムやオクターブ以外の基本間隔を持つ音階を含む、ゼナハーモニックな音階へのサポート。これにより12平均律の制限を克服しています。
証明可能な還元: 12平均律の下では、一般化された移調アクションが三和音に対する $D_{12}$ 二面体群の作用に等しいという形式的な証明。
モナドによるアルゴリズム作曲: モナドのプリミティブを用いて音楽を構成・分析するためのフレームワーク。これにより、作曲アルゴリズム（例：第一種対位法）の検証が可能になります。
相互運用性: 外部音楽ソフトウェアとの互換性のためのMusicXMLエクスポートや、Aldaを介した直接再生を備えた、カスタムDSLの統合。

結果と実装

論文では、以下の実装を通じてPrismriverの有用性を実証しています。

対位法作曲: 著者らは第一種対位法の規則のサブセットを実装しました。彼らは和声的・旋律的間隔、協和音、および特定の制約（例：三全音の転回点の禁止）に関する述語を定義しました。これらの述床を用いて、プログラム的に対位法を構築し、生成された作曲が第一種対位法の規則を満たしていることを証明しました。
和音進行分析: パヘルベルの『カノン』の和音進行を、移調アクションと和音の転回という観点から分析するために本ライブラリを使用し、一般化された二面体群作用モデルを検証しました。
コード例: 論文には、間隔の定義、三和音に対する二面体群作用の実装、および（Necrofantasiaに基づく）メロディを生成するための作曲モナドの使用を示すコードスニペットが含まれています。

意義

Prismriverは、検証可能なアルゴリズム作曲および伴奏生成への扉を開くと主張されています。音楽理論を証明助手（proof assistant）で形式化することにより、著者らは以下を可能にしました。

機械的検証: 音楽的な証明におけるエラーはコンピュータによって検出されるため、手書きの証明に伴う非効率性が排除されます。
再利用性: 結果やプリミティブは、将来の証明や作曲において機械的に再利用できます。
柔軟性: ユーザーはカスタムの調律システムや音楽的プリミティブを定義できるため、成長し続ける再利用可能な形式化ライブラリを促進します。
統合: 理論的な音楽分析と実践的な作曲ツールの間のギャップを埋め、標準的なソフトウェアで再生可能なMusicXMLの生成を可能にします。

著者らは、Prismriverを、Lulu（一般化された調律プリミティブを欠く）やHarmTraceまたはMezzo（特定の型システムエンコーディングや調律体系に限定されている）といった既存のツールの一歩先を行くものとして位置付けています。Leanの表現力を活用することで、Prismriverは音楽理論が証明可能かつ実行可能である汎用的な環境を提供します。