計算物理班紹介

計算物理班へようこそ！

　初めまして。知っている人はこんにちは。Physics Lab. 2025 計算物理班班長の平松です。この記事では、計算物理の魅力や普段の活動について、最後に僕が興味を持っている型理論について紹介します。

計算物理とは？

　計算物理は、物理学の問題を数値的に解くために計算機を使ってシミュレーションや解析を行う学問分野です。理論物理と実験物理の橋渡しとしての役割を果たす、新しめながら重要な分野になっています。物理には解析的に解けない問題がたくさんあります。物理好きの高校生なら知っているかもしれませんが、例えば3体問題は一般に解析解を得られません¹。そこで活躍するのが計算物理で、計算機によるシミュレーションで数値的に解くことができます。本質は計算機による単なるゴリ押しですが、泥臭くてもいいからなんとか解いてやろうという姿勢は僕は結構好きです。今ならChatGPTにお願いすれば簡単にコードを書いてくれるので、興味を持ったら自分で実験してみてください。こういう気軽さも計算物理の魅力ですよ？

　　　　　　　　　　　　　実際にお願いして出力されたシミュレーション

普段の活動

　今年度の計算物理班では以下のゼミが開かれています。

Deep Learningゼミ

　今年のノーベル物理学賞だった深層学習についてのゼミで、「基礎からの物理学とディープラーニング入門」²という本を読んでいます。統計物理班のページ³で紹介されているように、深層学習で使われるニューラルネットワークの概念は統計力学に強い影響を受けています。例えば、基本的な学習モデルの1つであるBoltzmannマシンは統計力学のIsing模型とそっくりで、初めて見た時は感動を通り越して不思議な気分になったものです。

Boltzmannマシンのエネルギー関数
$$E(\mathbf{s}) = -\sum_{i < j} w_{ij} s_i s_j - \sum_i b_i s_i$$

Ising模型のエネルギー関数
$$E(\mathbf{s}) = -\sum_{\langle i, j \rangle} J_{ij} s_i s_j - \sum_i h_i s_i$$

上の2式はそれぞれエネルギー関数を書いたものですが、結合の仕方に違いがある程度でほとんど同じです。つまり、2つの問題は等価と言え、片方が解けるならもう片方も解けることになります。Boltzmannマシンが出てきた頃に統計力学はとっくに出来上がっていたので、深層学習の研究者は物理学の成果を十分に活用できました。思いもよらない分野で応用先が見つかるの、良いですよね。

自然言語処理ゼミ

　今流行りの自然言語処理についてのゼミです。「言語処理のための機械学習入門」⁴という本を読んでいる・・・らしいです(僕は参加していないので詳しくは不明)。自然言語処理の応用先としてはChatGPTなどがあり、今一番ホットな分野ではないでしょうか。僕も時間があれば参加したかったです。

型理論とは？

　さて、ここからは僕が今興味を持っている型理論についてです。前年度Physics Lab. 2024の計算物理班では型理論ゼミがあり、「Introduction to Homotopy Type Theory」⁵という本を読んでいます(実は1年経った今もまだ続いています)。型理論の特にHoTT(Homotopy Type Theory)という理論を勉強しています。型理論は集合や命題の形式的な記述を可能にする枠組みの一つで、元々は数学の論理的基盤を再構築する試みで生まれました。型理論の理念には、数学の"証明"は"構成可能"であるべきという考えがあります。どういうことかというと、数学的な対象が存在することを証明するには実際に構成することが必要だという考えで、構成できないものには証明も考えられないというある意味自然な考えです。

　例えば、$x=2$という等式の変数依存の命題(型理論ではこのような変数依存命題を"依存型"と言います)があったとしましょう。$x$に$1$が代入されるなら$1=2$となりこの時はFalseが返されます。これの証明(型理論では"項"と言います)は$2=2$になり、この時はTrueが返されます。さて、$x=2$という型には$2=2$という項をとれたので証明が構成可能であることが示されました。では、もし$2=2$が見つからない世界があったとしたら、$x=2$には証明は存在すると断言できるのでしょうか？

　この話はかなり具体的に書いたのですが、普通の型理論はもっと抽象的で、集合論や圏論が好きな人におすすめです。型理論は実際にプログラミングのエラーを防ぐのに使われたり、プログラミング言語設計の理論的背景になったりしています。中には、これからはコンピュータで型理論を基盤に数学をやるべきだなんて主張する人も⁶。数学がコンピュータに支配される日も遠くないのかもしれませんね。

最後に

　ここまで読んでくださりありがとうございました！計算物理班では五月祭で展示企画をやる予定なので、興味を持ってくださった方はぜひいらしてください。Physics Lab. 2025をどうぞよろしくお願いします。

1. 理由は系の自由度に対して保存量が足りないから、砕けて言うと予測に使える情報が足りないからです。解析力学をやると分かります。 ↩

2. ―Pythonで実践―　基礎からの物理学とディープラーニング入門 (エンジニア入門シリーズ112) ↩

3. 統計物理班紹介 ↩

4. 自然言語処理シリーズ1 言語処理のための機械学習入門 ↩

5. ゼミで使っているのはIntroduction to Homotopy Type Theoryですが、有名なのはHoTT Book ↩

6. Vladimir Voevodskyという人。HoTTの第一人者だった。 ↩