Sign in

Masaki Waga

@mastodon.maswag.net
13 followers 3 following 146 posts

🌉 bridged from mastodon.maswag.net/@maswag on the fediverse by fed.brid.gy

PostsRepliesMedia
Masaki Waga @mastodon.maswag.net · 22/09/2026
こういうのを共同で書きました kensakayori.github.io/blog/posts/20…
1126
Masaki Waga @mastodon.maswag.net · 16/09/2026
Mastodon v4.7.2 🎉
000
Masaki Waga @mastodon.maswag.net · 13/09/2026
Mastodon v4.7.1 :tada:
000
Masaki Waga @mastodon.maswag.net · 13/09/2026
ゴルバド、バクーとかのあるアゼルバイジャンのアブシェロン半島の南のカスピ海上に半島を作ってそこにあることにしたみたいで、何かすごい (というか視聴同時tootをするのがとても久しぶりである) #vivant
000
Masaki Waga @mastodon.maswag.net · 05/09/2026
日本円が安すぎて空港近くのibis badgetが一泊2万円以上するのはなかなかバグっている
000
Masaki Waga @mastodon.maswag.net · 01/09/2026
大学のドミトリーなのについてきた朝食がfull breakfastなので満足度が高い
000
Masaki Waga @mastodon.maswag.net · 31/08/2026
liverpoolというかイギリス本質情報: 適当なpubが至るところにある
020
Masaki Waga @mastodon.maswag.net · 30/08/2026
お前のフライトそろそろだからなメールにゲートが書いていないのちょっと止めて欲しい (どの辺りで待機していれば良いのかわからん)
000
Masaki Waga @mastodon.maswag.net · 03/08/2026
京都ではなく東京のSota Satoと論文を書きました (大混乱案件
010
Masaki Waga @mastodon.maswag.net · 26/07/2026
タイトルを見て(津軽訛りではなく)南部訛りということだと勘違いしてしまった。英語翻訳で南部弁を仲介するはずはないか 「ウマ娘」で英語翻訳の定石「関西弁→南部訛り」を採用するとタマモクロスとタイキシャトルがキャラ被りしてしまう!?【CEDEC2026】 | Gamer share.google/zY48YNX4xs2szLahN
000
Masaki Waga @mastodon.maswag.net · 18/07/2026
local LLMにコードを書かせるの、qwen3.6でqwen codeを使うのが圧倒的正解という感じになっている。流石に安定している
000
Masaki Waga @mastodon.maswag.net · 13/07/2026
Proxy Quick + TermiusでSSHのSOCKS5のトンネリングをiPadでも無料で実現できることがわかった。Termiusが偉い(ので投げ銭するべきかもしれない
100
Masaki Waga @mastodon.maswag.net · 11/07/2026
Lean, プログラムについてfunctional correctnessだけではなくtime complexityの証明もできるし、expected execution timeすら議論できるらしい(quick sortでやってた) icml.cc/virtual/2026/84162
icml.cc
ICML CSLib: Towards a Lean Computer Science Library
110
Masaki Waga @mastodon.maswag.net · 11/07/2026
ほぼ自然言語で証明が書けるLean4のtacticsがあるらしい: github.com/PatrickMassot/verbose-le…
github.com
GitHub - PatrickMassot/verbose-lean4: Natural language tactics to teach mathematics using Lean 4
Natural language tactics to teach mathematics using Lean 4 - PatrickMassot/verbose-lean4
012
Masaki Waga @mastodon.maswag.net · 09/07/2026
copilotが作ったコードをqwenが見て、「AI generatedなクソコード」 (意訳) 呼ばわり しているのちょっと面白い。なおGitHubでcopilotにPRのreviewをさせてそこで提案されるコードは確かに品質が悪いことが多い。
000
Masaki Waga @mastodon.maswag.net · 29/06/2026
opencode + qwen3.6でコードを書いているけど、design choiceに関する質問をすると「you are right」という返答とともにそうではない方針に変更する。何だこいつと思ったけど人間でもこういう人 (質問を否定と受け取る人) いるわ
000
Masaki Waga @mastodon.maswag.net · 25/06/2026
mastodon v4.5.13 🎉
000
Masaki Waga @mastodon.maswag.net · 25/06/2026
湘南会議のコツ、完全に集中力が切れたと思ったら全てを投げ捨ててプールに行くことかもしれない (夕食を遅らせてプールに行った
000
Masaki Waga @mastodon.maswag.net · 20/06/2026
そういえばUSBメモリにISOイメージを焼くの、cpで動くのが面白くて結局これしか使ってないな
000
Masaki Waga @mastodon.maswag.net · 30/05/2026
opencode + qwen3.6に書かせたコードがだいぶ汚くなってきたので、codexにrefactoringさせている。短めのスクリプトを書かせるのだとqwen3.6でも良いんだけど、長くなると厳しい
100
Masaki Waga @mastodon.maswag.net · 22/05/2026
NIPSという会議 (というかworkshop) がある (できる?) らしい: www.edacentrum.de/en/nips
edacentrum.de
Workshop on Novel Designs for RISC-V Cores and Peripheral IPs (NIPS) | edacentrum
000
Masaki Waga @mastodon.maswag.net · 21/05/2026
何かactive automata learningの話を聞き逃してしまった。実は元から把握していたトークだけじゃなくてもう一つあったらしい
100
Masaki Waga @mastodon.maswag.net · 20/05/2026
ThalesがFrama-CのLSPを作ってVSCodeから色々叩けるようにしたらしい github.com/ThalesGroup/frama-c-lsp
github.com
GitHub - ThalesGroup/frama-c-lsp: This repository contains both the server and client software that implement the Language Server Protocol (LSP) for C/ACSL language. The server part is a novel Frama-C plugin called "lsp". The client part is a VsCode extension.
This repository contains both the server and client software that implement the Language Server Protocol (LSP) for C/ACSL language. The server part is a novel Frama-C plugin called "lsp"....
020
Masaki Waga @mastodon.maswag.net · 20/05/2026
まあopeningだし多少遅れても良いかと思ったけど、もしかしたらartifact evaluation chairなので最初からいることが期待されているかもしれない(地下鉄に1本乗り遅れた
010
Masaki Waga @mastodon.maswag.net · 20/05/2026
今週に入ってからcoding agentにLean4の証明を書かせたりしているけど、gpt-5.5/codexはだいぶ良く動く一方でlocal LLMはqwen3.6もglm-4.7-flash (on opencode) もリファクタリングすらできないという結論に至りつつある。人が必要なlemmaみたいな証明の大体のアイディアを自然言語で書いた後でcoding agentがひたすらギャップを埋めつづける時代が来てくれると良いんですが、少なくともlocal LLMではできないので、そういう体制を取るには資金力がある程度必要そう。あとはlocal LLM枠でgemma4とlocalじゃな […]
mastodon.maswag.net
Original post on mastodon.maswag.net
121
Reposted by Masaki Waga
Masaki Hara @qnighy.qnmd.info.ap.brid.gy · 19/05/2026
Q. 形式手法を使えばプログラムの正しさを証明できますか? A. できない。プログラムはたいてい正しくないため。
063
Masaki Waga @mastodon.maswag.net · 18/05/2026
マクロの鬼みたいなC++のembedded DSLが出てきた fcpp.github.io
fcpp.github.io
Home
FieldCalc++, an efficient C++14 implementation of the Field Calculus
010
Masaki Waga @mastodon.maswag.net · 18/05/2026
The week of FM2026 is starting! conf.researchr.org/home/fm-2026
010
Masaki Waga @mastodon.maswag.net · 17/05/2026
査読が終わったので池袋に落語を聞きに行く機運が高まっている
000
Masaki Waga @mastodon.maswag.net · 13/05/2026
昨日作ったスライドがiCloudで同期されなくて何事かと思ったけど、単に容量が溢れただけだった。こんなときに仕事用のマシンに外部からsshで接続しておくと良いんですよ (scpで持ってきた)
100
Masaki Waga @mastodon.maswag.net · 02/05/2026
mastodon v.4.5.8 🎉
000
Masaki Waga @mastodon.maswag.net · 01/05/2026
デュアルsimのうち通信量の制限がきつい方を使ってテザリングしていたことが発覚し、月初から通信制限にかかりそう
000
Masaki Waga @mastodon.maswag.net · 27/04/2026
計算論的学習理論、必要な部分だけつまみ食いした結果取り残しの多い分野の一つである(VC dimension周りとか)
000
Masaki Waga @mastodon.maswag.net · 27/04/2026
RT> この理由でJanを使ってみようとしているけど結局まだ諸々の準備ができておらずインストールしかしてない www.jan.ai
000
Masaki Waga @mastodon.maswag.net · 26/04/2026
RT> JRubyってまだ生きてたのか… JythonのPython 3対応が進んでいないのと同様に、何となく停滞している印象があった
000
Masaki Waga @mastodon.maswag.net · 26/04/2026
これの前夜祭に行こうと思っていたが仕事が終わらなかった…夜とは abc2026.chikara-u.com
abc2026.chikara-u.com
京都湯上がりクラフトビール祭 2026
伏見 力の湯で開催。過去最大25社のブルワリーが集結。竹田駅徒歩5分。
000
Masaki Waga @mastodon.maswag.net · 22/04/2026
悪いニュースと良いニュースとやっぱり悪いニュースがある。 論文締切があったので査読を先送りにしていたら一週間で6本査読を書かないといけない状況になってしまった 元々だいたい読んでいた論文もあったので既に3本査読を書いた まだ3本ある
110
Masaki Waga @mastodon.maswag.net · 20/04/2026
こういうことになると思っていたけど、ちゃんとあった Over 100,000 people and 67+ organizations are standing up to Google's attempt to lock down Android. Join the fight for a truly open mobile ecosystem. keepandroidopen.org @keepandroidopen #KeepAndroidOpen
keepandroidopen.org
Keep Android Open
Your phone is about to stop being yours. In September 2026, Google will block every Android app whose developer hasn't registered with them.
000
Masaki Waga @mastodon.maswag.net · 14/04/2026
今日の一句 LLM LLVM LVM
020
Masaki Waga @mastodon.maswag.net · 11/04/2026
弊ヤバイテックトーキョーは技術書典20で新刊を出すのでぜひ。オンラインでは既に販売を開始したみたいです yabaitech.tokyo/techbookfest20/2026…
yabaitech.tokyo
ヤバイテックトーキョーは技術書典20に出展します(さ15)
こんにちは、ヤバイテックトーキョーです。当サークルは来週から開催される技術書典20に出展します! オンサイト会場での配置は「**さ15** 」となっております。 今回の出展では新刊の yabaitech.tokyo vol.8 を頒布予定です! 今回は3つの記事が寄稿されています。 * 「トポスの内部論理で定理証明支援系を作る : 構成的基礎から非構成的公理まで」 by wasabiz * 「FalCAuN によるブラックボックス検査 ― 形式仕様に対する自動テスト ―」 by MasWag * 「ハードウェアの事情から理解する C++ メモリモデル」 by nullpo_head それでは技術書典でお会いできるのを楽しみにしております!
101
Masaki Waga @mastodon.maswag.net · 03/04/2026
ここ数日rebuttal golfをやっている。単語数を切りつめて内容を足して、さらに単語数を切り詰めるのである
020
Masaki Waga @mastodon.maswag.net · 02/04/2026
どうやら田村ゆかりは50歳らしい、「田村ゆかりさん、じゅうななさい」とか言っていたのが最近だと思っていたのに…
000
Masaki Waga @mastodon.maswag.net · 27/03/2026
そういえば勢いでPRISM formatのためのmajor modeを作った。tree-sitterえらい github.com/MasWag/prism-ts-mode
github.com
GitHub - MasWag/prism-ts-mode: Major mode for PRISM files using Tree-sitter
Major mode for PRISM files using Tree-sitter. Contribute to MasWag/prism-ts-mode development by creating an account on GitHub.
000
Masaki Waga @mastodon.maswag.net · 27/03/2026
無事にQEST+FORMATS'24のtrack chairとしての最後のお仕事であるSTTTのspecial issueも出版された模様 doi.org/10.1007/s10009-026-00853-1
link.springer.com
Introduction to the special issue on timed and stochastic approaches to system evaluation - International Journal on Software Tools for Technology Transfer
This special issue of the International Journal on Software Tools for Technology Transfer presents extended versions of four selected papers from QEST+FORMATS 2024, the first joint edition of the International Conference on Quantitative Evaluation of Systems (QEST) and the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). The joint conference was held in Calgary, Canada, in September 2024. The papers provide a compact snapshot of current directions in quantitative evaluation and timed systems research.
000
Masaki Waga @mastodon.maswag.net · 18/03/2026
CodexがまるでPythonしか書いたことのない人の書くshell scriptみたいなものを書いてきた(実際そう)ので全部書き直した
110
Masaki Waga @mastodon.maswag.net · 18/03/2026
今週はだいぶしっかりcodexを使ったけど、それでもまだ25%残っている (明日の朝がweekly limitの境目) ので相当使えるな
000
Masaki Waga @mastodon.maswag.net · 17/03/2026
完全に忘れてたけど今年もちゃんとやってたのか あかりをつけましょボンバーマン 2026 www.nicovideo.jp/watch/sm46012691?r… #sm46012691 #ニコニコ動画
nicovideo.jp
あかりをつけましょボンバーマン 2026
あかりをつけましょボンバーマン 2026 [エンターテイメント] 春です。もう踊るしかないのでつくりました。 ...
000
Masaki Waga @mastodon.maswag.net · 17/03/2026
何年か前から業績リストをこれのXMLで管理しているけど、もはやエントリーの追加はLLMでできる時代になってしまった。plain textの業績情報を適当にcodexに与えると追加できてしまうのじゃ… github.com/MasWag/XPubLiCon
github.com
GitHub - MasWag/XPubLiCon: An XML-based publication list converter
An XML-based publication list converter. Contribute to MasWag/XPubLiCon development by creating an account on GitHub.
100
Masaki Waga @mastodon.maswag.net · 09/03/2026
GitHubのPRを立てたりしていないので、どうやって何を読んだのかをtrackしようかと思ったけど、レポジトリ中に未読・既読のファイルをまとめておく org-mode のファイルを置いておくと良いことに気がついた。レポジトリ中にあるのでどの時点のどのファイルに対して LGTM と言ったかまでcommit logでtrackできている
000
Masaki Waga @mastodon.maswag.net · 08/03/2026
それはそうと論文駆動vibeコーディングというのをやってみているけど、コードリーディングが重いフェーズに来ている。うまくいっているともいう
000