PyTorch Tabular による表形式データの深層学習

ちょっくら機械学習ネタ。基本的に Python 書きたくないのでたまにしかやらない。

PyTorch Tabular とは

分類や回帰などの表形式データに対する機械学習には XGBoost, LightGBM などの勾配ブースティング手法が有効であることが知られている。一方で、近年になって表形式データに対する深層学習ベースの手法が提案されており、勾配ブースティングに匹敵する性能を出しつつある。詳細は以下のブログの記事を参照のこと。

deep-and-shallow.com

PyTorch Tabular は表形式データに対する深層学習のフレームワークである。お馴染みの深層学習フレームワークである PyTorch や PyTorch Lightning の上に実装されており、特に手軽に表形式データ(pandas のデータフレーム)に対する深層学習を実現することを狙いとしている。具体的には、深層学習のための高レベルな API が提供されていたり、 最新手法(Neural Oblivious Decision Ensembles for Deep Learning on Tabular DataTabNet: Attentive Interpretable Tabular Learning)の実装が提供されている。Githubリポジトリは以下であるが、2020年の12月に開発が始まったばかりであり、まだまだ開発途上といった感じである。

github.com

PyTorch Tabular のインストール

Github の手順に記載されているとおり、まず PyTorch の公式 から PyTroch をインストールする。このときマシンの GPU に合ったバージョンの CUDA を選択するようにする。マシンが Linux の場合は nvidia-cuda-toolkit パッケージの nvcc --version コマンドとか叩けばよい。詳細は以下。

How to get the CUDA version? - Stack Overflow

あとは pip でインストールするだけ。

$ pip install pytorch_tabular[all]

PyTorch Tabular を動かしてみる

PyTorch Tabular を使って、深層学習による簡単な分類(classification)のプログラムを実装してみた。そのソースコードの一部を以下に示してゆく。

まずは適当なデータセットを入手するところを以下に示す。

from sklearn.datasets import make_classification
def make_mixed_classification(n_samples, n_features, n_categories):
    X,y = make_classification(n_samples=n_samples, n_features=n_features, ...)
    ...

data, cat_col_names, num_col_names = make_mixed_classification(n_samples=10000, n_features=20, n_categories=4)
train, test = train_test_split(data, random_state=42)
train, val  = train_test_split(train, random_state=42)

sklearn.datasets の make_classification 関数を用いて、適当な分類のためのサンプルデータを生成している。n_samples=10000 とすることで、データセットのサイズを10,000 件としている。このデータセットを training set, validation set, test set に分割している。このあたりの用語がややこしくなったら Wikipedia のページ を見るべし。

つぎにモデルを定義する部分を以下に示す。

data_config = DataConfig(
    target=['target'], #target should always be a list. Multi-targets are only supported for regression. Multi-Task Classification is not implemented
    continuous_cols=num_col_names,
    categorical_cols=cat_col_names,
)
trainer_config = TrainerConfig(
    auto_lr_find=True, # Runs the LRFinder to automatically derive a learning rate
    batch_size=1024,
    max_epochs=100,
    gpus=1, #index of the GPU to use. 0, means CPU
)
optimizer_config = OptimizerConfig()

model_config = CategoryEmbeddingModelConfig(
    task="classification",
    layers="1024-512-512",  # Number of nodes in each layer
    activation="LeakyReLU", # Activation between each layers
    learning_rate = 1e-3
)

tabular_model = TabularModel(
    data_config=data_config,
    model_config=model_config,
    optimizer_config=optimizer_config,
    trainer_config=trainer_config,
)

PyTorch Tabular ではTabularModel というモデルを構築する。これに与えるパラメータは DataConfig, TrainerConfig, OptimizerConfig, CategoryEmbeddingModelConfig の4つであり、ニューラルネットワークアーキテクチャなどを指定している。このあたりを手軽にカスタマイズできるのがこのフレームワークの強みである。冒頭であった最新手法のモデルをどう構築できるのかはよく分かっていない。現状ドキュメンテーションが十分でないので、使い方を知るにはソースコード読む必要がありそう。

それにしても "classification" みたいな文字列を関数の引数に与えるのって バグの温床だと思うんだがあまり気にしないのかな。有限個の選択肢を指定するだけなんだから enum を定義してほしい。

最後に、データセットのデータを用いて学習を実行する。

tabular_model.fit(train=train, validation=val)
result = tabular_model.evaluate(test)

もし Jupyter Notebook を使っていて、このとき Widget Javascript not detected. It may not be installed or enabled properly. というエラーが発生する場合は以下を参照。プログレスバーの描画が上手くいっていない状況である。

python - Jupyter notebook: Widget Javascript not detected - Stack Overflow

学習の結果として、以下のような結果がレポートされる。データセットのサイズを 10,000 としたときの test set の accuracy で 0.78。なにも考えずに適当に実行してこの精度ならなかなかよいんじゃないか。ちなみに学習のための乱数のシードを固定してないので、実行ごとに異なる結果がレポートされる。

--------------------------------------------------------------------------------
DATALOADER:0 TEST RESULTS
{'test_accuracy': tensor(0.7776, device='cuda:0'),
 'train_accuracy': tensor(0.6200, device='cuda:0'),
 'train_loss': tensor(0.7699, device='cuda:0'),
 'valid_accuracy': tensor(0.7627, device='cuda:0'),
 'valid_loss': tensor(0.5853, device='cuda:0')}
--------------------------------------------------------------------------------

おまけとして、データセットのサイズを少なめの 1,000 にしたときの実行結果は以下である。

--------------------------------------------------------------------------------
DATALOADER:0 TEST RESULTS
{'test_accuracy': tensor(0.6840, device='cuda:0'),
 'train_accuracy': tensor(0.5516, device='cuda:0'),
 'train_loss': tensor(1.5615, device='cuda:0'),
 'valid_accuracy': tensor(0.4787, device='cuda:0'),
 'valid_loss': tensor(0.8586, device='cuda:0')}
--------------------------------------------------------------------------------

test set の精度が 0.68。やはり10,000 件のときより精度が下がった。機械学習においてデータ量は大切。

※ 実装したプログラム全体は Gist に置いた。

所感

  • 今後ますます性能の高い手法が発表されるのだろうが、こういった透過的なインターフェースをもつフレームワークに最新手法が搭載されていくのはよいことである。既存手法との比較とかやりやすそう。
  • それにしても Python を中心とした機械学習まわりのエコシステムがツラい。書きやすくもないし保守しやすくもない。強いて言うなら一人でフルスクラッチで書くなら分かる。多様なライブラリやフレームワークを使うことが前提なのに Python が主流になってる世の中がツラい。

Docker コンテナの OS を確認する方法

いきなりまとめ

ホストマシン上で次のコマンドを実行して出力されるメッセージを見る。

$ docker run --rm (調べたいDockerイメージ) sh -c "cat /etc/*-release"

背景

Dockerfile を書くときに RUNCMD コマンドで叩ける命令はベースとしている OS イメージに依存する。しかし、何の OS をベースとしているのかパッと見ただけでは分からない。 Dockerhub とかみれば分かることも多いが。

自分で調べる素朴な方法として、Dockerfile の FROM に指定されているベースイメージをたどっていき、OS のイメージ(debian とか alpine とか)に到達するまで繰り返すやり方がある。これは面倒くさいのでやりたくない。

