読み書きプログラミング

日常のプログラミングで気づいたことを綴っています

Leanを1行も書いたことがないLean使いになる!

遅ればせながら、Antigravityで初めてAIエージェントを試しました。
便利ですね。
パーサをちょっと書いてもらって「こりゃすごい!」と思ったのですが、すぐクォータが切れて2週間待てと…

流石にこれでは使い物にならないので、VSCodeの拡張Clineを導入しました。
サブスクは好きじゃないので、従量課金にすべくGemini API。

(余談ですが、最近までGeminiで満足していたのですが、あっちこっちあれがいいこれがいいという話を聞くとGeminiもひとつかな?という気分になったので、AIの評価というのは難しいものですね)

で、エージェントで何をしようかなと思ったのですが、やっぱりこれを機会に数学かと。
数学はついに、AIというツルハシで挑める金鉱という時代になりました。
なので、Leanを1行も書いたことがないLean使いになろうかと。

難しい現代数学よりオイラー辺りのほうが好きなのでその辺から遊ぼうかな。

追記。
n^2が偶数ならnも偶数の証明に$0.5かかりました。(無料枠も使ったから実際にはもっと?)
そして…できたコードがよくわからない🤪

Gemini in Chromeのショートカットに💢

最近、Geminiがお気に入りです。実際、無課金勢には今一番性能がいい気がします。

で、しばらく使っていたSafariをやめてChromeに戻りました。Gemini in Chromeのためです。
見ているサイトの話ができるっていいですよね。AIアプリにURL貼っても読めないことが多いし。

ところが、Gemini in ChromeはグローバルにCntl-Gをフックしてショートカットにします。
Cntrl-Gってエディタの必須ショートカットですよ??何してくれるん?です。

Chromeの設定の「AIイノベーション」から「Gemini in Chrome」の設定を開くことができます。
そこにショートカットの設定があるので、他のキーかショートカットなしにすればOKです。

AFM 3 Core Advancedって結局何?

WWDC 2026で一番気になったのがAFM 3 Core Advancedでした。
どうも、12GB以上のDRAMを持つ端末限定で、20B級VLMが動くようです。
20B級は知識としても相当です。これはすごい!
ウェイトをDRAMに全部置かずに決めたMoE分SSDから読むとか。

でも、なんかもやもやするんですよねぇ。
少なくともApple純正機能としては、そのAFMを使うかをユーザーに選ばせる気はなさそうです。
必要に応じて適したモデルを使う。
ということは、Core Advanced未対応の端末の場合、処理はPCC(Private Cloud Compute)が処理することになりそう。
Cloudなので当然、レイテンシーとか悪くなり、プライバシーも若干心配になります。
でも応答が稚拙になることはなさそう。
もしかしたらPCCではなくCoreにフォールバックするかもしれなくてその場合、応答は稚拙になるはずですが。

もしCoreにフォールバックしなかったら、なんかレイテンシーを忘れると、Core Advancedって、クラウド代大変だから12GB DRAM端末は自分で計算してくれっていうせこいサービスに思えませんか?

もしかしたら、Core Advanced未対応端末を使うことがApple Intelligence勝ち組かもしれません🤪

Zigがいい!

Swiftでガチガチのチューニングに挑戦して挫折しました。
今更C++も大変だし、Rustもアイデアは素敵と思ってもコーディングは何かしんどいという感じ。
諦めかけていたところ、Zigを知りました。

Rust is a better C++, Zig is a better C.

だそうで、その通りの言語仕様です。
メモリモデルがRustのように目新しくないので、文法さえ知れば普通に書けます。

まだ、バージョン1に到達していなくて破壊的な改良が続いているのでプロダクションに使うのは難しいと思いますが、正式版が出たら一定の層に流行ると思います。

Python/Swift/Zigの3つの言語がそれなりに使えたら大体満足できそう。
Python, Swiftの代替候補は色々ありますが、3つ目のC/C++/Rust層がつらかったんだよねぇ。
「俺の最強言語」という厨二病を持ちながら3つの言語で頑張ればいい😁

