博士取得やUKでポスドクをはじめたりなどがあった。博士号取得は正直去年という感覚が否めないのと、以前書いていた2024年度を振り返ってという未公開記事と被っているので、主に4月以降のUKについてからの話をまとめる。blueskyを見ながらなんとなく思い出していきたい。
入国
https://bsky.app/profile/moratorium.bsky.social/post/3llglm6jdt22e
https://bsky.app/profile/moratorium.bsky.social/post/3llizbpz4fk27
https://bsky.app/profile/moratorium.bsky.social/post/3lljpdh27qk27
https://bsky.app/profile/moratorium.bsky.social/post/3llognmhlts2x
懐かしい。とにかく(大学の優しいシステムのおかげで)家だけががあり、ほかは何も無い状況からスタートしたので、まあもちろん何もない状況よりはよかったものの、かなり色々手探りで大変だった。上のポストにもあるように、まずインターネットがなく、家にmobile回線が届かないので、寒い中まだ使えた東大のeduroamアカウントを使って諸々を調べざるをえなかった。主に、インターネットがない影響で、家の中でやることが本当になく、eduroamで適当に動画をダウンロードしてオフラインで見るなどをしていた気がする。
https://bsky.app/profile/moratorium.bsky.social/post/3llognmhlts2x
ちなみに未だに僕より英語喋るのが下手なやつみたことない、blueskyを見ていると当初はかなり英語が終わっていることを気にしていたっぽいが、強い心を手に入れることで解決してしまった(そういうことをしていると英語力は大して伸びない)
研究
- 4月直後は博士中にやっていた話を終わらせた。あとから思うともう少し練れた部分は多かったのではないかと思わなくはないが、まあ新天地での研究に集中したかったので仕方がない
- 個人的にまだ発展性があると思っているのでこちらもほそぼそ続けていきたい
- また、予算関係で面倒が発生したため、海外学振に急遽申請することにしたため4月末は思ったよりもこちらの研究ができなくて困った記憶がある。予算って突然消えることがあるんだ。ちなみに無事通ったため、日本政府が狂ったり日本円が狂ってしまわない仮定の上で数年の安定を得た
- こちらの研究室に来て一番良かったのは、クソデカコラボレーションで研究を回すというのができた点。たまに https://bsky.app/profile/moratorium.bsky.social/post/3lt4xfsfls22w のような気分になることもあったが、全体的には今まで(手数含めなかなか一人で回すのは難しいので)やれてこなかった実際のソフトウェアに自動検証を応用する研究を実際に行うことができており、これ自体はかなり気分が良い。
- ちなみにこのブログを読んでいる人が興味があるのかは謎ですが、大雑把に何の研究をしているかを書いておくと、C(やunsafe rust)で書かれたシステムプログラムの検証手法を研究しています。この分野は非常に長い研究の歴史があるわけですが、我々のアプローチは実用と研究のギャップを埋めるためのyet anotherな方法論を提示するという観点で「仕様を書くと即それがテストに利用できるし、さらに仕様・証明を書いていくと、信頼性を向上していけるような枠組み」というものを分離論理上の検証システムとして実装しています。
- このようなシステムプログラムの(ほぼ全自動な)検証手法はAI時代においてますます輝く、今まで人類の手に届きそうでギリギリ届かなかった聖杯の一つだと思っていて、特にLeanのような定理証明支援系のコードの自動生成が注目されがちなものの、LLM時代においてもつきまとうだろう証明と実装の保守運用という問題に対する一つの解決策のひとつなんじゃないかなと思っています。
- 来年以降のAI性能がどうなるかイマイチ読めないものの、特に現代のCoding Agentの成功を見ると、test-debugを通して検証を遂行する枠組みはその意味でもかなりAIと親和性が高いのではないかと思っていて、その上でAIが利用できるより強固なPL的土台を構築していくことが全体の検証精度向上に大切だろうと思っているんですが、来年以降どうなるやら。実は全部AIってやつでなんとかできるかもしれません。
訪問国・地域
- エディンバラ・グラスゴー
- バルセロナ
- 旅行で行った
- サグラダ・ファミリアには入れず(は?)
- 旧市街やいくつかのガウディの建築物、グエル公園や浜辺も訪れたが、最終的に一番良かったなと感じたのは(やや居住エリアで観光客としてのこのこ行くのが少しはばかられたのと、途中にいた放し飼いの番犬が突然近寄ってきて命の危機を感じた点を除けば)Bunkers del Carmelという場所で、バルセロナの市街や海を一望できてかつそこまで混んでない個人的なお気に入り
- あとはバルセロナ郊外のモンセラートにもいって、ここも良かった、岩とか登れる
- アイラ島
- 旅行で、ウイスキー蒸留所巡りを
- Laphroaig, Lagavulin, Kilchomanの3つの蒸留所を訪問した
- Lagavulinではexperienceに行き、Lagavulin 26年を飲み、これが今までの人生で飲んだことのあるもっとも価値のあるウイスキーとなった
- 蒸留所ツアー的な観点では、Kilchomanの体験がかなり良かった。まず、visitor centreが新しめで、大きな暖炉があったりクオリティの高いランチが食べられるレストランがあったりなど見学者のための施設自体が洗練されていた点や、割と大量にタダ同然で多様な種類のウイスキーを飲むことができるバーなどもあり、バスが通ってないという難点を鑑みてもおすすめするならここだなという感じ
- ちなみに、アイラ島は思ったよりもでかく、東京23区くらいの大きさがあるらしい。間違っても歩いて回れると思ってはいけない
- 島の至る所に羊がおり、かなりかわいい。実際自然がかなり豊かで、Puffinなども実はいい時期に行くと見られるらしい。
- その他イギリスの地域
- ケンブリッジ(は?)
- 未だに行ったことのない場所も多いが、有名アクティビティはさすがに網羅した、パンティングとかね。
- collegeはKing’s, Trinity, Queen’s, St John’s, Clareには入ったし、他にも入った事がある場所があるが、失礼なので名前を忘れてしまった。個人的に、おすすめするなら、やはりKing’s collegeのチャペルで、とはいえ、個人的にはQueen’s collegeのこぢんまりとした感じも好き
- パソカタオタク向けケンブリッジオススメスポットとしては、公式Raspberry Piショップがあり、これは世界唯一のはず(そもそも需要がね。。)。見た目はAppleストアと見紛う感じで、ただ中に入ると多様なRaspberry Piやその拡張アタッチメントが売られている。Tシャツやマグもあるが、実はこれはショップ限定ではなく、オンラインで買える。
- もう一つのパソカタ向けスポットは、ひょっとすると弊デパートメントかもしれないが、それをのぞくと、The Centre for Computing Historyで、ここにはクソデカCPU(レジスタ等の動作がLEDのチカチカで可視化されている)が置かれていたり、古いMacやらゲーム機やらが置かれており、近現代のコンピュータを感じられる
- 他にもボルダリング、植物園、博物館pubといったものも当然あるし、クリスマスマーケットやら、教会やら、無意味に広大な草原やら、日本ではあまり見ないものが多いので、単に観光できても数日は楽しめる(なおその後…)。なので皆さん会いに来てください。
- Ely
- でかい大聖堂がある
- Cam川の続きが流れており、いい感じの川辺があり、良い
- ロンドン
- https://bsky.app/profile/moratorium.bsky.social/post/3lx57wdwkek2v
- 大英博物館で、ロゼッタストーンやミイラを一度くらい見ておいてもバチは当たらないかもしれないとおもって、見に行った。
- ミュージカルも3本見た(Wicked, Phantom of the opera, les miserables)。問題として英語が聞き取れん
- ロンドン塔、Victoria and Albert Museum、ビッグベンなどwestminster周辺、バッキンガム宮殿など有名どころは訪れた
- Kew Gardenというロンドンの西にある大きな公園があり、ここが思いの外良かった。アクセスが悪いのが難点だが。heathrowに近く、頭上をブンブン飛行機が飛んでいる
- ケンブリッジ(は?)
- パリ
- 学会で訪問
- 到着した日がちょうど2024-2025年シーズンのChampions Leagueの決勝の日と被っており、街中がカオスで良かったような最悪だったようなという経験だった。結果的にパリ・サンジェルマンが優勝したっぽく、優勝後はそこらじゅうで素人がロケット花火をあげたり、クラクションをならしながら走行する車がいたり、広場で暴走するバイクがいたりしていて、命の危険すら感じたが、ある意味で面白い経験ではあった(あとから思うと)
- 4月から12月の間で、海外で寿司っぽいものを唯一食べたのがパリだったが、その店がかなり微妙で、さも問題が何一つないかのような顔をするのが難しかった
- 学会のバンケットがかなり良かった。そこで出たワインが個人的に結構良かったなと思ったので、知り合いのフランス人にその話をしたところ、まあ別にそんなことないという反応をされて、悲しくなった
- シンガポール
- 学会で訪問
- ホテル代を低めに抑えたら、今まで泊まったことのあるホテルの中では、かなり最悪寄りのホテルでつらかった。まず、なんか玄関がよくわからん匂いがする。これはあとから気付いたが、床清掃のための洗剤の匂いの模様で、その意味では清潔さの犠牲かもしれない。また、シャワーとトイレが一体型(仕切りがいっさいなく、シャワーをすると便器が濡れるような状態)で、最初どうすればよいか困惑した。ちなみに、あとから知ったがこれは東大三鷹寮も同様らしい。
- https://bsky.app/profile/moratorium.bsky.social/post/3m3hwm4yjhs2f
- 一番すごいなと思ったのは空港隣接の商業施設Jewelで、ただでさえ蒸し暑いのに、天井から落ちてくるクソデカ滝により、フードコートが熱帯雨林になっていた、エグい。とはいえ壮観なことには間違いなく、涼しい部屋でinstagram越しに見るのが一番良いだろうなと思った。
- changi空港は、今まで行ったことのある空港の中では一番規模が大きく綺麗だったように感じる。一方ヒースローは。
- Latisana? Lignano Sabbiadoro? (Venice?)
- BunkyoWesternsの人が集まらなかったっぽいので、まあ近いしryanairで200ポンドでいけるしということでノコノコついていった。ちゃんとした方のCTFであんまり仕事できなかったので、事実上リアルワールドCTFという名のワクワク宝探しで歩き回る労働力だけ提供した。優勝に貢献できたとはさすがに言えませんね…
- ホテルのご飯が本当に美味しくなかった。本当に美味しくなかった。
- Veniceの空港に到着して、そこから電車に乗る乗り換えのタイミングで10分くらいVeniceを観光した。駅前だけでも普通に美しかったが、ゴンドラに乗ったりさすがにしたかったのでまた再訪しよう(そもそもStanstedに行くまでの電車が突然キャンセルされてかなり困った、結局空港に1時間前についたが、やたらと荷物検査がすぐに終わったのでなんとか間に合った、こういうときに限ってryanairは大して遅延しないので許せない)
- あまりに金をケチりすぎたので、VeniceからStanstedに行く飛行機が早朝で、しかも休日の場合電車がないことに前日に気づいたので、なくなく最終日前にVenueを出発し、50ユーロくらいのMestreのホステルに泊まった。さすがに金をケチり過ぎである。とはいえ、同室になった人との会話は割と楽しかった。一人が中国出身でミラノのコンセルバトワールで音楽を習っているという話で、イタリア語がペラペラですごかった。
- 日本(は?)
- 渋谷行ったら人多くてウケた
- 改めて考えると日本の都市はどこもクソでかいと思う
- 東大正門がよく分からん紫色のライトアップしてて、Tiktoker/インスタグラマーに媚びてんのかなと思いました、あれいる?
その他
- ICC作問、いっちょ噛みだけした。5,6月くらいに問題を作ったが、気づいたらAIが解けるようになっていて、かなり焦った、直前で修正して多少改善したが、ひょっとすると5.2 Codexとかなら解けてしまうかもしれない。コンパイラ等のロジックバグを問題にするのが好き寄りだったが、こういった問題はAIの得意分野だと思うので、作問がかなり難しい時代になったなと思うし、来年にはもう成立する問題が作れないかもしれない
- Alpacahack: 最後のpwn回に参加した、楽しかったねえ。6時間で終わるAlpacahack、本当にドーパミン中毒のクソガキ向けコンテンツだと思っていて、気持ちがいいんですよね、これがAIによって潰されると思ったら許せねえよ、なんとかなりませんか?
- Daily Alpacahackの作問も最初期に本当にいっちょ噛みだけした、気づいたら一億問くらい問題が作られており、完全に笑っていた。実は12月5日に出題したInteger Writer、割と気に入っているbeginner向け問題で、簡単なスタック破壊問ではあるものの微妙に一捻りあって、ちょっと気持ちがいいんですよね。皆さん見てみてください。実際、(coding agentだとさすがに基本解けるが)Thinkingでは必ずしも解けるか解けないかガチャが入る感じの問題になっており、まだまだAIには負けんぞという気持ちを新たにできます。
- 日本に帰ってきた際に飲んでくれた方々(飲んでくれる予定の方々)ありがとうございます。日本楽しすぎという気持ちになるので、困りました
- ケンブリッジ大学の日本人会でもところどころ顔を出して、微妙に自分の研究について発表をしたりもした。プログラムの自動検証を人に伝えるの結構難しくなんとなくニュアンスを伝えようと思ってひたすらみじん切りが停止するのかどうかについて議論する変な人をしたりした。こちらにいる日本人PhD・ポスドクはほとんどが医療・生命科学系でなかなか肩身が狭い、コンピュータ科学系に来る人がいたらお声がけください
- 人生パートでももろもろがありました、あったらしいです
https://bsky.app/profile/moratorium.bsky.social/post/3lnvlyjhsg22f
気づいたら日本時間でもう年を超えそうなので、done is better than perfectということで終わらせるか。来年もよろしくおねがいします。




















