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
2k
定理証明プラットフォーム lapisla.net
abap34
January 27, 2025
Tweet
Share
More Decks by abap34
See All by abap34
Kaggle 班ができるまで
abap34
1
760
「並列化時代の乱数生成」
abap34
3
1.1k
東工大 traP Kaggle班 機械学習講習会 2024
abap34
2
460
Julia Tokyo #11 トーク: 「Juliaで歩く自動微分」
abap34
2
2.2k
Other Decks in Programming
See All in Programming
自分のために作ったアプリが、グローバルに使われるまで / Indie App Development Lunch LT
pixyzehn
1
140
php-fpm がリクエスト処理する仕組みを追う / Tracing-How-php-fpm-Handles-Requests
shin1x1
5
890
Denoでフロントエンド開発 2025年春版 / Frontend Development with Deno (Spring 2025)
petamoriken
1
1.3k
Kamal 2 – Get Out of the Cloud
aleksandrov
0
140
CRE Meetup!ユーザー信頼性を支えるエンジニアリング実践例の発表資料です
tmnb
0
540
Firebase Dynamic Linksの代替手段を自作する / Create your own Firebase Dynamic Links alternative
kubode
0
200
Devinのメモリ活用の学びを自社サービスにどう組み込むか?
itarutomy
0
1.9k
リアルタイムレイトレーシング + ニューラルレンダリング簡単紹介 / Real-Time Ray Tracing & Neural Rendering: A Quick Introduction (2025)
shocker_0x15
1
250
複雑なフォームと複雑な状態管理にどう向き合うか / #newt_techtalk vol. 15
izumin5210
4
3.7k
AIコーディングワークフローの試行 〜AIエージェント×ワークフローでの自動化を目指して〜
rkaga
2
1.3k
ローコードサービスの進化のためのモノレポ移行
taro28
1
350
PHPのガベージコレクションを深掘りしよう
rinchoku
0
260
Featured
See All Featured
Code Reviewing Like a Champion
maltzj
522
39k
Refactoring Trust on Your Teams (GOTO; Chicago 2020)
rmw
34
2.9k
Side Projects
sachag
452
42k
Practical Orchestrator
shlominoach
186
10k
Design and Strategy: How to Deal with People Who Don’t "Get" Design
morganepeng
129
19k
Making the Leap to Tech Lead
cromwellryan
133
9.2k
[RailsConf 2023] Rails as a piece of cake
palkan
53
5.4k
Why Our Code Smells
bkeepers
PRO
336
57k
Put a Button on it: Removing Barriers to Going Fast.
kastner
60
3.8k
The Myth of the Modular Monolith - Day 2 Keynote - Rails World 2024
eileencodes
22
2.6k
Bash Introduction
62gerente
611
210k
Mobile First: as difficult as doing things right
swwweet
223
9.5k
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! ⭐️