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.1k
定理証明プラットフォーム lapisla.net
abap34
January 27, 2025
Tweet
Share
More Decks by abap34
See All by abap34
Kaggle 班ができるまで
abap34
1
790
「並列化時代の乱数生成」
abap34
3
1.2k
東工大 traP Kaggle班 機械学習講習会 2024
abap34
2
500
Julia Tokyo #11 トーク: 「Juliaで歩く自動微分」
abap34
2
2.3k
Other Decks in Programming
See All in Programming
External SecretsのさくらProvider初期実装を担当しています
logica0419
0
190
生成AI時代のフルスタック開発
kenn
9
2k
TSConfig Solution Style & subpath imports to switch types on a per-file basis
maminami373
1
160
AI時代のリアーキテクチャ戦略 / Re-architecture Strategy in the AI Era
dachi023
0
180
CRUD から CQRS へ ~ 分離が可能にする柔軟性
tkawae
0
210
Blueskyのプラグインを作ってみた
hakkadaikon
1
140
MLOps Japan 勉強会 #52 - 特徴量を言語を越えて一貫して管理する, 『特徴量ドリブン』な MLOps の実現への試み
taniiicom
2
350
「MCPを使ってる人」が より詳しくなるための解説
yamaguchidesu
0
290
データベースの技術選定を突き詰める ~複数事例から考える最適なデータベースの選び方~
nnaka2992
3
3.9k
SpringBootにおけるオブザーバビリティのなにか
irof
1
850
CursorとDevinが仲間!?AI駆動で新規プロダクト開発に挑んだ3ヶ月を振り返る / A Story of New Product Development with Cursor and Devin
rkaga
5
1.8k
AIにコードを生成するコードを作らせて、再現性を担保しよう! / Let AI generate code to ensure reproducibility
yamachu
7
5.7k
Featured
See All Featured
Producing Creativity
orderedlist
PRO
345
40k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
233
17k
Building Flexible Design Systems
yeseniaperezcruz
329
39k
Building a Scalable Design System with Sketch
lauravandoore
462
33k
Cheating the UX When There Is Nothing More to Optimize - PixelPioneers
stephaniewalter
280
13k
Facilitating Awesome Meetings
lara
54
6.4k
How STYLIGHT went responsive
nonsquared
100
5.6k
Docker and Python
trallard
44
3.4k
Embracing the Ebb and Flow
colly
85
4.7k
Speed Design
sergeychernyshev
30
960
Distributed Sagas: A Protocol for Coordinating Microservices
caitiem20
331
21k
jQuery: Nuts, Bolts and Bling
dougneiner
63
7.8k
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! ⭐️