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
830
「並列化時代の乱数生成」
abap34
3
1.3k
東工大 traP Kaggle班 機械学習講習会 2024
abap34
2
560
Julia Tokyo #11 トーク: 「Juliaで歩く自動微分」
abap34
2
2.4k
Other Decks in Programming
See All in Programming
Compose Multiplatform × AI で作る、次世代アプリ開発支援ツールの設計と実装
thagikura
0
140
Vue・React マルチプロダクト開発を支える Vite
andpad
0
110
Navigating Dependency Injection with Metro
zacsweers
3
240
Go言語での実装を通して学ぶLLMファインチューニングの仕組み / fukuokago22-llm-peft
monochromegane
0
120
🔨 小さなビルドシステムを作る
momeemt
4
670
詳解!defer panic recover のしくみ / Understanding defer, panic, and recover
convto
0
230
Kiroで始めるAI-DLC
kaonash
2
580
ソフトウェアテスト徹底指南書の紹介
goyoki
1
150
Ruby×iOSアプリ開発 ~共に歩んだエコシステムの物語~
temoki
0
270
AIコーディングAgentとの向き合い方
eycjur
0
270
HTMLの品質ってなんだっけ? “HTMLクライテリア”の設計と実践
unachang113
4
2.8k
Testing Trophyは叫ばない
toms74209200
0
860
Featured
See All Featured
Exploring the Power of Turbo Streams & Action Cable | RailsConf2023
kevinliebholz
34
6k
JavaScript: Past, Present, and Future - NDC Porto 2020
reverentgeek
51
5.6k
Fireside Chat
paigeccino
39
3.6k
The MySQL Ecosystem @ GitHub 2015
samlambert
251
13k
Testing 201, or: Great Expectations
jmmastey
45
7.7k
Statistics for Hackers
jakevdp
799
220k
Practical Tips for Bootstrapping Information Extraction Pipelines
honnibal
PRO
23
1.4k
Building a Scalable Design System with Sketch
lauravandoore
462
33k
The Success of Rails: Ensuring Growth for the Next 100 Years
eileencodes
46
7.6k
Dealing with People You Can't Stand - Big Design 2015
cassininazir
367
27k
Building Applications with DynamoDB
mza
96
6.6k
Build The Right Thing And Hit Your Dates
maggiecrowley
37
2.9k
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! ⭐️