AIで形式証明もだいぶ楽になってみんなやってる感じあるけど、Rocq を1.8億行は規模がだいぶおかしい。というか実際には試行過程では10億行くらい生成してるのね… 証明行が大きいのはソースコードじゃなくてバイナリでやってるからもありそう、AI がなかったらいろんな意味で出来なかった方向性だな
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
さいきん本当にいろんな人から日本旅行の話を聞くんだけど、この前インドの人と話しててミュンヘンに来る前は東京にいたって言ったら、「ここではビジネスではみんなヨーロッパに行きたがる。東京は観光でみんな行きたがる」って言われてそうか、つまりそういう話なんだな…ってなった
不正アクセスが増えまくってて怖いけど、ずっと予想されてたのでついに来たか感もある…
セキュリティはそもそも守備と攻撃の間に非対称性があって、守備は全称量化側でどうしても不利になる。双方が同じくらいのモデルを使うとすると、守備側は似たような戦略(見つけてなおす)だけだと勝つのが難しい
まあ今が何かの最後のときでこの先は変わるんだな…そして止まらないんだな、みたいな思いを持ってる人は結構いると思う。この印象は AI Frontier 側に近いはずの人と話すほど強くなるのもその通りで、その人達もそう思っているという事実が静かに衝撃を与える
note.com/takahiroanno/n/n4ac…
今週はアトランタに来てるんだけど、アトランタは全米で最も監視カメラが多い都市らしい。ちなみに警官も街中にめちゃめちゃおり、カメラとの連携も進んでるらしい。でもそれで安全に感じるかは当たり前だけど人によるっぽい… 他の場所に行くと「あれっ警察少ないな…」って思うとも言ってた
確かにアメリカの人は人にもよるけどかなり婉曲表現を使う気がする… 婉曲過ぎて何言われてるのかわかんないこともあった
ドイツは直球表現の人が多くて、最初引いたけど(いや今でも時々引くけど)これはこれでわかりやすくて悪くない。めちゃ言い合ってるうちにだんだん仲良くなってることも
今週だけで4つくらいエスカレーションdoc書いてる
AI 時代になってインフラや専門性による優位性も長期プランも誰も気にしなくなって、仁義なき戦いが起こりまくり
一方で AI 関係なくちゃんとした設計思想や品質管理がないまま作られるとやっぱり酷いクオリティになるわけですよ、当たり前でしょ。。
数週間が経過し、作るものが
素数判定→
素因数分解→
簡易pythonインタプリタ(?)→
弾幕ゲーム(??)
と謎の進化を遂げている、ちなみに環境はスマホ上で Pydroid + Gemini (検索のAIモード) というね、、ときどきチャットでコードが送られてきて「実行してみて！」と強要される
いまどきの子…なのか？
次男が唐突にカシオのカラー関数電卓が欲しい！欲しい！と騒ぐので買ってあげたら、これ Python 動くのね。さっそく本見ながら毎日なんかぽちぽち打ってる。
今日はこれ作った、明日はあれ作る、と夢広がりまくり
うちの子はAIが得意なことが得意だなあ…と思いつつ
わかる、わかるよ、楽しいよねそれ
Mythos が Apple MIE を破ったのは割と象徴的というか、MIE はすごく良くやってるけど穴をゼロにする手法ではないので、AIで攻撃側のコスト関数が変わって「狙えば攻撃は可能なはず」がそのまま示された形に見える。攻撃面を大きく減らす MIE の利点は変わらないけど、戦略的位置づけは変わりそう
またアメリカ出張に来てるけど、ミュンヘン出るときのチェックインカウンターの人がこの前日本に旅行してきてそれがすっごく良かったらしく、
「最高だったわ〜！であなたいつ帰るの？え、ここに帰ってくるの？え、ここに住んでるの？？なんで？？？」
と出国に関係ない質問されまくって答えに困った
どういうコードベースを想定してるのかな？ASTはデータフローを表すものじゃないし100%のグラフの根拠にならない、Taint 解析も証明支援系や充足可能ソルバを使わず AI に探索させても特に保証にならないけど
(構造化されたデータをあげた方が良いケースがあるのはその通り)
qiita.com/harupython/items/e…
ここ２か月くらいでのサイバーセキュリティ界の様相の変わり方がなかなか激しいな… いろんなグラフの傾きが急に変わってもうまったく違う性質の問題になってる。でももっと怖いのはこれがサイバー界だけじゃなくて外でも起こるだろうことかしら