というわけで、Zigが無事正式リリースを迎えることを心から願います。
できれば貢献したいな。何かツール作ろうかな?

やっぱりMac Studioじゃない?

今年1月のProject DIGITSの発表から10ヶ月弱、ようやくDGX Sparkが出荷され始めました。

LLMについて色々調べて、特にToken Generationはメモリ帯域律速だということもわかって、DGX Spark、1PFLOPSの割にきついんじゃないかという気がしていました。
ベンチマーク結果は、M3 Maxと同じぐらいのようです。メモリ帯域(Spark 273GB/s, M3 Max 400GB/s)を考えると善戦。
(というか、M3 Maxチューニング足りてないのかも)

さて、値段ですが、日本では代理店経由で価格未公開が多いですが、公開しているところを参考にすると、税込70万円かそれ以上。
同等のスペックをMac Studioでカスタマイズすると、

で、税込733,800円。

AppleSSDは高速ですが、Apple税が入っているので?節約コースを考えると、

583,800円+40,000円=623,800円。DGX Sparkより安いです。

CUDAに慣れていてLLMをゴリゴリしたい人にはDGX Sparkはいいかもしれませんが、その辺りはお任せ、大きなLLMを動かして使いたいだけという人には、Mac Studioがお値打ちなようです。

一番に最初に、LLMにはMacがいいと言った人の先見の名に感心します。
当時、私も、LLMと言えばNVIDIA GPU必須やろ、さすがにMacがいいは言い過ぎと思いました。

AI PC/Copilot+ PCも基本UMAですが、Macほどその自由度が高くないようです。
NPUがメモリをフルにアクセスできなかったり帯域が絞られていたり。

というわけで、DGX Spark欲しい熱が冷めて、Mac Studioいいなぁと思いながらIntel iMacでブログを書いている今日この頃です。

Swiftが嫌いになりました

struct InlineArray<let count : Int, Element> where Element : ~Copyable

InlineArrayのシグニチャを見て、「え?Elementはコピーできないの?なんのこっちゃ」と思ったのですが、今時のLLMに聞くとこれは「コピーできてもできなくてもいい」という意味らしいです。
そして、whereでElementがコピーできないという制約は書けないらしいです。

狂っている。控えめに言って狂っている。

この瞬間、Swiftの嫌なところがどっと湧いてきました。

classとstructって何?最初は参照型か値型かでメンタルモデルも作りやすかったです。しかし今では特に大きなデータの場合、結局どっちで作るのがいいか、ほぼどうでもいいのに決定しなければいけない無駄な意思決定を要求されます。

DispatchQueueかasync/awaitか。async/awaitのほうが効率良さそうなのはわかります。しかし移行するのにHaskellモナドぐらい敷居があります。一つasyncで書くと、利用しているメソッド群を雪崩式にどどどっと書き直さないといけない。過去のリソースを使わない新規プロジェクトならいいですが、そうじゃない場合、結局両方書けっていうこと?

SwiftUIって結局、ロジックとUIの分離が難しくなってない?MVCかMVVMかTCA?もうええって。

ずっと、Swiftラブだったのに。愛はいつか冷めるもんですね。
ああ美しい言語と出会いたい。

Gemma 3nは一体どうやって使うの?

5月にプレビュー版が公開されていたGemma 3nが正式公開です。

developers.googleblog.com

プレビュー版では.task(LiteRT (TensorFlow Liteのリブランディング))ファイルが公開されて、Androidでは一応動かせたようですが、正式公開では、各機械学習ライブラリ向け.safetensorsが公開されただけです。
モバイルで動くことが一番のアピールポイントなのにモバイル向けカスタマイズはサードパーティさん頑張ってと。
音声や動画まで扱えるマルチモーダルLMってサードパーティでどこも実現していないような…

研究段階だったLLMがいきなりイノベーションの先端に立って3年弱。研究者が製品を出荷するような状況で大変なんでしょうね。
そろそろ、ライセンス含めて使いやすいローカルLLMが出てきて欲しいです。