冬ハッカソンで定理証明支援系「lapisla-prover」(and more !) を開発しました！

この記事は 1/19 ~ 1/26 に行われた冬ハッカソン2024 10 班「Cat dance at the cafe」の参加記です。

私たちは今回のハッカソンで定理証明支援系「lapisla-prover」とそのほか全てを開発し、技術賞を獲得しました 🥳‌

この記事ではこの lapisla-prover のコンセプトと実装を紹介します。

※ この記事の内容は 2025年 1月 27日現在のものです。

メンバー

カーネルチーム: @zer0-star, @wasabi, @abap34‌‌‌‌
フロントチーム: @Z, @abap34‌‌
‌‌バックエンドチーム: @comavius, @Ponjuice

定理証明支援系とは　🐱

定理証明支援系について知らない方向けに少しだけゆるく定理証明支援系について説明します。定理証明支援系は簡単にいえば「証明の土台を提供して、書かれた証明が正しいことを確認してくれるソフトウェア」のことです。

Theorem thm1 P ∧ Q → P 
  apply ImpR 
  apply AndL1 
  apply I 
qed

これは、lapisla による P ∧ Q → P の証明の記述です。
これをゆるい日本語風に直すと、次のようになります。

P ∧ Q → P という予想に thm1 と言う名前をつけます.
P ∧ Q という前提から P が結論づけられれば OK.
P ∧ Q という前提が使えるなら、P という前提を使って OK.
P という前提から P といえる！
証明完了！

このように、使えるルールのようなものが提供されていて、その上で証明を書きます。これの正しさの保証をすること、そして証明を書くための様々なサポートを提供してくれるのが定理証明支援系です。

‌

このように「証明」を計算機で扱えるかたちにすると、人間には扱いきれない複雑な証明の正しさを機械が検証してくれるのでいろいろな間違いに気がつくことができます。

さらに、(おそらくこれの読者の大部分を占めるであろう) エンジニアの人にとって役立つ使い方としては、プログラムの「正しさ」の検証の道具というものがあります。

例えば、与えられた配列をソートする関数を作るときを考えてみます。

こんな感じの実装を書いてみて、

def sort(arr): 
    if len(arr) == 1: 
      return arr 
    pivot = arr[0] 
    left = [x for x in arr[1:] if x <= pivot] 
    right = [x for x in arr[1:] if x > pivot] 
    return sort(left) + [pivot] + sort(right)

これが正しいことを調べるために色々なケースで確かめます。これをたくさん書けば sort はバッチリでしょう！

check(sort([4, 5, 2, 1, 3]) == [1, 2, 3, 4, 5]) 
check(sort([1, 2, 3, 4, 5]) == [1, 2, 3, 4, 5]) ...

ということはもちろんなく、勘のいい方はお気づきのように、この関数は空配列を与えると配列外参照の実行時例外を投げます。

(そもそも↑のテストの仕方に問題があるという議論はさておき、) テストは信頼性を向上させるための非常に有効なアプローチですが、テスト以外にもソフトウェアの信頼性を高めるためのアプローチはあります！

その一つが定理証明支援系を使うことです。

プログラムのさまざまな性質は定理証明支援系のシステム上で表現することができます。例えばソートするプログラムは、以下のような性質が満たされていて欲しいですが、このような性質は普及している多くの定理証明支援系で表現できます。

出力は入力の並べかえである
出力は昇順になっている

このような事実を証明したアルゴリズムとその実装を使うことで、信頼性が非常に高いソフトウェアを作ることができます。自分のブログの投稿順を sort する関数にこのような検証を行なうのは割に合わないでしょうが、例えばロケットを飛ばすとき、大規模な株取引、OS を作るとき ...「バグったら本当にヤバい」場面では優れた道具になります。

lapisla のモチベーション

では今すぐテストをやめ、全てを証明しろ！と言われても困ると思います。だいいち、世の中は実際にはそのようなことにはなっていません。

その要因は色々あるでしょうが、究極的には次のような事実に起因するのではないかと思います。

証明は大変！

このブログを書いているメンバーであるところの @abap34 も昨年末になって初めて Coq を使い始めたのですが、例にも挙げているソート (アルゴリズムは全然違います) の性質の証明を 1週間粘ってもできませんでした。

そこで自分が感じた難しさは以下のようなものでした。

1. そもそも、定理証明支援系で書く「証明」は結構訓練が必要

飛躍が本当の本当にない証明を書くのは訓練されていないととても難しいです。普段自分がやっている証明(笑) がいかに多くの明示されていない前提に立っているかを思い知らされます。

