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…
0
0
17
1,615
さいきん本当にいろんな人から日本旅行の話を聞くんだけど、この前インドの人と話しててミュンヘンに来る前は東京にいたって言ったら、「ここではビジネスではみんなヨーロッパに行きたがる。東京は観光でみんな行きたがる」って言われてそうか、つまりそういう話なんだな…ってなった
0
0
14
2,618
不正アクセスが増えまくってて怖いけど、ずっと予想されてたのでついに来たか感もある…
セキュリティはそもそも守備と攻撃の間に非対称性があって、守備は全称量化側でどうしても不利になる。双方が同じくらいのモデルを使うとすると、守備側は似たような戦略(見つけてなおす)だけだと勝つのが難しい
セキュリティはそもそも守備と攻撃の間に非対称性があって、守備は全称量化側でどうしても不利になる。双方が同じくらいのモデルを使うとすると、守備側は似たような戦略(見つけてなおす)だけだと勝つのが難しい
3
79
375
31,464
まあ今が何かの最後のときでこの先は変わるんだな…そして止まらないんだな、みたいな思いを持ってる人は結構いると思う。この印象は AI Frontier 側に近いはずの人と話すほど強くなるのもその通りで、その人達もそう思っているという事実が静かに衝撃を与える
note.com/takahiroanno/n…
note.com/takahiroanno/n…
0
11
72
13,235
今週はアトランタに来てるんだけど、アトランタは全米で最も監視カメラが多い都市らしい。ちなみに警官も街中にめちゃめちゃおり、カメラとの連携も進んでるらしい。でもそれで安全に感じるかは当たり前だけど人によるっぽい… 他の場所に行くと「あれっ警察少ないな…」って思うとも言ってた
0
0
3
1,317
今週だけで4つくらいエスカレーションdoc書いてる
AI 時代になってインフラや専門性による優位性も長期プランも誰も気にしなくなって、仁義なき戦いが起こりまくり
一方で AI 関係なくちゃんとした設計思想や品質管理がないまま作られるとやっぱり酷いクオリティになるわけですよ、当たり前でしょ。。
AI 時代になってインフラや専門性による優位性も長期プランも誰も気にしなくなって、仁義なき戦いが起こりまくり
一方で AI 関係なくちゃんとした設計思想や品質管理がないまま作られるとやっぱり酷いクオリティになるわけですよ、当たり前でしょ。。
0
5
39
3,203
数週間が経過し、作るものが
素数判定→
素因数分解→
簡易pythonインタプリタ(?)→
弾幕ゲーム(??)
と謎の進化を遂げている、ちなみに環境はスマホ上で Pydroid + Gemini (検索のAIモード) というね、、ときどきチャットでコードが送られてきて「実行してみて！」と強要される
いまどきの子…なのか？
素数判定→
素因数分解→
簡易pythonインタプリタ(?)→
弾幕ゲーム(??)
と謎の進化を遂げている、ちなみに環境はスマホ上で Pydroid + Gemini (検索のAIモード) というね、、ときどきチャットでコードが送られてきて「実行してみて！」と強要される
いまどきの子…なのか？
次男が唐突にカシオのカラー関数電卓が欲しい！欲しい！と騒ぐので買ってあげたら、これ Python 動くのね。さっそく本見ながら毎日なんかぽちぽち打ってる。
今日はこれ作った、明日はあれ作る、と夢広がりまくり
うちの子はAIが得意なことが得意だなあ…と思いつつ
わかる、わかるよ、楽しいよねそれ
0
0
18
5,007
次男が唐突にカシオのカラー関数電卓が欲しい！欲しい！と騒ぐので買ってあげたら、これ Python 動くのね。さっそく本見ながら毎日なんかぽちぽち打ってる。
今日はこれ作った、明日はあれ作る、と夢広がりまくり
うちの子はAIが得意なことが得意だなあ…と思いつつ
わかる、わかるよ、楽しいよねそれ
今日はこれ作った、明日はあれ作る、と夢広がりまくり
うちの子はAIが得意なことが得意だなあ…と思いつつ
わかる、わかるよ、楽しいよねそれ
0
1
37
8,618
Mythos が Apple MIE を破ったのは割と象徴的というか、MIE はすごく良くやってるけど穴をゼロにする手法ではないので、AIで攻撃側のコスト関数が変わって「狙えば攻撃は可能なはず」がそのまま示された形に見える。攻撃面を大きく減らす MIE の利点は変わらないけど、戦略的位置づけは変わりそう
0
2
16
3,359
ふだんユーロの国にいるせいでドルの値段を見るとユーロ比だと安く感じてしまうけど、ここで正気に返って円換算すると意識が飛ぶので正気に返らずに1ドルも1ユーロも100円換算し続けるのですよ…
0
1
23
3,295
またアメリカ出張に来てるけど、ミュンヘン出るときのチェックインカウンターの人がこの前日本に旅行してきてそれがすっごく良かったらしく、
「最高だったわ〜！であなたいつ帰るの？え、ここに帰ってくるの？え、ここに住んでるの？？なんで？？？」
と出国に関係ない質問されまくって答えに困った
「最高だったわ〜！であなたいつ帰るの？え、ここに帰ってくるの？え、ここに住んでるの？？なんで？？？」
と出国に関係ない質問されまくって答えに困った
1
0
31
4,132
どういうコードベースを想定してるのかな？ASTはデータフローを表すものじゃないし100%のグラフの根拠にならない、Taint 解析も証明支援系や充足可能ソルバを使わず AI に探索させても特に保証にならないけど
(構造化されたデータをあげた方が良いケースがあるのはその通り)
qiita.com/harupython/ite…
(構造化されたデータをあげた方が良いケースがあるのはその通り)
qiita.com/harupython/ite…
0
2
22
3,819
ここ２か月くらいでのサイバーセキュリティ界の様相の変わり方がなかなか激しいな… いろんなグラフの傾きが急に変わってもうまったく違う性質の問題になってる。でももっと怖いのはこれがサイバー界だけじゃなくて外でも起こるだろうことかしら
0
2
12
2,885