Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
定理証明プラットフォーム lapisla.net
Search
abap34
January 27, 2025
Programming
1
2.4k
定理証明プラットフォーム lapisla.net
abap34
January 27, 2025
Tweet
Share
More Decks by abap34
See All by abap34
Kaggle 班ができるまで
abap34
1
840
「並列化時代の乱数生成」
abap34
3
1.3k
東工大 traP Kaggle班 機械学習講習会 2024
abap34
2
590
Julia Tokyo #11 トーク: 「Juliaで歩く自動微分」
abap34
2
2.5k
Other Decks in Programming
See All in Programming
monorepo の Go テストをはやくした〜い!~最小の依存解決への道のり~ / faster-testing-of-monorepos
convto
2
500
Leading Effective Engineering Teams in the AI Era
addyosmani
7
450
Server Side Kotlin Meetup vol.16: 内部動作を理解して ハイパフォーマンスなサーバサイド Kotlin アプリケーションを書こう
ternbusty
3
210
私達はmodernize packageに夢を見るか feat. go/analysis, go/ast / Go Conference 2025
kaorumuta
2
590
bootcamp2025_バックエンド研修_WebAPIサーバ作成.pdf
geniee_inc
0
110
理論と実務のギャップを超える
eycjur
0
140
Introduce Hono CLI
yusukebe
6
2.6k
SwiftDataを使って10万件のデータを読み書きする
akidon0000
0
150
Serena MCPのすすめ
wadakatu
4
1k
技術的負債の正体を知って向き合う
irof
0
180
バッチ処理を「状態の記録」から「事実の記録」へ
panda728
PRO
0
160
uniqueパッケージの内部実装を支えるweak pointerの話
magavel
0
1k
Featured
See All Featured
Cheating the UX When There Is Nothing More to Optimize - PixelPioneers
stephaniewalter
285
14k
GraphQLとの向き合い方2022年版
quramy
49
14k
Facilitating Awesome Meetings
lara
56
6.6k
Why You Should Never Use an ORM
jnunemaker
PRO
59
9.6k
Gamification - CAS2011
davidbonilla
81
5.5k
Design and Strategy: How to Deal with People Who Don’t "Get" Design
morganepeng
132
19k
10 Git Anti Patterns You Should be Aware of
lemiorhan
PRO
657
61k
Exploring the Power of Turbo Streams & Action Cable | RailsConf2023
kevinliebholz
35
6.1k
The Art of Programming - Codeland 2020
erikaheidi
56
14k
Building Applications with DynamoDB
mza
96
6.7k
Thoughts on Productivity
jonyablonski
70
4.9k
YesSQL, Process and Tooling at Scale
rocio
173
14k
Transcript
定理証明プラットフォーム Cat dance at the Cafe. 2025/01/26 lapisla.net
👣 今回のハッカソンでは「定理証明支援系」と そのエコシステムを作りました! 1 💡 既存の定理証明支援系と異なり - Web 上で動作したり -
ほかの人の成果を簡単に import する 仕組みなどを提案しています!
「証明」を書く土台を提供して、 その証明の正しさをチェックしてくれる処理系。 1. 定理証明支援系とは? 2
3 1. 数学の土台として 2. プログラムの正しさの検証の道具として ← 👀
4 なんだろう、嘘つくのやめてもらっていいですか 与えられた配列をソートする関数を作りました! テストもいっぱい書いて全部パスしたしバッチリ! テストを頑張って書いても、 一般に全ての入力を網羅するのは困難ですよね?
5 網羅できてないケースでバグってた... 信頼性が とても 求められる ソフトウェアを作るためのひとつのアプローチ... 定理証明支援系を使って「証明つき」の開発をする 「どんな入力に対しても停止します」 「出力する配列は絶対に昇順です」 などを示したアルゴリズムとその実装が使える!
6 ところが... 証明は難しい!!! 😞 本当に飛躍していない証明を書くのは訓練が必要 😖 前提をちゃんと自分で一から組み立てるのは単純に量が多すぎてとても大変
7 😞 飛躍はダメ 😖 一からやるのは大変 これって...「ふつうの開発」と同じような気もするけど、 「ふううの開発」はそんなに大変じゃない。
8 why? ▶︎ 人の成果を簡単に利用できるから!! import org.apache.hadoop.fs.FileSystem; import numpy as np
import React from 'react'; #include <iostream> import "fmt" require 'kramdown'
目標 成果を簡単に 共有・利用できる 定理証明支援系とそのエコシステムを作る!
成果を簡単に 共有・利用できる 定理証明支援系とそのエコシステムを作る! ▶︎ Demo ▶︎ そのために... 賢いエコシステムを構築する Web 上で全ての開発を行え、
簡単に結果を共有・登録できるようにする!
10 IDE を全て Web上で完結させて、 ワンクリックで共有・Registry に登録できるようにする。 Web 上でもローカルに負けない開発体験を作るために, カーネルはクライアントとサーバ側両方で動作してとても軽快に. エラー報告が優れたパーサを書いてシンタックスエラーの精度を向上.
Web UI を生かしてデバッグのためのいろんな情報を見れるように. 技術的な工夫...
@abap34 カーネル、エディタ @comavius バックエンド @Ponjuice バックエンド @wasabi カーネル @Z フロントエンド
@zer0-star カーネル (B3) (B2) (B2) (D1) (M1) (B3) 11 メンバー @yukikurage 卒論 スペシャルゲスト (B4) ( (
lapisla-prover/lapisla-prover Try & Star me! ⭐️