次のアイデアといえば、調べたいコンテナを起動して中に入って OS の情報を得るやり方である。ただし、シェルを起動するコマンドが OS に依存する問題がある。Alpine Linux では bash が使えないので docker run -it (コンテナイメージ) bash とか叩くと Error: Cannot find module '/bash' とかエラーが出る。もう少しスマートにやりたい。

コンテナの OS の調べ方

だいたいの Linux OS では /etc/os-release というファイルに OS の情報が載っている。コンテナ内にあるこのファイルを覗きたい。ただし、centos では代わりに /etc/redhat-release を見るべきらしい。

そして、Dockerfile のベースイメージが FROM scratch でもない限りは sh コマンドは叩けるだろう。ってことで以下のコマンドをホストマシンで叩けばよい。

$ docker run --rm (調べたいDockerイメージ) sh -c "cat /etc/*-release"

ここで --rm オプションは、コンテナの実行が終了したときに、そのコンテナを削除するために指定している。

実行の例

上記のコマンドをいくつかの Docker イメージに対して実行して OS を調べてみる。

node:15

Docker の node:15 イメージで使われる OS を調べてみよう。

$ docker run --rm node:15 sh -c "cat /etc/*-release"
PRETTY_NAME="Debian GNU/Linux 9 (stretch)"
NAME="Debian GNU/Linux"
VERSION_ID="9"
VERSION="9 (stretch)"
VERSION_CODENAME=stretch
ID=debian
HOME_URL="https://www.debian.org/"
SUPPORT_URL="https://www.debian.org/support"
BUG_REPORT_URL="https://bugs.debian.org/"

ふむふむ。Debian らしい。

node:alpine3.13

$ docker run --rm node:alpine3.13 sh -c "cat /etc/*-release"
3.13.2
NAME="Alpine Linux"
ID=alpine
VERSION_ID=3.13.2
PRETTY_NAME="Alpine Linux v3.13"
HOME_URL="https://alpinelinux.org/"
BUG_REPORT_URL="https://bugs.alpinelinux.org/"

名前の通りもちろん Alpine Linux。シェルを起動したいときは ash を使おう。

golang:1.14

$ docker run --rm golang:1.14 sh -c "cat /etc/*-release"
PRETTY_NAME="Debian GNU/Linux 10 (buster)"
NAME="Debian GNU/Linux"
VERSION_ID="10"
VERSION="10 (buster)"
VERSION_CODENAME=buster
ID=debian
HOME_URL="https://www.debian.org/"
SUPPORT_URL="https://www.debian.org/support"
BUG_REPORT_URL="https://bugs.debian.org/"

これも Debian

mongo:latest

$ docker run --rm mongo sh -c "cat /etc/*-release"
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=18.04
DISTRIB_CODENAME=bionic
DISTRIB_DESCRIPTION="Ubuntu 18.04.5 LTS"
NAME="Ubuntu"
VERSION="18.04.5 LTS (Bionic Beaver)"
ID=ubuntu
ID_LIKE=debian
PRETTY_NAME="Ubuntu 18.04.5 LTS"
VERSION_ID="18.04"
HOME_URL="https://www.ubuntu.com/"
SUPPORT_URL="https://help.ubuntu.com/"
BUG_REPORT_URL="https://bugs.launchpad.net/ubuntu/"
PRIVACY_POLICY_URL="https://www.ubuntu.com/legal/terms-and-policies/privacy-policy"
VERSION_CODENAME=bionic
UBUNTU_CODENAME=bionic

これは Ubuntu

hello-world:latest

$ docker run --rm hello-world sh -c "cat /etc/*-release"
docker: Error response from daemon: OCI runtime create failed: container_linux.go:367: 
starting container process caused: exec: "sh": executable file not found in $PATH: unknown.

sh コマンドが見つからないってエラーメッセージが出る。これは FROM scratch している Docker イメージだと思えばよさそう。Dockerfile の FROM にこのイメージを指定しても RUN とか CMD で何のコマンドも叩けない。

参考

python - determine OS distribution of a docker image - Stack Overflow

os-release

Docker ネットワークで遊ぶ

ソフトウェアエンジニアって物理現象を相手にするの嫌いですよね(偏見)。LAN ケーブル買ってきて断線とかしてたら最悪。ってことで今日は Docker network で仮想的なネットワークを作って遊んでみる。秋葉原で何も買ってこなくてよいので楽チン。

Docker network の機能を使うと、起動した Docker コンテナが他のコンテナと通信できたりする。もちろん外部との通信もできる。今回は Docker network のうち host ネットワークと bridge ネットワークを使って遊んでみたメモ。ホストマシンは ubuntu 20.04。

簡単なサンプルサーバーを作る

Docker を起動する準備として、まずは nodejs の express フレームワークを使ってシンプルな Web アプリを作ってみる。 3150 番ポートにアクセスされると Hello World! と返すだけのサーバアプリである。以下の通りに index.js を実装した。

const express = require('express')
const app = express()
const port = 3150

app.get('/', (req, res) => {
    res.send('Hello World!\n')
})

app.listen(port, () => {
    console.log(`Example app listening at http://localhost:${port}`)
})

この Web アプリの依存関係をインストールするための package.json は以下。

{
  "name": "exp_server",
  "version": "1.0.0",
  "description": "",
  "main": "index.js",
  "scripts": {
    "test": "echo \"Error: no test specified\" && exit 1"
  },
  "author": "",
  "license": "ISC",
  "dependencies": {
    "express": "^4.17.1"
  }
}

index.js と package.json を同じディレクトリに置いて npm install を実行すれば自動的に依存ライブラリがインストールされる。とはいっても、今回はそのインストールを Docker イメージのビルド時にやってしまうため、ただ2つのファイルを手元に作っておけばよい。

今回用いるコンテナイメージを作成するための Dockerfile は以下の通り。

FROM ubuntu:18.04

RUN apt update \
    && apt install -y sudo curl \ 
    && curl -fsSL https://deb.nodesource.com/setup_lts.x | sudo -E bash - \
    && sudo apt-get install -y nodejs

WORKDIR /root
COPY index.js /root
COPY package.json /root

RUN npm install

CMD node index.js

ubuntu:18.04 をベースとして 、nodejs や npm を NodeSource からダウンロードしてきて、コンテナ内にインストールする。Docker Hub の node イメージ を使ってもよいのかもしれないが、ubuntu からコマンド叩くほうが個人的には何やってるか分かりやすいので今回はこの形を採用した。

index.js と package.json を手元に置いて、以下のコマンドを実行することにより exp_ubuntu という名前のコンテナイメージをビルドする。

$ docker build -t exp_ubuntu .

しばらく待ったらコンテナイメージのビルドが完了する。以下のコマンドで確認できる。

$ docker images
REPOSITORY    TAG       IMAGE ID       CREATED              SIZE
exp_ubuntu    latest    c8f01578eecc   About a minute ago   270MB

これで Docker コンテナを起動する準備が完了した。

host ネットワーク

まずは host ネットワークから作ってみる。以下のページを参考にした。

Use host networking | Docker Documentation

host ネットワークは Docker を動かしているホストマシンと同一のネットワークである。host ネットワーク上でコンテナを起動することは、Docker コンテナをホストマシン上の1つのアプリとして実行するような感じになる。

以下のコマンドにより、先ほど作成した Web アプリのコンテナイメージを host ネットワーク上で起動する。server1 というコンテナ名を付けている。--network host というオプションによって、接続するネットワークとして host を指定しているのがポイント。

