Lean4で数独

LeanでPyTorchのEagerモードっぽくニューラルネットワークを書けるようにしたTorchLeanというプロジェクトがある。

TorchLean: Formalizing Neural Networks in Lean

 leandojo.org

Leanは、定理証明（形式的証明）とプログラミングを一体化した言語・環境であり、関数型プログラミング言語に近い文法を用いて、証明と実装を同じコードで扱える。

TorchLeanは、LeanでPyTorchのようなコードを書けるフレームワークを提供する。このフレームワークを使ってニューラルネットワークのコードを書くと、実際にそのコードを実行して機械学習を動かせるだけでなく、同時に証明や検証も可能となる、というのがコンセプト。論文によれば、自動微分による逆伝播の検証や、FP32の誤差境界の証明を行った、としている。

このTorchLeanはさておき、Leanがいつのまにか4になっているのを知らなかった。このバージョン4は2021年にリリースされた。LeanはもともとはIsabelleやRocq(旧Coq)¹のような定理証明支援系のソフトだったと記憶しているけど、4から「照明もできる汎用プログラミング言語」となっている。檜山正幸氏のまとめが分かりやすかった。

プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog)

証明支援系Lean〈リーン〉は、かなり前（2017年くらい）から注目しているソフトウェアです。注目はしているんですが、ちゃんと調べる機会がなかったので、このブログで触れたことはありませんでした。2022年のうちに紹介したい（今は大晦日の夜）。Leanは現在、バージョン3系とバージョン4系が混在しています。このため情報が錯綜していて、分かりにくい状況になっています。今はバージョン3系が使われていますが、これからLeanを使い始めるならバージョン4をインストールしてもいいかも知れません（ただし、開発バージョンであることは承知の上で）。Leanは、CoqやIsabelleと同様、証明支援系〈proo…

 m-hiyama.hatenablog.com

というわけで、昔遊んだコードや3から4への更新ガイドとにらめっこしながら、愚直に探索するだけの数独ソルバーをLean4で書いてみた。

sandbox/lean-example at main · disktnk/sandbox

Contribute to disktnk/sandbox development by creating an account on GitHub.

 github.com

探索部分は下の感じで、普通のプログラミングっぽさはある。

partial def solve (b : Board) : Option Board :=
  match findEmpty b with
  | none => some b
  | some (r, c) =>
    let rec tryDigits (ds : List Nat) : Option Board :=
      match ds with
      | [] => none
      | d :: ds' =>
        if isValid b r c d then
          let b' := setCell b r c d
          match solve b' with
          | some sol => some sol
          | none => tryDigits ds'
        else
          tryDigits ds'
    tryDigits ((List.range N).map (· + 1)) -- [1..N]