Masaki Waga
@mastodon.maswag.net
🌉 bridged from https://mastodon.maswag.net/@maswag on the fediverse by https://fed.brid.gy/
こういうのを共同で書きました
https://kensakayori.github.io/blog/posts/2026-09-22.html
https://kensakayori.github.io/blog/posts/2026-09-22.html
September 22, 2026 at 7:16 AM
こういうのを共同で書きました
https://kensakayori.github.io/blog/posts/2026-09-22.html
https://kensakayori.github.io/blog/posts/2026-09-22.html
Mastodon v4.7.1 :tada:
September 13, 2026 at 2:29 PM
Mastodon v4.7.1 :tada:
日本円が安すぎて空港近くのibis badgetが一泊2万円以上するのはなかなかバグっている
September 5, 2026 at 8:31 PM
日本円が安すぎて空港近くのibis badgetが一泊2万円以上するのはなかなかバグっている
大学のドミトリーなのについてきた朝食がfull breakfastなので満足度が高い
September 1, 2026 at 6:53 AM
大学のドミトリーなのについてきた朝食がfull breakfastなので満足度が高い
liverpoolというかイギリス本質情報: 適当なpubが至るところにある
August 31, 2026 at 7:11 PM
liverpoolというかイギリス本質情報: 適当なpubが至るところにある
お前のフライトそろそろだからなメールにゲートが書いていないのちょっと止めて欲しい (どの辺りで待機していれば良いのかわからん)
August 30, 2026 at 1:05 PM
お前のフライトそろそろだからなメールにゲートが書いていないのちょっと止めて欲しい (どの辺りで待機していれば良いのかわからん)
京都ではなく東京のSota Satoと論文を書きました (大混乱案件
August 3, 2026 at 2:40 AM
京都ではなく東京のSota Satoと論文を書きました (大混乱案件
タイトルを見て(津軽訛りではなく)南部訛りということだと勘違いしてしまった。英語翻訳で南部弁を仲介するはずはないか
「ウマ娘」で英語翻訳の定石「関西弁→南部訛り」を採用するとタマモクロスとタイキシャトルがキャラ被りしてしまう！？【CEDEC2026】 | Gamer https://share.google/zY48YNX4xs2szLahN
「ウマ娘」で英語翻訳の定石「関西弁→南部訛り」を採用するとタマモクロスとタイキシャトルがキャラ被りしてしまう！？【CEDEC2026】 | Gamer https://share.google/zY48YNX4xs2szLahN
July 26, 2026 at 7:03 AM
タイトルを見て(津軽訛りではなく)南部訛りということだと勘違いしてしまった。英語翻訳で南部弁を仲介するはずはないか
「ウマ娘」で英語翻訳の定石「関西弁→南部訛り」を採用するとタマモクロスとタイキシャトルがキャラ被りしてしまう！？【CEDEC2026】 | Gamer https://share.google/zY48YNX4xs2szLahN
「ウマ娘」で英語翻訳の定石「関西弁→南部訛り」を採用するとタマモクロスとタイキシャトルがキャラ被りしてしまう！？【CEDEC2026】 | Gamer https://share.google/zY48YNX4xs2szLahN
local LLMにコードを書かせるの、qwen3.6でqwen codeを使うのが圧倒的正解という感じになっている。流石に安定している
July 18, 2026 at 11:12 AM
local LLMにコードを書かせるの、qwen3.6でqwen codeを使うのが圧倒的正解という感じになっている。流石に安定している
Proxy Quick + TermiusでSSHのSOCKS5のトンネリングをiPadでも無料で実現できることがわかった。Termiusが偉い(ので投げ銭するべきかもしれない
July 13, 2026 at 5:52 AM
Proxy Quick + TermiusでSSHのSOCKS5のトンネリングをiPadでも無料で実現できることがわかった。Termiusが偉い(ので投げ銭するべきかもしれない
Lean, プログラムについてfunctional correctnessだけではなくtime complexityの証明もできるし、expected execution timeすら議論できるらしい(quick sortでやってた)
https://icml.cc/virtual/2026/84162
https://icml.cc/virtual/2026/84162
ICML CSLib: Towards a Lean Computer Science Library
icml.cc
July 11, 2026 at 4:54 AM
Lean, プログラムについてfunctional correctnessだけではなくtime complexityの証明もできるし、expected execution timeすら議論できるらしい(quick sortでやってた)
https://icml.cc/virtual/2026/84162
https://icml.cc/virtual/2026/84162
ほぼ自然言語で証明が書けるLean4のtacticsがあるらしい: https://github.com/PatrickMassot/verbose-lean4/tree/master
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
github.com
July 11, 2026 at 12:27 AM
ほぼ自然言語で証明が書けるLean4のtacticsがあるらしい: https://github.com/PatrickMassot/verbose-lean4/tree/master
copilotが作ったコードをqwenが見て、「AI generatedなクソコード」 (意訳) 呼ばわり しているのちょっと面白い。なおGitHubでcopilotにPRのreviewをさせてそこで提案されるコードは確かに品質が悪いことが多い。
July 9, 2026 at 9:30 AM
copilotが作ったコードをqwenが見て、「AI generatedなクソコード」 (意訳) 呼ばわり しているのちょっと面白い。なおGitHubでcopilotにPRのreviewをさせてそこで提案されるコードは確かに品質が悪いことが多い。
opencode + qwen3.6でコードを書いているけど、design choiceに関する質問をすると「you are right」という返答とともにそうではない方針に変更する。何だこいつと思ったけど人間でもこういう人 (質問を否定と受け取る人) いるわ
June 29, 2026 at 8:23 AM
opencode + qwen3.6でコードを書いているけど、design choiceに関する質問をすると「you are right」という返答とともにそうではない方針に変更する。何だこいつと思ったけど人間でもこういう人 (質問を否定と受け取る人) いるわ
湘南会議のコツ、完全に集中力が切れたと思ったら全てを投げ捨ててプールに行くことかもしれない (夕食を遅らせてプールに行った
June 25, 2026 at 9:58 AM
湘南会議のコツ、完全に集中力が切れたと思ったら全てを投げ捨ててプールに行くことかもしれない (夕食を遅らせてプールに行った
そういえばUSBメモリにISOイメージを焼くの、cpで動くのが面白くて結局これしか使ってないな
June 20, 2026 at 9:02 AM
そういえばUSBメモリにISOイメージを焼くの、cpで動くのが面白くて結局これしか使ってないな
opencode + qwen3.6に書かせたコードがだいぶ汚くなってきたので、codexにrefactoringさせている。短めのスクリプトを書かせるのだとqwen3.6でも良いんだけど、長くなると厳しい
May 30, 2026 at 6:53 AM
opencode + qwen3.6に書かせたコードがだいぶ汚くなってきたので、codexにrefactoringさせている。短めのスクリプトを書かせるのだとqwen3.6でも良いんだけど、長くなると厳しい
NIPSという会議 (というかworkshop) がある (できる?) らしい: https://www.edacentrum.de/en/nips
Workshop on Novel Designs for RISC-V Cores and Peripheral IPs (NIPS) | edacentrum
www.edacentrum.de
May 22, 2026 at 4:42 AM
NIPSという会議 (というかworkshop) がある (できる?) らしい: https://www.edacentrum.de/en/nips
何かactive automata learningの話を聞き逃してしまった。実は元から把握していたトークだけじゃなくてもう一つあったらしい
May 21, 2026 at 7:05 AM
何かactive automata learningの話を聞き逃してしまった。実は元から把握していたトークだけじゃなくてもう一つあったらしい
ThalesがFrama-CのLSPを作ってVSCodeから色々叩けるようにしたらしい
https://github.com/ThalesGroup/frama-c-lsp
https://github.com/ThalesGroup/frama-c-lsp
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"....
github.com
May 20, 2026 at 3:19 AM
ThalesがFrama-CのLSPを作ってVSCodeから色々叩けるようにしたらしい
https://github.com/ThalesGroup/frama-c-lsp
https://github.com/ThalesGroup/frama-c-lsp
まあopeningだし多少遅れても良いかと思ったけど、もしかしたらartifact evaluation chairなので最初からいることが期待されているかもしれない(地下鉄に1本乗り遅れた
May 19, 2026 at 11:42 PM
まあopeningだし多少遅れても良いかと思ったけど、もしかしたらartifact evaluation chairなので最初からいることが期待されているかもしれない(地下鉄に1本乗り遅れた
今週に入ってから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じゃな […]
Original post on mastodon.maswag.net
mastodon.maswag.net
May 19, 2026 at 11:07 PM
今週に入ってから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じゃな […]