$ docker run -d --network host --name server1 exp_ubuntu
$ docker container ls
CONTAINER ID   IMAGE        COMMAND                  CREATED         STATUS         PORTS     NAMES
4975bdef4adb   exp_ubuntu   "/bin/sh -c 'node in…"   8 seconds ago   Up 6 seconds             server1

ブラウザから http://localhost:3150/ にアクセスすると Hello World! というメッセージが表示される。3150 番のポートでリクエストを受け付けていることが確認できた。

ちなみに、これはホストマシン上で以下のコマンドを起動したときの挙動と全く変わらない。

$ node index.js

host ネットワーク上のコンテナとして Web アプリを起動する利点は、環境構築をコンテナという隔離されたところでできる点だけでなく、性能の最適化を行うときに便利だったりするらしい。

起動中のコンテナの中身を覗いてみる。lsof コマンドによって 3150 番のポートで LISTEN されていることが確認できる。

$ docker exec -it server1 bash
~# apt install -y lsof
~# lsof -i
COMMAND PID USER   FD   TYPE DEVICE SIZE/OFF NODE NAME
node      7 root   18u  IPv6 706707      0t0  TCP *:3150 (LISTEN)
~# exit

docker network inspect コマンドで host ネットワークの状況を確認できる。

$ docker network inspect host
[
    {
        "Name": "host",
        ...
        "Containers": {
            "4975bdef4adbdf2b520d9b0d35838e46dc9cdc6ab4e31496830ae7625c93e55e": {
                "Name": "server1",
                "EndpointID": "75088badf4fd62ed7edf0f1265a0177214ddcfa9e172f961b9ff143f7f8feb2d",
                "MacAddress": "",
                "IPv4Address": "",
                "IPv6Address": ""
            }
        },
        "Options": {},
        "Labels": {}
    }
]

Web アプリを起動している server1 コンテナがネットワーク上に登録されていることが確認できた。

最後に server1 を停止してコンテナを削除する。

$ docker container stop server1
$ docker container rm server1

bridge ネットワーク

つぎに bridge ネットワーク上でコンテナを起動してみる。bridge ネットワークはもっともオーソドックスな Docker ネットワークであり、同じネットワーク内のコンテナ同士の通信を実現する。ホストマシンとは異なるネットワークであるのがポイントである。以下を参考にした。

Use bridge networks | Docker Documentation

bridge ネットワーク上で Web アプリを起動してみる。せっかくなので2つのコンテナを起動してみる。それぞれ server1, server2 という名前を付けている。--network bridge というオプションによって bridge ネットワーク上でコンテナを起動することを指定している。ただし bridge ネットワークはデフォルトのネットワークなので、このオプションは無くてもよい。

$ docker run -d --network bridge -p2001:3150 --name server1 exp_ubuntu
$ docker run -d --network bridge -p2002:3150 --name server2 exp_ubuntu

-p2001:3150 というオプションによって、ホストマシン側に公開するポートを指定している。具体的には、ホストマシン側の 2001 番ポートが bridge ネットワーク側の 3150 番ポートに対応する。実際、http://localhost:2001/http://localhost:2002/ にアクセスすると Web アプリにアクセスできる。

bridge ネットワークを inspect してみる。

$ docker network inspect bridge
[
    {
        "Name": "bridge",
        ...
        "Driver": "bridge",
        "EnableIPv6": false,
        "IPAM": {
            "Driver": "default",
            "Options": null,
            "Config": [
                {
                    "Subnet": "172.17.0.0/16"
                }
            ]
        },
        ...
        "Containers": {
            "328253b90470aa98c8419aec36c36610b113e6c2393ce5fd3ff37c261efb366d": {
                "Name": "server1",
                "EndpointID": "0d26a79bd7969059afc12765a4e207887c6ffccfda7d2bdf93162ae3df7e4d76",
                "MacAddress": "02:42:ac:11:00:02",
                "IPv4Address": "172.17.0.2/16",
                "IPv6Address": ""
            },
            "99b67c70283e1f1111430bb2c6c126e967a422522196ed636356b4be2c7e9642": {
                "Name": "server2",
                "EndpointID": "a7167ff0b5562125fb14a07872d4fb96eb9c0ca4a2b017a68892ff1ba864a945",
                "MacAddress": "02:42:ac:11:00:03",
                "IPv4Address": "172.17.0.3/16",
                "IPv6Address": ""
            }
        },
        ...
    }
]

server1server2 はそれぞれ、bridge ネットワーク内の IP アドレス 172.17.0.2172.17.0.3 が割り当てられていることが分かる。

ポートの対応関係は docker ps コマンドで確認できる。PORTS 列にまさにポートの対応関係が示されている。

$ docker ps
CONTAINER ID   IMAGE        COMMAND                  CREATED         STATUS         PORTS                    NAMES
5385113b3b6d   exp_ubuntu   "/bin/sh -c 'node in…"   7 minutes ago   Up 7 minutes   0.0.0.0:2002->3150/tcp   server2
5717a0502c50   exp_ubuntu   "/bin/sh -c 'node in…"   7 minutes ago   Up 7 minutes   0.0.0.0:2001->3150/tcp   server1

ちなみに、ホストマシン上で ip コマンドを叩くと docker0 という仮想ブリッジが存在することが確認できる。ホストマシンと bridge ネットワーク上のコンテナはこのブリッジ経由で通信される。

$ ip a show docker0
3: docker0: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc noqueue state UP group default 
    link/ether 02:42:36:1e:b2:60 brd ff:ff:ff:ff:ff:ff
    inet 172.17.0.1/16 brd 172.17.255.255 scope global docker0
       valid_lft forever preferred_lft forever
    inet6 fe80::42:36ff:fe1e:b260/64 scope link 
       valid_lft forever preferred_lft forever

所感

手軽に Docker コンテナ同士をネットワークで接続できるのでいろいろ実験してみたくなる。自分でネットワーク構成考えてみて、各ネットワークにコンテナを配置する遊びとかできそう。簡易的なロードバランサーとか実装してみたくなった。

風船であそぼう!Rust 入門「所有権」編

この記事では Rust 初心者向けに Rust の基本的な概念を説明します。とはいっても、私自身 The Rust Programming Language の一部を読んで、Rust のコードを 1,000 行ほど書いた程度の理解度です。そのわりに「Rust の世界観を風船で表現しよう!」というヘンな切り口での説明を試みてます。間違ってたらすみません。書きたい衝動を抑えられなかった...。ってことで始めましょう。

なぜか関数が1度しか実行できない...

Rust はヘンな言語です。いろんな言語に触れたことのあるプログラマであっても、Rust を触り始めると知らない概念がたくさん。まさに未知との遭遇です。

手始めに hello というメッセージを2度表示するプログラムをこんな感じに書いてみました。

fn f(t: String) {
    println!("{}", t);
}

fn main() {
    let s = String::from("hello");
    f(s);
    f(s);
}

文字列 s を引数に与えて関数 f を2度実行するだけです。

...しかし、残念ながら以下のようなコンパイルエラーが発生します。

$ rustc main.rs 
error[E0382]: use of moved value: `s`
 --> main.rs:8:7
...

ちなみに関数 f を1度だけ実行するプログラムならコンパイルエラーにはなりません。なにか Rust には他の言語とは違う秘密がありそうです。
本記事では、このプログラムの例を通じて Rust の "所有権" を理解しましょう。

ようこそ風船の世界へ!

Rust の気持ちを理解するため、とある世界を考えてみましょう。

この世界の "住人" は変数です。そして、"風船" が値に対応します。たとえば、以下の代入文では、右辺の String::from("hello") によって得られる値が左辺の変数 s に代入されます。