2. イチからやるのはかなり量が多くて大変

「うーんこれとこれとこれを目標のために示しておきたいな、絶対誰かやってるから調べるか...　▶︎ すみません、ありません。自分で書くか....」ということが頻発します。すると最終的に示したいことにたどり着くまでにたくさんの細かい事実を自前でやる必要があり、大変です。

ところで、これはよく考えたら多くの人が行っているふつうの (?) プログラミングと同じです。

飛躍したことは書けない　　ですし、
イチから作るのはめっちゃ大変　です。

しかし、ふつうのプログラミングはあっちにもこっちにもやっている人がいます。なぜみんなできているのでしょうか？我々は以下のようなことを考えています。

普及しているプログラミング言語は便利なレジストリを備えており、成果を簡単に利用することができる。
コードを共有する文化もあり、色々なところで実装を参考にできる。
それらと比較すると、既存の定理証明支援系はそのエコシステムが貧弱であるのが問題なのではないか？
強力なエコシステムを備えることをコンセプトにした定理証明支援系を作ることで、定理証明支援系が難し過ぎると思われてしまう問題にアプローチできないか？

そこで開発を始めたのが lapisla です。つまり、正確に言えば、作ったものは定理証明支援系ではなく定理証明支援系のカーネル、エディタ、レジストリなどかなり広い範囲のものです。‌

その意味で、成果物は「定理証明プラットフォーム」を名乗っています。

lapisla は次のような特徴を備えています。

1. 全てが Web 上で完結すること。

コードを容易に共有でき、ユーザ同士で多くのサポートができるようになって欲しいです。その実現のための過激な手段として、全てをブラウザ上で完結させています。

カーネルはブラウザ上で動作し、ユーザはワンクリックでコードの Permanent link を作成・共有・閲覧したり、レジストリ (後述) にコードを登録したりすることができます。

一般的な開発と比較して定理証明支援系はローカルで実行することによる利益があまり大きくないことにも着目しています。

2. 便利なレジストリを作り、簡単に他人の成果を import できること。

lapisla はレジストリをホストする機能を備えていて、証明を簡単に登録・利用することができます。登録時にはサーバ上でもVerify を行い、正しい証明のみが登録されます。そのため間違った証明が import されることはありません。

lapisla.net の紹介

それでは機能を紹介します！ lapisla は lapisla.net から利用できます。

Lapisla.net

Lapisla is a user-friendly theorem prover and ecosystem designed for everyone. Greetings! 👋

‌

lapisla.net は、GitHub アカウントでログインできます。‌

ログインすると file を作成可能です。

‌

作成、もしくはファイルを選択すると、エディタ画面に移行します。

最初に例に出した定理を証明してみましょう。ソースコードを貼り付けて、右上にある↓ボタン (または Ctrl/Cmd + ↓) で、証明を 1 step 進めることができます。‌

すると、最初に書いたような日本語に対応する手順で証明が進んでいくことがわかると思います！最後まで証明を進めると "Proven!" と表示されて右下の Environment に示した定理が追加されます。 ‌

そして、サイドバーの保存ボタンを押してから共有ボタンを押すと Permanent Link が作成され、簡単に共有ができます！

さらに、サイドバー最下のボタンを押すと、証明をレジストリに登録することができます。すると、他のユーザも含めこのファイルにある証明を以下のような構文で利用することができます！

import "abap34/example@1"

Theorem ...
   use thm1 {...}

例えばこの証明は別のユーザが書いた定義を使っています！

このようにユーザは全く複雑な操作をすることなく簡単に他のユーザと成果を共有・利用することができます。

How does it work?

ここからは使用している技術などの話をします。

全体について

lapisla の開発面でいちばん面白い点は、カーネルがクライアントサイドでもサーバサイドでも動作している点です。

まず、カーネルは、基本的にはクラインアント側で動作しています。‌‌

カーネルを提供する一番簡単な方法は、全ての操作についてバックエンドサーバにお伺いを立てることでしょうが、ローカルに負けない体験を提供するためには証明を進める/戻すという作業のたびに通信による遅延を発生させることを許容できませんでした。また、そもそもたくさんのユーザからの大量の操作を捌くサーバを用意することは金欠学生には厳しいです。

ところが、先述のように証明をレジストリに登録する際はそれが正しいことを確かめておく必要がありますから、登録時するまさにそのときにはサーバ側で一度実行するのは避けられません。なので結局両方で動くカーネルを書く必要があります。

そのため、今回は

