🍣
Leanの定理証明はコード最適化に役立つのか？

2025/05/03に公開
 結論から言うと、「役立つ」
 なぜそう言えるのか？Leanはコード生成の際に「その分岐が発生し得ないことの証明」を示されると、その分岐を削除するからです。

 そもそも何の話をしているのか?
 LeanとはLeanはMicrosoft Researchを中心に開発されているプログラミング言語で、かつ、定理証明支援系です。「依存型型理論」なるものに基づいて数学的命題やその証明を形式的に記述できる点が大きな特徴です。

https://lean-lang.org/

 Leanを使用する目的Leanを使用する目的として例えば次のようなものが考えられます。

 プログラムの正しさの証明Leanはプログラムが特定の仕様を満たすかどうかを記述し、検証することができます。
例えば、ソフトウェアやハードウェアの設計で安全性や信頼性を重視する分野、たとえば制御システムや暗号プロトコルの検証などの用途が考えられます。

 数学的証明の記述Leanは数学的命題とその証明を記述できるため、数学定理の形式化に用いることができます。また、記述された命題の証明が正しいかどうかをコンピューターによって検証できます。
実際に数学ライブラリであるMathlibでは大規模な形式化が行われていて、現在進行中のプロジェクトも多いです。

https://leanprover-community.github.io/mathlib-overview.html
フェルマーの最終定理を形式化しようという取り組みなどもあります。

https://leanprover-community.github.io/blog/posts/FLT-announcement/
他にも自動定理証明など話題が多く、アツい分野です。正直、話がいろいろあってついて行けていない話題も多いです。

 実際にやってみましょうさて、「定理証明がコード最適化に役立つ」という話に戻ります。Leanが証明に基づいて不要なコードを削除するという話でした。
実際にLeanのコードを実行してみて、関連する分岐が削除されるかを見てみます。

 手順まず、Leanをインストールした状態で
% lake new hello_lean exe
と実行すると、空のHello Worldプロジェクトを生成してくれます。
Main.leanがメインの実行ファイルなので、次のように入力していきます。
まずは入力になるリストからです。
def l : List Nat := [1, 2, 3, 4, 5]
次にこのリストのtailを取る関数を作成します。
-- リストのtailを返す関数その1
-- リストが空ではない証明を使って、空リストのチェックを含まないコード
def tl1 (l : List Nat) (hnonempty : ¬ (l = [])) : List Nat :=
  match hl : l with
  | [] => absurd (by rfl) hnonempty
  | _ :: xs => xs
第一引数が入力リストで、第二引数にこのリストが空でないことの証明を受け取ります。分岐の中にabsurdという定義を含んでいます。absurdは「矛盾」を表していて、この処理の分岐が発生しえないことを示します。
ざっくりいうと、この関数の引数が空であるという選択肢はありえない、ということを表明しています。unreachableみたいな？
もう一つ、普通のtail関数を用意して比較します。
-- リストのtailを返す関数その2
-- リストが空の時をチェックして、空のリストを返すチェックを含むコード
def tl2 (l : List Nat) (hnonempty : ¬ (l = [])) : List Nat :=
  match l with
  | [] => []
  | _ :: xs => xs
こちらはインタフェースの互換性のために証明は受け取りますが、中では使用しておらず、リストが空の場合は空リストを返すことで対応します。
最後に、main関数です。まず、リストlが空でないことを証明し、次にtailを取って出力するだけです。
def main : IO UInt32 := do
  -- リストlが空でない事を証明する
  have hl_nonempty : ¬ (l = []) := by
    rw [l]
    exact List.cons_ne_nil 1 [2, 3, 4, 5]
  -- リストのtailを取得する
  let xl : List Nat := tl1 l hl_nonempty
  -- リストを出力する
  for x in xl do
    IO.println s!"num : {x}"
  return 0
準備ができたので、lakeコマンドでビルドして実行します。
% lake exe hello_lean

 実行結果tl1 tl2いずれを採用した場合も期待した通りに出力を返してきます。
num : 2
num : 3
num : 4
num : 5

 比較さて、Leanはこの実行の過程でCコードを吐き、これをコンパイルして実行します。このコードは.lake/build/ir/Main.cに残されています。このコードを見てみます。
まずはtl1のコードです。
LEAN_EXPORT lean_object* l_tl1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; 
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
return x_3;
}
}
ちょっと何をやっているかわからないかも知れませんが、オブジェクト内の二番目にあるポインタを返しているようです。
次に、tl2のコードを見てみます。
LEAN_EXPORT lean_object* l_tl2(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_3; 
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; 
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
return x_4;
}
}
}
こちらは、最初にオブジェクトの種別をチェックしてから、分岐しているようですね。
オブジェクトのタグが空の時(if文が成立したとき)：
新しい空のオブジェクトを生成して返しているようです。

オブジェクトのタグが空でなかったとき(if文が成立しなかった時)：
この処理はtl1と同じようです。


 つまりLeanはabsurdによって到達不可能なパスが示されたとき、そのパスに関する条件チェックを省略することができるようです。最適化の際の前提条件を与え、それが満たされる時のみ、チェックを省略することができるんですね。そして、それはいつ起こるかわからないということではなく、コードを書く側が条件を与えることができるというわけです。

 わざわざ証明を書く必要があるのか？いい質問ですね。結論から言うと「分岐削除の客観的根拠を与えるために重要」ってことです。
不可達コードをマークする方法は通常のプログラミング言語でも存在します。C言語などのコンパイラはユーザーからある分岐が不可達とマークされると、その分岐を削除します。
んー、でもそれなんで正しいのですかね？誰かがマークしたから正しい？それが正しいかどうかはコードをメンテナンスしていく上でどこまで正しいと保証できるのでしょうか？十分なドキュメンテーション？それはいいですね。でも、コード外のコンテキスト理解を必要としますね。
Leanの証明は客観的です。論理的にそのパスに到達しないことを明確に示し、実際に実行パスを削除します[1]。その最適化が正しいかどうかは人間が判断するのではなく、コンパイラが客観的に判断することができます。

 おしまいLeanという言語はさわるだけでもいろいろな発見があります。
興味を持たれたら、ぜひ一緒に学んでみましょう。国内にはlean-jaというコミュニティもあり、お互いに助け合って学んでいます。
lean-jaの情報はこちらにあります。 → https://github.com/lean-ja

脚注
なお、Leanでは証明が書けなくとも、証明を書くべき場所にsorryと記述することで通常のプログラミング言語と同様に根拠なしに分岐を削除することもできます。その場合、Leanでは警告がマークされます。厳密な証明が与えられたものと、そうでないものを明確に区別しています。 ↩︎
結論から言うと、「役立つ」

なぜそう言えるのか？

そもそも何の話をしているのか?

Leanとは

Leanを使用する目的

プログラムの正しさの証明

数学的証明の記述

実際にやってみましょう

手順

実行結果

比較

つまり

わざわざ証明を書く必要があるのか？

おしまい

Discussion