let s = String::from("hello");

これを以下のように図示することにします。

f:id:t-keita:20210315034410p:plain

住人 "s" が値に対応する風船を持っているだけです。ちなみに風船にはヘリウムガスが入っていて、住人が手を放すと空へ飛んでいってしまいます。本記事では "値" としてスタック領域ではなくヒープ領域に格納されるもののみを扱うものとしています。

変数がスコープに所属するのと同様に、住人は特定の範囲に住んでいます。たとえば、以下のプログラムではスコープ 'a 中に変数 s が存在します。

{// 'a
   let s = String::from("hello"); 
}

これを図示すると以下になります。住人は 'a と書かれた高台に住んでいます。

f:id:t-keita:20210315021124p:plain

そして、プログラムの実行が進むにつれて、この世界では住人が移動します。たとえば以下のプログラムを考えます。プログラムの実行に対応する時刻 t1 と t2 をソースコードコメントとして記載しています。

...
{// 'a
   let s = String::from("hello"); 
   // time = t1
   ...
}
// time = t2

このプログラムの実行を図示すると以下になります。

f:id:t-keita:20210315021041p:plain

左の図が時刻 t1 で、右の図が時刻 t2 に対応します。時刻 t1 では住人が風船をしっかり持っています。しかし、時刻 t2 では住人が高台 'a から落ちてしまいました。住人はあまり丈夫ではありません。悲しいことに住人は息絶え、風船は空の彼方へ消え去ります。これは、変数がスコープの外に出たとき、その変数が参照していたメモリが自動的に解放されることを示しています。

一見すると悲しい世界ですが、実はこの仕組みによって世界は "クリーン" に保たれています。風船にはヘリウムガスが入っているので、住人が息絶えたタイミングで風船は空の彼方に消えてゆくのでした。では、この風船が水風船だったらどうでしょう?住人が息絶えると水風船は地面に落ち、ゴミとしてその場に残り続けます。そしてプログラムの実行が進むつれて世界がゴミだらけになってゆきます。そのためゴミを定期的に掃除したくなるのですが、これはまさに Java などに見られるガーベジコレクションです。

他方、住人の生死問わず不要になったタイミングで水風船を捨てるように管理するとしましょう。これはいわゆるメモリの解放であり C/C++ などの基本戦略です。しかし、不要になったタイミングで水風船を捨てるのを忘れ、メモリリークとして問題化してきたわけです。

このような背景から、Rust では変数が生存区間から出るとき、その変数が参照している値を自動的に解放する仕組みが採用されています。ガーベジコレクションも明示的なメモリの解放も不要なわけです。その結果、Rust は圧倒的な実行性能を保ちつつ、メモリ安全性を担保するといったシステムプログラミングに最適な強みを持つわけです。

所有権とムーブ

住人が息絶えるタイミングで風船も消え去る。こんな世界では代入文がもつ意味すらひと味違います。代入は風船の受け渡しになります。

以下の代入文を考えてみましょう。変数 s の値を変数 t に代入するだけです。

let s = String::from("hello");
let t = s;

これは以下のように図示できます。

f:id:t-keita:20210314125852p:plain

左の図が代入前で、右の図が代入後です。ここで重要なのは、住人 s は風船を手放してしまっていることです。つまり、変数 s はもはや値に関する情報を持っていません。

Rust ではこの状況を「変数 s が持っていた値の 所有権(ownership) が変数 tムーブ(move)された」という言い方をします。この "所有権" と "ムーブ" こそが Rust の重要な概念のひとつです。この世界では、"所有権" は住人が風船を持っていることに相当し、"ムーブ" は風船の受け渡しに相当します。

ここまで来ると、以下のプログラムがコンパイルエラーになるのも納得できるはずです。

let s = String::from("hello");
let t = s;
println!("{}", s); // compile error!

代入(ムーブ)によって住人 s が風船を手放した後に、住人 s がもつ風船を使おうとしている状況を思い浮かべられたらオッケーです。このような状況が発生することは、実際にプログラムを実行するまでもなく Rust コンパイラによって検出されます。

実際、以下のようなコンパイルエラーが発生します。

$ rustc main.rs 
error[E0382]: borrow of moved value: `s`
 --> main.rs:4:20
  |
2 |     let s = String::from("hello");
  |         - move occurs because `s` has type `String`, which does not implement the `Copy` trait
3 |     let t = s;
  |             - value moved here
4 |     println!("{}", s);
  |                    ^ value borrowed here after move

最後のメッセージ "value borrowed here after move" は、ムーブした後に変数を使おうとしてるからダメだよ、と教えてくれています。("borrow" という文言は今は気にしなくて大丈夫です。あとで説明します。)

異なるスコープ間での代入はシンプルです。以下のプログラムでは、内側のスコープに属する変数へ所有権をムーブしています。

{// 'b
   let s = String::from("hello");
   {// 'a
      let t = s;
   }
}

図は以下のような感じでしょうか。

f:id:t-keita:20210316000829p:plain

この世界では変数のスコープには高台が対応するのでした。住人 s が風船を手放すと風船は宙へ浮き上がり、住人 t がキャッチします。これで無事 "上の階" に住む住人に風船をパスできました。

"下の階" に住む住人へ風船をパスすることでもできます。このプログラムを考えてみます。

{// 'b
   let t;
   {// 'a
   let s = String::from("hello");
   t = s;
   }
}

これを図示すると以下になります。

f:id:t-keita:20210314135446p:plain

上の階に住む住人 s が糸を垂らし、それを下の階の住人 t がキャッチします。住人 s が風船から手を放すと風船の受け渡しができます。ちなみに、プログラムの実行時にはスコープ 'a を抜けるタイミングで上の階の住人 sは息絶えます。しかし、風船は下の階の住人 t に引き継がれたので、風船が空へ消えてゆくことはありません。

関数呼び出し

この世界では、関数は文字通り雲の上の存在です。具体的に見ていきましょう。

まずは以下の関数 f を考えてみます。

fn f(t: String) {
    println!("{}", t);
}

これを図示すると以下のようになります。

f:id:t-keita:20210315024145p:plain

関数そのものは雲の上に存在します。関数の仮引数は住人として表現され、実引数となる風船を今か今かと待ち構えています。では実際に、この関数を実行してみましょう。

以下のようなプログラムで関数 f を実行します。

fn f(t: String) {
    println!("{}", t);
}

fn main() {
    let s = String::from("hello");
    f(s);
}

これを図示すると以下になります。

f:id:t-keita:20210315025530p:plain

左の図は関数 f の実行前の状態で住人 s が風船を持っています。真ん中の図は関数 f を実行するために引数として風船の受け渡しを行った様子です。先ほどの ”上の階" に風船を渡すのと同じように、下の住人 s が風船を手放し、それを住人 t がキャッチする流れです。右の図は関数の実行が終了した直後の様子です。プログラム実行にともなって住人は移動するのでした。雲の上に住む住人も例外ではありません。住人 s は息絶え、風船は空の彼方へ消えてゆきます。これが Rust における関数実行の流れです。つまり、引数として与えた値は、関数の仮引数へムーブされたのち、関数の終了時に消え去ります。

なぜ関数が1度しか実行できなかったのか?

ここでようやく冒頭のプログラムの例「なぜか関数が1度しか実行できない...」に戻ってきます。冒頭のプログラムを以下に再掲します。

fn f(t: String) {
    println!("{}", t);
}

fn main() {
    let s = String::from("hello");
    f(s);
    f(s); // compile error!
}