カーネル, フロントエンド, バックエンドを全て TypeScript で書く
カーネルを Internal Package として作って　フロント, バックエンドで利用する

という方針を取りました。

WebAssembly に簡単にコンパイルできる言語を使う案もありましたが、ひとまずハッカソン終了時にはある程度動くものができていて欲しいと考えていて、その時点での成果の最大化を考えると TypeScript に軍配が上がるだろうということで TypeScript で書くことになりました。

振り返ると、これはいい判断だったと思います。開発の立ち上がりの早さもそうですし、比較的苦労せずカーネルと WebUI の連携は進みました。

フロントエンド

Next.js を使っています。ほとんどのページを @Z さんが作ってくれました。

エディタ画面は主に @abap34 が作りました。‌‌エディタのエディタの部分は monaco-editor を利用しています。

きちんと補完も Syntax Error の報告もしてくれます。

‌

バックエンド (+ レジストリ)

ここでのバックエンドはファイルの管理, ログイン周り, レジストリ周りのことです。NestJS を使っています。

バックエンドは @comavius くんと @PonJuice くんが非常に頑張ってくれました。

とくに、今後 GitHub とさまざま連携することを考えて GitHub ログインを実装することになったのですが、これが結構大変そうでした。ところが、最終的に動くものが無事出来上がったのは本当に素晴らしかったです！

カーネル

カーネルは @myuon さんの claire と一人Computer Science Advent Calendar 2017 に非常に強い影響を受けています。

というか、 @abap34 と @zer0-star がたまたまこのアドカレを見つけて、どうもそれなりのことができる定理証明支援系を自分達で作るのはいけるらしいな、となったことによってまともに計画が動き始めたので、影響どころか完全に始祖と言ってもよいです。

さて、カーネルは主に @zer0-star, @wasabi, @abap34 が担当しました。

分担範囲を表現するのが難しかったので主要な PR を挙げます。

zer0-star: パーサのほとんど全て, constant と axiom の実装, その他全てなどを担当してくれました。lapisla-prover の王.

‌

wasabi: 型検査器, カーネルのトップレベルの状態管理などを実装してくれました。型検査の王 (?)

abap34: import の実装, 実際にエディタとやりとりする上で必要な全てを実装しました。monaco の王 (実在)

‌

カーネルの開発は分担も難しかったのですが、ペアプロをしたり相互にデバッグを頑張り、うまくいきました。

とくに最後の方はどちらかというとエディタとの通信のために必要な部分に注力していた @abap34 とずっとコアに手を入れていた @zer0-star で非常にうまく分担できていた気がします。

lapisla の野望

短期的に

次のような機能は作っていく予定です。

タイムライン機能

すでにプロトタイプは稼働しているのですが、(lapisla.net/timeline) このような GitHub Explore のような画面を実装予定です。リロードすると新しい証明がどんどん登録されていく画面が見られたら流石に面白いですね。‌

レジストリに対する賢い検索

検索はまだ未実装なのですが、例えば

単純なコードの検索
タグによる検索

のようなものに加えて、もう少し工夫した高度な検索のアイデアがいくつかあり、それらを実装していきたいと考えています。

パーサ・エディタ支援の強化

パーサはすでにちゃんとエラー報告していたりと比較的ちゃんと書かれているのですが、例えばエラー回復をできるようにしたり、hover で型を出したりなどできるようにしてエディタ支援を強化していきたいと思っています。

カーネル自体の改良

lapisla のカーネル自体はまだまだ出来立てで発展途上です。より簡単にさまざまなことを示せるように改良していきたいです。例えばマクロの定義などが実装されていく予定です。

自動証明

やはり自動で証明を生成する機能はコンセプト(難易度感を下げる) とマッチするのでやっていきたいところです。幸い、アルゴリズムや機械学習に強いメンバーが揃っているので色々やってみようと思っています。

バグ

すいません、直します...

長期的に

次のような野望を持っています。

さまざまなカーネルへの対応

いま、lapisla 全体は lapisla-prover を組み込む前提で作られています。そのため、まだ本格的に証明を広げていくにはカーネルの強化を待つ必要があります。が、それ以外の実用性を高める方向性として、他の普及しているカーネルへの対応は面白いだろうなと思っています。

https://github.com/jscoq/jscoq のようなものであれば現実的にできるような気もするので、長期的にはやってみたいところです。

定理証明の国プルーヴィア

ソースコードの Permanent Link を簡単に発行できるという機能を活かして定理証明の話だけがされる謎の SNS を組み込みたい。

感想

@abap34

