助教@国立情報学研究所 専門: 形式検証•プログラム検証、(応用)圏論
Tokyo
Joined May 2023
- Tweets234
- Following130
- Followers154
- Likes708
Kazuki Watanabe retweeted
From Formal Methods to Fuzzing and Back
Invited paper for my upcoming talk at FSTTCS, on how I started in FM (intellectually mind bending bug would not scale!), moved mainly into fuzzing (so much fun!), and am now getting right back into FM thanks to AI.
doc.ic.ac.uk/~afd/papers/202…
Kazuki Watanabe retweeted
私は数学は終わるのではなく、歴史上再び自分の「外部」を取り入れて、より深く普遍的で、よりインタラクティブな学問に変容する地殻変動が始まったと捉えています。例えば、次の note でそれを論じました。
note.com/katobungen/n/n0655f…
「数学が終わった感が強い」と茂木健一郎。AIの圧倒的進化で直面する数学を取り囲む状況。
news.livedoor.com/article/de…
Kazuki Watanabe retweeted
縁あって凸解析 × モデル検査の研究に関わることができました。個人的に「AI 時代はこうした共同研究を楽しんでいきたい」と感じられる良い経験でした。
とても奥深い問題を分かりやすく教えてくれた @KWatanabeCS 、着想から一つの研究として仕上げるまでリードしてくれた @levelfour_ に感謝です🙏
凸解析 × モデル検査の論文を書きました。まさか形式検証の研究（の端くれ）をするとは思いだにしませんでした。検証の分野にこんなにリッチな凸性があることを教えてくれた @KWatanabeCS と、相変わらずスマートな凸解析のアイデアに貢献してくれた @shinsaku_sakaue との共同研究です。
Kazuki Watanabe retweeted
凸解析 × モデル検査の論文を書きました。まさか形式検証の研究（の端くれ）をするとは思いだにしませんでした。検証の分野にこんなにリッチな凸性があることを教えてくれた @KWatanabeCS と、相変わらずスマートな凸解析のアイデアに貢献してくれた @shinsaku_sakaue との共同研究です。
Convex analysis meets model checking🧐
Probabilistic model checking can be seen as set inclusion test between a safe region and the achievability set to failure states in MDP. Using convex analysis, we propose a computationally efficient query.
arxiv.org/abs/2610.17541
Kazuki Watanabe retweeted
I put Tex2Lean to extract and formalize the algorithm presented in the OpenAI's paper on counting common bases of matroids, and 48 hours, we have a formal pseudocode whose correctness is proven. 1/
Kazuki Watanabe retweeted
自分は少なくともここ数ヶ月、数学の研究にAIを使ってない日は一日たりともないので、AI数学に対する感想でも呟いてみる
（ちなみに数ヶ月以上前は、個人で使えるモデルだと、うちの分野の研究で使うにはまだちょっと性能が微妙だったので，それまでは数学研究にはAIはそんなに使っていませんでした）
Kazuki Watanabe retweeted
I am not surprised;
This is what I warned yesterday: xitter.cf/ksmeel/status/21076397…
I believe Tex2Lean infrastructure can help!
The plot thickens.
"We show that the formalised Lean proof does not correspond to the [written paper] proof of blow-up of solutions to the Navier-Stokes equations."
arxiv.org/abs/2610.08144
Kazuki Watanabe retweeted
I'm hiring a postdoc! Please share broadly with potential candidates.
I'm looking for someone with expertise in PL, FM, and/or networked systems who is excited about contributing to a research and teaching in a growing lab.
careers.epfl.ch/job/Lausanne…
プログラミング言語•理論計算機科学(論理)•形式検証の三分野の紹介も兼ねて、当該分野の研究者らが活躍している主要な国際会議をまとめた記事を公開いたしました(若手研究者の連名)！分野の概観が気軽に掴める良い記事になっていると思いますので、ぜひご一読ください！
kensakayori.github.io/blog/p…
Kazuki Watanabe retweeted
24 Fields Medal winners have written a letter of objection economist.com/science-and-te…
Kazuki Watanabe retweeted
タオ先生も似たようなこと言ってた。
極論、誰かが面白い講演をしているときに、それを聴いた聴衆が、その横でAIを走らせて、講演中により良い結果を得てしまう可能性だってあるわけでしょ。
講演しなくなるよね。論文も発表しなくなるよね。今まで長年かけて考えてきた問題が直前で誰かに盗まれたらたまったもんじゃない。
Still more absolute 🔥 from Terence Tao:
“We have now seen that even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it before the original research project has time to reach its full potential. The incentives may now be pointing in the direction of no longer sharing any promising research directions with the broader community, which would reverse centuries of traditions of open science and do serious long-term damage to the future of the field”
Kazuki Watanabe retweeted
I deleted my previous post. I'm just going to post the entire statement page by page. It's a complicated situation.
Statement: cims.nyu.edu/~tristanb/state…
cims.nyu.edu/~tristanb/euler…
cims.nyu.edu/~tristanb/ipm.p…
cims.nyu.edu/~tristanb/bouss…
github.com/tristanbuckmaster…
Kazuki Watanabe retweeted
As #ICFP2026 wraps up, I've been reflecting on it, and the past two years of work. My first @icfp_conference was 2006 in Portland (GC'ed by John Reppy, who helped bring me into FP), and it's hard to believe that 20 years on, I'm now reporting on the success of our community.
Kazuki Watanabe retweeted
書いた。形式仕様を使ってOSSの分散システム(celld)のバグを実際に見つける話です
zenn.dev/mizchi/articles/qui…
Kazuki Watanabe retweeted
Postmortem for Lean Kernel Soundness Bug #14576
leodemoura.github.io/blog/20…
#lean4 #leanlang #leanprover