2度目の関数呼び出し f(s); がなぜエラーになるのかもうお分かりですね。この時点で住人 s が風船を持っていないのです。持ってない風船は渡せません。それがコンパイラによって検出されるため、コンパイルエラーとして指摘されるわけです。

では、関数を2度実行するにはどうすればよいでしょうか?一番素朴なやり方は、関数に渡された風船を、関数の実行が終了した後に呼び出し元に返すやり方です。以下はその例です。

fn f(t: String) -> String {
    println!("{}", t);
    return t;
}

fn main() {
    let mut s = String::from("hello");
    s = f(s);
    f(s);
}

さきほどのプログラムからの修正点は2点あります。1つ目は、関数 f の戻り値として引数に受け取った変数をそのまま返すようにした点です。2つ目は、関数 main 内の変数 s をミュータブルに変更し、関数 f の実行結果を変数 s に代入するようにした点です。これで無事関数 f を2度実行できます。

これに対応する図は以下のようになります。

f:id:t-keita:20210315031950p:plain

左の図は関数の引数として風船を受け取った状態です。真ん中の図では、住人 t が雲の上から糸を垂らすことで関数の戻り値を住人 s に返しています。右の図は関数 f の実行後の様子です。住人 t が息絶えるものの、住人 s が風船を持っているため風船が消えることはありません。住人 s が風船を持っているため、この後もう一度関数 f を実行することができるわけです。めでたしめでたし。

...しかしながら、関数を定義するときに、引数を戻り値として返すのはあまりに面倒ですし、プログラムの複雑化を招きます。なにかもっと良い方法がありそうです。そこで登場するのが Rust の重要な概念である "所有権の借用" です。

以降では借用について説明したのち、冒頭の例を借用を使っていい感じに書き直してみます。

所有権の借用(borrowing)

住人と住人の間で風船のやり取りをしてきましたが、関数呼び出しのときは一時的に風船を借りた後に返すという一連の流れが生まれるのでした。この "借りた後に返す" こそが Rust において "所有権の借用(borrowing)" という概念です。借り方は2パターンあります。1つは不変参照(immutable reference)であり、もう1つは可変参照(mutable reference)です。具体的に見ていきましょう。

不変参照(immutable reference)

まずは不変参照から見ていきましょう。

let s = String::from("hello");
let t = &s;

このプログラムでは変数 s&s という形にして変数 t に代入を行っています。これによって、変数 t は変数 s の値を参照することのみ許されます。変数 s の値を更新することは許されていません。このとき値の所有権は変数 t へムーブされません。

ここで、不変参照型の変数に対応する新たな住人を登場させます。以下の図をご覧ください。

f:id:t-keita:20210315034255p:plain

右の住人t が新たな住人です。この住人は風船を見ることだけが許されています。風船を掴むことはできません。この住人は雲の上に載ったときによい仕事をしてくれます。その様子を見てみましょう。

冒頭のプログラムを、不変参照を用いて以下のように書き換えてみます。

fn f(t: &String) {
    println!("{}", t);
}

fn main() {
    let s = String::from("hello");
    f(&s);
    f(&s);
}

元のプログラムからの変更点は、関数 f の引数を不変参照にしただけです。このプログラムを実行すると期待通りに hello というメッセージを2度表示してくれます。プログラムとしてもスッキリしていい感じです。

関数 f の実行時に対応する図は以下の通りです。

f:id:t-keita:20210316005116p:plain

関数 f の呼び出し時、地上にいる住人 s は雲の上に住む住人 t に風船を見せます(左の図)。あくまで見せるだけであって風船を渡すわけではありません。住人 t は風船から値を読み取れるので、それを使って関数の処理を行います(真ん中の図)。そして、関数の実行が終了すると住人 t は雲の上から落ちて息絶えます。しかし、風船は地上の住人 s がずっと持っていたので空の彼方へ消えてゆくことはありません。そのため、住人 s はその後も風船を他の住人に渡したり見せたりすることができます。このように、参照を使うことで引数に所有権をムーブすることなく関数を実行できました。

可変参照(mutable reference)

上記の不変参照の例では関数 f が引数の値を参照できれば十分でした。一方で、引数の値を更新する必要がある場合、不変参照では不十分です。そこで登場するのが可変参照です。

以下に可変参照を用いたプログラムの例を示します。

let mut s = String::from("hello");
let t = &mut s;

この代入文では変数 s の値を &mut s として変数 t に代入しています。その結果、変数 t は変数 s が持つ値を更新することが許されます。もちろん参照することも許されます。ただし所有権はムーブされません。あくまで一時的に更新する権利を貸し出しているだけです。

可変参照型の変数に対応する新たな住人を登場させます。以下の図をご覧ください。

f:id:t-keita:20210316011353p:plain

右の住人 t が新たな住人です。この住人は風船大好きで、風船本体をしっかり抱えて持つのが特徴です。かわいいヤツです。

あまり面白みはないですが、可変参照を用いた関数実行の例を見ておきましょう。

fn f(t: &mut String) {
    t.push('!');
    println!("{}", t);
}

fn main() {
    let mut s = String::from("hello");
    f(&mut s);
    f(&mut s);
}

関数の引数を &mut とすることで可変参照として所有権を借用しています。関数 f では引数の文字列に ! を付加したうえでそれを表示します。そのため、この関数を実行すると hello!hello!! が続けて表示されます。

これに対応する図を書くと、上記の不変参照の図のうち不変参照の住人を可変参照の住人に置き換えたものになります。あえて載せるほとではないのでここでは省略します。

Rust のルール

ここまで、所有権とその借用として不変参照と可変参照を紹介してきました。実は、これらを使うにはいくつかの決まりが存在します。プログラムを書くときはその決まりを満たすように書かなければなりません。さもなければ Rust コンパイラによってエラーとして指摘されてしまいます。しかしご心配なく。対応する風船の世界を考えることで、それらのルールに従っているかどうか直感的にイメージできます。すでに道具は揃っているのです。

所有権(ownership)のルール

まず、所有権について以下の決まりがあります。Rust プログラマは常にこれを意識してプログラムを書く必要があります。

所有権規則

(規則1) Rustの各値は、所有者と呼ばれる変数と対応している。

(規則2) いかなる時も所有者は一つである。

(規則3) 所有者がスコープから外れたら、値は破棄される。

所有権とは? - The Rust Programming Language 日本語版 から一部改変)

(規則1)は、すべての風船は住人によって持たれていることに対応します。住人に持たれていない風船は空の彼方に消えてゆくのでした。

(規則2)は、風船の所有者は常に1人であることに対応します。風船のヒモは1本しかないので、複数の住人で風船を持つことはできません。

(規則3)は、住人が足場から落ちたとき、息絶えて風船が空の彼方に消えてゆくことに対応します。

いかがでしょうか。すべて風船の世界では当たり前に思えるのではないのでしょうか。

参照(reference)のルール

次に参照を扱う上での決まりを見てゆきます。これはちょっとややこしいです。

参照の規則

(規則4) 任意のタイミングで、一つの可変参照か不変な参照いくつでものどちらかを行える。

(規則5) 参照は常に有効でなければならない。

参照と借用 - The Rust Programming Language 日本語版から一部改変)

(規則4)について、許されるパターンを以下の図を用いて説明します。

f:id:t-keita:20210316015848p:plain