lapisla は自分と zer0-star が個人的にやろうとしていたプロジェクトがハッカソンに輸出された形なのですが、誘い込んだ (?) メンバーが本当に頑張ってくれてとても面白いものができて満足しています。

一応自分が全体を把握している人だったのですが、今回のハッカソンはチームがかなり上手く回っていてそれがとても良かったです。

また、Z さんが作業中ずっとグリーンバックの猫ミームの動画を流していて、本当に頭がおかしくなるのではないかと思ったのですが、途中からなんか面白くなってきました。最後に、お気に入りの猫ミームの動画を貼って終わりにします。ありがとうございました。

‌ ‌

@Z

フロントエンドを担当しました‌‌ハッカソンの一週間を振り返っていきたいと思います‌‌

【月曜日】‌‌editのガワが初日してできあがった　今回のハッカソン順調すぎ　余裕やな

‌ ‌

‌‌【火曜日】‌‌ちょっと作業した

‌ ‌

‌‌【水曜日】‌‌ガワ完璧にできた　余裕すぎｗｗｗｗ

‌ ‌

‌‌【木曜日】‌‌ちょっと作業した

‌ ‌

‌‌【金曜日】‌‌決起集会でお酒を飲んだ

‌ ‌

‌‌【土曜日】‌‌滝プラザで集まって開発‌‌昼はピザをパクパク

‌ ‌

‌‌ログインバックエンドができたためエンドポイント繋ぎこみをする

‌ ‌

家に帰っても繋ぎこみ

‌ ‌

‌‌以外と終わらなくて眠くなる‌‌

‌ ‌

‌‌寝落ちしてしまう

‌ ‌

‌‌【日曜日】‌‌朝起きて焦る‌‌

‌ ‌

‌‌なんとか最低限の機能は間に合った‌‌

‌ ‌

‌‌デプロイしてみるとFireFoxでしかログインできない‌‌(現在はFireFox Chrome Edgeで動きます)‌‌

‌ ‌

‌‌技術賞を獲得‌‌

‌ ‌

@wasabi

定理証明支援系という自分の好きな技術を実際に作った，そしてそれがハッカソンで賞をいただいたということで，とても貴重な経験をさせていただきました！自分一人の力だけではこのようなものは到底作ることはできませんでした．チームメイトの皆さん，特に誘っていただいたabap34さんとzer0-starさんには本当に感謝です．ありがとうございました！

定理証明支援系，サイコー！！٩( ᐛ )و

@zer0-star

元から作りたかったものを作っただけではあったのですが、こういう機会でもなければモチベと労力などが足りなくてここまでのものを作ることは難しかったと思うので、ハッカソンという機会を与えてくれたtraPとチームメンバーには本当に感謝しています。

それと、カーネルの設計・実装で大いに参考にさせていただいた定理証明支援系Claireの作者であるmyuonさんも、本当にありがとうございました。

最初から最後（まだ続くけど）までほぼカーネルのみを触っていて、ウェブの部分は全然見てもいない状態でしたが、分業がマジでうまく行っていて（というかabap34がうまく指揮をとっていて）カーネルだけやっていれば勝手に全体の開発が進んでいるという安心感がすごかったです。

というか"定理証明支援系作ったことある側の人"になったのアツ　君らもこっち来なよ

あとお気に入りの猫ミームはpopcatです。

@comavius

@Ponjuiceとバックエンドサーバーを書きました。使用言語以外にこれといった制約もなくかなり広い裁量のもと実装できたので、前々から触ってみたかった技術を使ってみるなど楽しく作業することができました。チームに誘ってくださったabap さん zer0-star さんをはじめチームメンバーには感謝しかありません。

定理証明支援系を初めてまともに触ったのがハッカソン1週間前でカーネルの中身も全く理解できていないのですが、せっかく今回このような機会をいただけたので今後勉強してみたいです。

今回のハッカソンで猫ミームデビューしました。案外面白くて悔しい

@Ponjuice

普段は競技プログラミングが中心で普段何かを作ることは少なく、少々不安要素はありましたがバックエンドを頑張らせていただきました。‌‌普段使わない言語であったこともあり、comaviusくんに頼ったり、手探りでやらせていただいたのですが、ちゃんと動くものができてとても満足しています。‌‌メンバーの皆さん、ありがとうございました！

さいごに

lapisla は今後もオープンソースのソフトウェアとして開発を続けていきます！‌‌

Contribution お待ちしています！

冬ハッカソンで定理証明支援系 「lapisla-prover」(and more !) を開発しました！