左の図は、風船1つにつき、可変参照の住人が1人でも存在するときは他の可変参照や不変参照が許されないことを示しています。可変参照の住人は風船を抱え込んで隠してしまうので、他の住人が参照を行うことは許されません。右の図は風船1つに対して複数の不変参照の住人が存在できることを示しています。不変参照の住人は風船を見るだけです。みんなで仲良く風船を見ることができます。

(規則4) を破るようなケースを見ることでより理解が深まるかもしれません。以下のコードは(規則4)を満たしません。

let mut s = String::from("hello");
let t = &mut s;
let u = &s; // compile error!
println!("{}", t);

これを図に書くと以下のようになります。

f:id:t-keita:20210316020937p:plain

可変参照の住人 t が抱え込んでいる風船を不変参照の住人 u が見ることは許されません。可変参照の住人は独占欲が強く、他の住人に風船を見られることすら嫌うのです。

実際、可変参照と不変参照を同時に作ると危険なケースがあります。たとえば、以下の関数 push_all に同じ変数の可変参照と不変参照を与えたとき、不正なメモリアクセスが発生する可能性があります。

fn push_all(from: &Vec<i32>, to: &mut Vec<i32>) {
    for i in from.iter() {
        to.push(*i);
    }
}

詳しくは このページ を参照ください。

(規則5) 「参照は常に有効でなければならない。」は、参照の住人が存在している間は所有権を持つ住人は生きていなければならないことを示します。当たり前に満たされる話に聞こえるかもしれいないので、以下に満たさない例を示します。このプログラムはコンパイルエラーになります。

fn f() -> &String { // compile error!
    let s = String::from("hello");
    return &s;
}

fn main() {
    let t = f();
    println!("{}", t);
}

関数 f で不変参照 &s を返していますが、その値の所有権を持つ変数 s は関数 f の呼び出し後に消え去ります。そのため、呼び出し元の変数 t は解放済みのメモリを参照してしまうわけです。

対応する図を以下に示します。

f:id:t-keita:20210316023559p:plain

地上の住人 t が雲の上の風船を見ようとしたとき、雲の上の住人 s は息絶えてしまいます。その結果、地上の住人 t は空の彼方へ消えゆく風船を見続けることになってしまいます。あまりにも住人 t が可哀想ですね。

これは、いわゆる ダングリングポインタ を防ぐための規則です。これが Rust コンパイラによって検出されるので、実行時の安全が担保されます。C/C++ のような言語だと、実行時にプログラムが落ちるしかなかったわけです。

ちなみに、関数の戻り値が参照になっていても、この規則を満たすようなケースは存在します。例えば、戻り値がその関数の引数の参照になっているケースや、'static なライフタイムを持つ参照になっているケースです。これについては次回の「ライフタイム」編で書きたいと思います。

いかがでしょうか。いろんな決まりがありましたが、どれも風船の世界を考えることで、何がまずいのか直感的にイメージできたのではないでしょうか?

さいごに

この記事では、風船と住人からなる世界を通して Rust の気持ちを可視化してみました。我ながら(私の理解している範囲においては)よい説明になっていると思います。Rust の学習曲線が険しいということはよく聞くので、とくに初心者の理解の助けになれば幸いです。

この記事の続きとして、近いうちに Rust 入門「ライフタイム」編を書きたいと思います。ただ、たくさんの絵を書くはしんどい...。

A* アルゴリズムいろいろ

かの有名な A* アルゴリズムについてのメモ。
ダイクストラ法と A*, weighted A*, anytime A* について。

ダイクストラ法と A* アルゴリズム

A* アルゴリズムはグラフ上の最短経路を求めるアルゴリズムである。最短経路の素朴なアルゴリズムといえば ダイクストラ法 であるが、A* アルゴリズムダイクストラ法を一般化したものになっている。

最短経路の探索問題では経路の始点 s と終点 t が与えられるものとする。ダイクストラ法と A* アルゴリズムは、どちらも始点 s から探索を開始し "次にどのノード n を調べるか" を決定し、ノード n に到達するのにかかるコストを計算してゆく。ダイクストラ法と A* アルゴリズムの違いは "次にどのノード n を調べるか" の部分にある。ダイクストラ法では、始点 s からノード n までの距離 g(n) が最小となるようなノードを n として採用する。一方で A* アルゴリズムでは、g(n) に加えてノード n から終点 t までの距離の推定値 h(n) を考慮する。

具体的には A* アルゴリズムではノード n の評価値 f(n) を以下のように定義し、それが最小となるノード n を次に調べる。

f(n) = g(n) + h(n)

ここで g(n) は始点 s からノード n までかかるコストという実績値であり、h(n) はノード n から終点 t までかかるコストの推定値である。つまり、ノード n の "よさ" を評価するために「n に到達するのにこれだけかかる」という実績値 g(n) と「n から終点までこれくらいかかりそう」という推定値 h(n) を考慮している。こういう経験的に上手くいきそうなアルゴリズムは一般に「ヒューリスティック」と呼ばれ、A* アルゴリズムの文脈では h(n)ヒューリスティック関数と呼ばれる。なお h(n)=0 とした A* アルゴリズムダイクストラ法に一致する。

推定値 h(n) は、理想的にはノード n から終点 t までの最短距離にしたいのだが、それは最短経路を求めたい今の状況において知ることはできない。よって、ノード n から終点 t までの最短経路の近似になっているようなヒューリスティック関数 h(n) を設計してやる必要がある。本記事では、 h(n) としてノード n から終点 t までの マンハッタン距離 を採用することにする。終点 t までのマンハッタン距離が小さいのであれば終点 t までの最短経路も小さいだろう、というアイデアである。他の h(n) も考えられるが、ちゃんと最短経路を見つけるためには consistent と admissible という性質を満たすものが望ましいらしい。マンハッタン距離はこれを満たしているので求まる経路は常に最適解である。このあたりに関して軽く調べたので別の記事でまとめたい。

Weighted A*

A* アルゴリズムの派生系として重み付き A* アルゴリズム(weighted A*)が存在する。基本的なアルゴリズムの構造は A* と同様だが評価値 f(n) だけが異なる。具体的には以下のように f(n) が定義される。

f(n) = g(n) + \epsilon \times h(n)

A* アルゴリズムとの違いは \epsilon の有無だけである。ここで \epsilonヒューリスティック関数 h(n) に対する重みであり、\epsilon = 1 のとき A* に一致するし、\epsilon = 0 のときダイクストラ法に一致する。\epsilon \leq 1 のときは厳密な最短経路(つまり最適解)が求まるが、\epsilon > 1 のときは最適解が求まるとは限らない。ただし、最短経路の \epsilon 倍以内の近似解が求まることが知られているうえ、アルゴリズムの実行に要する時間は短いので有効な場合がある。このあたりについても別の記事で書きたい。

Weighted A* を実装してみた

Wikipediaの A* アルゴリズム のページを参考に Kotlin を用いて Weighted A* を実装してみた。

f(n) を考慮しながら探索を繰り返す部分を以下に示す。

fun weightedAsterCost(weight: Double): Map<P, Int>? {
    // h: heuristic function with weight
    val h = { n: P -> weight * n.distance(grid.goal) }

    val costs = mutableMapOf<P, Int>()
         .apply { this[grid.start] = 0 }
    val queue = PriorityQueue<PC>()
         .apply { add(PC(grid.start, h(grid.start))) }
    while (queue.isNotEmpty()) {
        val p = queue.poll().point
        if (p == grid.goal) return costs
        grid.neighbors(p).forEach { n ->
            val cost = costs[p]!! + p.distance(n) 
            if (costs[n] == null || cost < costs[n]!!) {
                costs[n] = cost
                queue.add(PC(n, cost + h(n)))  // f(n) = g(n) + h(n)
            }
        }
    }
    return null // the goal is unreachable
}

ここだけ切り取っても分かりづらいが、コード全体は Github 上にある

Weighted A* を実行してみた

引数の重み \epsilon を変えながら実行してみた。

実行結果を示す前に、今回の探索対象のグラフを以下に示す。濃いマスが壁であり通ることができない。

f:id:t-keita:20210308012431p:plain

左上 (0,0) が始点 s で、右下 (13, 19) が終点 t である。この間を結ぶ最短経路を求めてみる。

\epsilon = 0 の場合

まずは \epsilon = 0 としたとき、つまりダイクストラ法の実行結果を以下に示す。

f:id:t-keita:20210308023109p:plain

左の図が実際に求まった経路。もちろん始点 s から終点 t までの最短経路になっている。右の図はその過程で始点 s からの距離を求める必要があったノードを図示したものである。色の濃いノードほど始点 s からの距離が大きいことを示す。ほとんどすべてのノードを調べる必要があることが分かる。

\epsilon = 1 の場合

つぎは \epsilon = 1、つまり A* アルゴリズムの実行結果を以下に示す。

f:id:t-keita:20210308023538p:plain

左の図により最短経路が求まっていることが分かる。マンハッタン距離がよい性質をもつヒューリスティック関数 h(n) であるため、任意のグラフにおいて最短経路を求めることができる。一方で右の図より、\epsilon = 0 のときより少ないノードのみを調べていることが分かる。つまり、A* アルゴリズムではヒューリスティック関数によって「最短経路がこのノードを含むことはない」という事実が検出され、結果として調べるノードの範囲が小さくなっている。精度を落とすことなく無駄な探索は減らせるという実に上手いアルゴリズムである。

\epsilon = 2 の場合

重みが1より大きい \epsilon = 2 の場合の実行結果を以下に示す。

f:id:t-keita:20210308024316p:plain

左の図より、最短でない経路が求まってしまったことが分かる。これは重み \epsilon が大きすぎるため、終点 t に向けてまっすぐ進む力が強すぎて、最短経路を見落としてしまった状況である。ただし、求まった経路の長さが最短経路の2倍以内に収まっていることは保証されている。右の図からは \epsilon = 1 の場合よりさらに少ないノードを探索していることが(ちゃんと色のついたノードを数えれば)分かる。よって高速に動作することが期待できる。

Anytime A*

ここまでの話を聞くと「 A* では \epsilon = 1 にするのが無難で 、\epsilon > 1 は使いどころがないのでは?」と思ったに違いない。しかし、現実の問題ではグラフが巨大で最適解を出すことが難しい場合も多い。そんなときは、最適でないにせよそこそこの精度をもつ解を求めることが望ましい。

もっというと、なるべく最適解に近い解が欲しいが、途中で打ち切られたときであってもそれまでのベストの解を返すようなアルゴリズムが有用である場合がある。このようなアルゴリズムは anytime algorithm と呼ばれる。anytime な A* はそのまま anytime A* と呼ばれる。

Anytime A* - Wikipedia

anytime A* の実現方法として、weighted A* の \epsilon の値を大きなものからスタートし、徐々に \epsilon を小さくしながら1に近づけてゆく方法がある。\epsilon の大きな方が探索にかかる時間は小さいので、最適でないにせよとりあえず経路は求まる。その後、異なる \epsilon の値によってより短い経路が見つかれば、その時点での最短経路が更新される。この繰り返しの過程において、一度計算したコストを再利用するなどの手法が存在するらしい。

所感

参考文献

https://papers.nips.cc/paper/2003/file/ee8fe9093fbbb687bef15a38facc44d2-Paper.pdf

【Z3ソルバー】関数の define と declare

Z3 ソルバーについてのメモ。
主なトピックは SMT-LIB の definedeclare について。

Z3 と SMT-LIB

Z3 は言わずと知れた SMT ソルバーである。オープンソースであり、Github のページにインストール手順も載っている。この手順の通りにやれば(少なくとも Ubuntu 上では)簡単にインストールできる。ソルバーに与えられる命令列の形式として SMT-LIB がサポートされているため、ユーザは解きたい論理式を SMT-LIB の形式で Z3 に与えればよい。また、各種プログラミング言語から Z3 ソルバーへアクセスするためのインターフェースも充実しており、アルゴリズムの一部として SMT ソルバーを使用したいときは Z3 は使い勝手がよい。詳しくは Github のページを参照。

SMT-LIB 上での関数定義

define-fun(独自の関数を定義)

SMT-LIB では define-fun 命令を用いて関数を定義できる。
試しに2つの引数のうち最大値を返す max 関数を以下のように定義してみる

(define-fun max ((x Int) (y Int)) Int 
    (ite (>= x y) x y)
)

(assert (= (max 1 3) 3))

(check-sat)

ここで ite は if-then-else であり、assert によって  \text{ max }(1, 3) = 3 であることを表明している。そして、(check-sat) によって assert された制約式が真になりうるか検証する。

もちろんこの制約は真なので、これを Z3 に与えたときの結果は以下のように sat(充足可能)と判定される。

$ z3 f1.smt2 
sat

こんな感じで独自の関数を define-fun によって定義できる。
ちなみに ite>= などの演算子が使用可能なのはこれらが Core theory に含まれるからである。Core Theory は任意の Theory において暗黙的にインポートされる。詳しくは SMT-LIB の言語仕様 の 3.7.1 章を参照。

declare-fun(未知の関数を定義)

declare-fun では未知の関数を定義できる。
つまり、Z3 に「こんな制約を満たす関数は存在するか?」という問い合わせができる。
たとえば、具体的な定義が不明な max 関数を declare-fun を用いて定義してみる。

(declare-fun max (Int Int) Int)

(assert (= (max 0 1) 1))
(assert (= (max 4 2) 4))

(check-sat)
(get-model)

この実行結果は以下のようになる。

$ z3 f2.smt2 
sat
(
  (define-fun max ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 4) (= x!1 2)) 4
      1))
)

充足可能であることが sat として表示された後、具体的に得られた max 関数が (get-model) 命令により define-fun として表示されている。この関数は「第一引数が 4 で第二引数が 2 のときは 4 を返すけど、それ以外のときは 1 を返す」ものである。最大値を一般的に求める関数は得られなかったが、一応 assert を満たす関数は構成できた。

余談。これは一種のプログラム合成、とくに入出力例からプログラムを合成する inductive synthesis の問題を解いたことになる。ただし、その解は「2引数を最大値を返す」ような一般性のあるものではなく、assert によって与えられた入出力例に overfit したものである。こういう解を出すのではプログラム合成としてはつまらない。もっと一般性の高い解を見つけられるソルバーを開発したい。そういうモチベーションを持っているのが SyGuS というコミュニティである。

t-keita.hatenadiary.jp

define-fun と declare-fun の関係

SMT-LIB の言語仕様を見ると以下のような話がある。

(define-fun f ((x1 σ1) · · · (xn σn)) σ t)
with n ≥ 0 and t not containing f is semantically equivalent to the command sequence
(declare-fun f (σ1 · · · σn) σ)
(assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t))

つまり、

  • (define-fun f ((x1 σ1) · · · (xn σn)) σ t)

という命令は、以下の2つの命令列と意味的に等しい。

  • (declare-fun f (σ1 · · · σn) σ)
  • (assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t))

具体的を考えてみる。さきほど挙げた max 関数の例では

(define-fun max ((x Int) (y Int)) Int 
    (ite (>= x y) x y)
)

(declare-fun max (Int Int) Int)
(assert (forall ((x Int) (y Int)) (= (max x y) (ite (>= x y) x y))

が意味的に等しいということ。

以上、当たり前みたいな話でした。

「宿題を家に忘れました」で入門する統計的仮説検定

はじめに

この記事では 宿題を家に忘れました を題材にして、統計的仮説検定について解説します。本記事の説明には以下の特長があります。

  • 仮説検定の考え方や手順を初心者にもわかりやすく説明します。
  • 仮説検定の説明にありがちな、確率分布を考慮した具体的な計算は登場しません。

仮説検定に関していろいろ勉強してみたが、計算を理解するのに必死で、仮説検定の本質が何なのかイマイチ分かってない人にオススメです。

「宿題やったんですけど家に忘れてきました」

あなたは学校の先生です。いつものように生徒に宿題を課しました。
そして宿題の提出日、ある生徒Aが白々しくこう言うわけです。

生徒A「宿題やったんですけど家に忘れてきました」

あなたは直感的にこう考えます。

仮説 H_1: 生徒Aはそもそも宿題をやってない
(※ 示したい主張を仮説 H_1 と名付けています。)

主張  H_1 の正しさをなんとか示したいですね。
そこで、あえて主張の否定形 H_0 について考えてみます。背理法みたいな感じです。

仮説 H_0: 生徒Aは本当に宿題をやっている

ここで「生徒Aが宿題をやったのにそれを家に忘れてくる確率は 3% である」ことが知られているとしましょう。生徒Aが本当に「宿題をやった」という状況が100回あったとき、3回くらいは家に忘れるが、97回くらいは学校に持ってくる、ということです。 (この数値 3 %という数値は深く考えずに認めましょう。本来の統計的仮説検定では、この確率が確率分布やそのパラメータに基づいて計算されます。)

つまり、以下のことが言えるわけです。

仮説 H_0 が正しいとすると、3%の確率でしか起こらないことがいま起こっている

いまは「家に忘れる」というかなり珍しい状況が起こったので、以下のように考えるわけです。

仮説 H_0 を受け入れるのは厳しい。やはり仮説 H_1 が正しいだろう。

これで「仮説 H_1: 生徒Aはそもそも宿題をやってないに違いない」の妥当性が高いことを示せたわけです。

どうでしょうか?「宿題を家に忘れました」と言われたとき、普通に考える思考プロセスではなかったでしょうか? これこそが仮説検定の流れです。

仮説検定とは

上記の例を一般的な仮説検定の用語に当てはめていきましょう。
まずは、「仮説 H_1: 生徒Aはそもそも宿題をやってない」のような示したい主張を対立仮説と言います。それに対し、その否定形である「仮説 H_0: 生徒Aは本当に宿題をやっている」を帰無仮説と言います。

仮説検定のプロセスでは、帰無仮説を正しいと仮定したときに現在起こった状況が起こる珍しさを計算します。この珍しさを確率で表現したものが p値 です。上記の例では、「宿題をやった」と仮定したうえで、「宿題を学校に持ってきていない」が起こっている状況であり、それが起こる珍しさ(p値)が 3% であったわけです。

p値が一定の基準より珍しいといえるとき、帰無仮説棄却されて、対立仮説が採択されることで、主張の妥当性が認められます。この「一定の基準」は有意水準と呼ばれ、一般には 5% や 1% が用いられます。実は、上記の例では有意水準として 5% を想定していました。「宿題を家に忘れる」確率が 3% であり、有意水準の 5% より小さいので、この状況が十分に珍しいものであると言えるわけです。一方で、有意水準を 1% とするのがスタンダードな業界であれば、上記の例の 3% は十分に珍しいとは認められません。

ここでひとつ注意したいのが、p値が有意水準を下回らず帰無仮説が棄却されないからといって、帰無仮説が正しいと主張できるわけではないということです。
上記の例を、別の生徒について改めて考えてみましょう。普段から非常に忘れっぽい生徒Bがいたとします。生徒Bの場合は、宿題をやったのにそれを家に忘れてくる確率が 10% であるとします。10回に1回くらいは宿題を家に忘れてくるわけです。このとき、生徒Aのときと同様の仮説検定のプロセスを進めると、帰無仮説「仮説 H_0: 生徒Bは本当に宿題をやっている」は棄却されません。10% という値が有意水準を上回るからです。しかしながら、ここで「生徒Bは本当に宿題をやっている」と積極的に主張してよいことにはなりません。いま起こった状況が十分に珍しいとはとはいえないだけであり「それが高い確率で起こる」とは限りません。いま起こった状況だけでは、帰無仮説を棄却するのに十分な根拠があるとは言えない、と解釈するのが正しい姿勢です。
p値や有意水準の扱いについて、研究者であってもよく誤用が見られることが知られています。統計的有意性と P 値に関する ASA 声明 のような声明が出るほどです。p値や仮説検定の結果からなにを主張してよいのか、そもそも p 値の導出に問題はなかったのか、など正しく扱う必要があります。

2種類の誤り

主張の根拠が確率的な事象に基づいている以上、導く結果が誤っている可能性があります。誤りには2種類あって、第一種過誤と第二種過誤と呼ばれています。

第一種過誤または偽陽性は、帰無仮説が正しいのに棄却してしまうことです。この誤りが発生する確率は有意水準に一致します。
上記の例では「仮説 H_0: 生徒Aは本当に宿題をやっている」が真実なのに、それを棄却してしまうことです。生徒Aからすると「本当に宿題やったのに、先生には宿題やってないと思われて悲しい」という状況です。生徒Aがふてくされてしまうので、先生としては望ましくない判断と言えます。有意水準を 5% としたとき、このような状況は20回に1回くらいは発生してしまいます。 有意水準を 1% にすれば100回に1回くらいにおさえられるので、やさしい先生と思われたければそうするのがよいでしょう。

第二種過誤または偽陰性は、対立仮説が正しいのに帰無仮説を棄却できないことです。
上記の例では「仮説 H_1: 生徒Aはそもそも宿題をやってない」が真実なのに、その対立仮説「仮説 H_0: 生徒Aは本当に宿題をやっている」を棄却できないような状況です。普段から忘れっぽい生徒Bは10回に1回くらいは宿題を家に忘れてくるので、「宿題やったけど忘れた」とさえ言えば、宿題をやっていなくても先生に怒られずに済むわけです。生徒Bからするとラッキーですが、先生からすると適切な指導が出来ていないと言えます。先生としては生徒Bに、宿題と同じ問題をその場で解かせてみるとか、生徒Bの家に電話をかけて昨晩の様子を聞いてみるとか、より帰無仮説を否定する根拠が集まるような検定の設計にすべきでした。(ちなみに帰無仮説が棄却されるまで検定の設定を変えながら頑張るというのは NG です。Data Dredging と呼ばれるイカサマです。)

さいごに

この記事の内容は、確率の計算を排除し、身近な「宿題を家に忘れました」という例を題材に統計的仮説検定の考え方を説明したものです。とくに仮説検定の流れを理解することに重点を置きました。一方で、実際にみなさんの目の前の対象について仮説検定を行うときは、やはり統計や確率に関して十分な理解を持っておくべきだと思います。なかなか難しいですが、正しい理解をもってデータを扱いましょう。

参考: