uehaj

もともと2024大統領戦でもHarissの方が10ポイントもTrumpより得票が多かった。

・TLA+やQuintは、見た目はプログラムでも、書いているのは「状態の組についての論理式」と「その上の時相論理式」 ・モデル検査は、その含意が成り立つかを有限の範囲で機械的に確かめる作業 ・数学や論理学の話は、使い方の表面ではなく、意味の土台にある ・TLA+は、作者のLamportが「仕様はプログラムではなく数学だ」と強調している言語 ・土台は、集合論（ZF集合論）と時相論理 ■ なぜ実務では数学が表に出にくいか ・仕様を書いてモデル検査にかけるだけなら、プログラムを書く感覚で使えてしまう ・Quintはまさに、その使い方に合わせて文法をプログラマー向けにしている ・数学が前面に出てくるのは、詳細化を示すとき、活性を扱うとき、TLAPSで証明するとき

生成AI・AIコーディング ニュース（2026年11月7日） 今日の注目：AIのセキュリティ能力をめぐる発表が続きました。Google DeepMindがAIエージェントで旧来の1024ビットRSAに2つの弱点を見つけたと発表し、OpenAIはサイバーセキュリティ能力を自社基準で最高の「Critical」と評価したGPT-6 Cyberを、限られた組織だけに提供し始めました。 ■ Google DeepMind、AIエージェントで旧来の1024ビットRSAに2つの弱点を発見 Google DeepMindが11月6日、人間の暗号研究者とAIエージェントが協力して、旧来の1024ビットRSAに2つの弱点を見つけたと発表しました。1つは署名偽造に関するもので、条件によっては従来の最良手法より理論上約1,600倍効率的です。もう1つは鍵の一括因数分解で、1024ビット鍵を1本追加で破るときの平均コストが約30分の1に下がります。2048ビット以上の鍵は影響を受けないとしています。 出典: officechai.com/ai/google-dee… ■ OpenAI、セキュリティ研究者向けの「GPT-6 Cyber」を限定提供 OpenAIがGPT-6 Astraをサイバーセキュリティ向けに特化させた「GPT-6 Cyber」を公開しました。Preparedness Frameworkではサイバーセキュリティ能力を最高の「Critical」と評価しています。エクスプロイト開発タスクの96%を完了しており、当面はDaybreak Redの審査を通った組織だけが使えます。 出典: deploymentsafety.openai.com/… ■ OpenAI、評価額1.25兆ドルで110億ドルを調達とBloomberg報道 Bloombergが11月6日、OpenAIが評価額1.25兆ドルで新たに110億ドルを調達したと報じました。この調達ラウンドは合計約200億ドルになる見込みで、数週間以内に完了するとされています。9月の報道では評価額1.4兆ドルで300億ドルを目指すとされており、それを下回る水準です。 出典: techcrunch.com/2026/11/06/op… ■ Cursor、クラウドエージェントでWebアプリを作って公開まで行う「Build Live Apps」を提供 Cursorが、クラウドエージェントで動くWebアプリを作り、そのまま公開できる機能を発表しました。アプリの土台作り、必要に応じたPostgresデータベースの用意、Cursor SSOによる認証、ホスティングまでを自動で設定します。公開前には決まった手順の検査とエージェントによる検査の両方でセキュリティを確認し、ユーザーが明示的に公開を決めるまで公開されません。クラウドエージェントを有効にした全有料プランで使えます。 出典: cursor.com/changelog/build-l… ■ Anthropic、Claude Enterpriseにセキュリティチーム向けの管理機能を追加 Anthropicが11月5日、Claude Enterpriseにセキュリティセンター（ベータ）を追加しました。組織の設定をAnthropicの推奨設定と比べられます。プロンプトやツール呼び出しの前にDLPなどの検査を挟める「Inference hooks」は一般提供になりました。親組織の一元管理コンソール、Admin APIによるメンバーのサインアウト、IPアローリスト、CoworkでのEDR対応もベータで加わっています。 出典: claude.com/resources/article… ■ GitHub、Copilotの効果ダッシュボードでチャットとVS Codeエージェントの利用も集計 GitHubが11月6日、Copilot impact dashboardのエージェント導入チャートにCopilot ChatとVS Code Agentsウィンドウを加え、集計対象を9機能にしました。「Passive users」という区分は「Chat-first users」に名前が変わりました。企業・組織向けの28日間利用状況レポートにも同じ2機能が加わります。 出典: github.blog/changelog/2026-1… ■ METRの独立評価、AnthropicのAI研究開発のペースが約1.9倍に 評価機関のMETRが11月5日、AnthropicのAI研究開発がどれだけ加速しているかを独自に評価した結果を公開しました。2025年10月以降、Anthropicの能力指標の伸びは1.9倍（95%信頼区間1.5〜2.8倍）に速まったと推定しています。METRは、加速分の「おそらく約80%」はAIによるものとみています。ただし、METRが最も重要とした証拠の多くはAnthropicが非公開にしています。 出典: metr.org/blog/2026-11-05-ant… ■ Thinking Machines Lab、MoEモデル「Inkling 2 Small」を発表 Thinking Machines Labが「Inkling 2 Small」を発表しました。総パラメータ数5,940億、アクティブ17B（170億）のMixture-of-Expertsモデルで、画像入力にも対応します。まずTinker経由で提供し、外部の安全性テストを経たうえで、重みを「来週」Apache 2.0ライセンスで公開する予定です。 出典: thinkingmachines.ai/news/ink…

今日の学び。outputstyle=LearningでClaude Codeに教えてもらうと学習がとてもはかどります。 Q. テストと検証は違うのか。 A. 一般と形式手法の世界の用法という分野によって「検証」の意味は違います。 Q. ソフトウェア工学一般での「検証」とは何か。 A. 「仕様どおりに作られているか」を確かめる活動の総称です。この定義では、テスト、レビュー、静的解析、モデル検査、定理証明がすべて検証の手段です。IEEE や ISO の用語集はこの立場で、V&V（Verification and Validation）の V がこれです。対になる「妥当性確認」(validation) は「そもそも作るべきものを作っているか」です。この用法では「テストは検証の一種」なので、「テストと検証は違う」とは言えません。 Q. 形式手法の世界での「検証」とは何か。 A. 「性質が成り立つことを数学的に示す」ことに限定します。この用法ではテストは検証に含まれず、さっき説明した区別になります。Quint の verify も、この狭い意味です。 Q. 結局どう理解すればよいか。 A. 文脈で範囲が変わります。ソフトウェア工学一般では、検証は仕様適合を確かめる活動すべてを指し、テストも検証に含まれます。形式手法では、検証は数学的に正しさを示すことだけを指し、テストは含まれません。私がさっき「違う」と言い切ったのは Quint の文脈だったからで、一般論としては「テストは検証の一手段だが、網羅性のない弱い手段」が正確な言い方です。 Q. なぜ同じ語で意味がずれるのか。 A. 分野ごとに語が育った歴史が違うからです。形式手法の人が「テストでは検証できない」と言うときは狭い意味、品質保証の人が「テストで検証した」と言うときは広い意味で、どちらも誤りではありません。混乱を避けたいなら「網羅的か」「ok が何を保証するか」で言い換えるのが安全です。語の定義争いより、保証の中身を Q. テストは反例探しか。 A. 本質的にはそうです。テストは「この入力で、この結果になるはず」という主張を立て、実際に動す行為です。破れれば反例が見つかったことになり、破れなければ「この入力では反例がなかった」としか言えません。Dijkstra の「テストはバグの存在を示せるが不在は示せない」という言葉は、テストが反例探しであることをそのまま述べています。 Q. では quint run とふつうのテストは同じものか。 A. 構造は同じで、違いは入力の選び方だけです。ふつうの単体テストは人間が入力を選びます。quint run は乱数が選びます。プロパティベーステスト（QuickCheck など）も乱数で選びます。どれも「性質を書き、入力を与え、破れを探す」という形で、run はプロパティベーステストを状態遷移系に適用したものと見なせます。 Q. モデル検査も反例を出すが、それはテストではないのか。 A. 反例を出す点は同じですが、入力の選び方が「全部」です。TLC は到達可能な全状態を訪ね、Apal論理式で一括して扱います。全部調べて反例がなければ「範囲内に反例は存在しない」と言えるので、そこが反例探しを超えて検証になる境目です。言い換えると、モデル検査は「網羅的な反例探し」で、テストは「部分的な反例探し」です。 Q. テストが反例探しなら、テストに価値はないのか。 A. 逆です。反例が見つかること自体が最大の価値で、実務で見つかる誤りの大半はテストで見つかります。網羅しなくても、1 手で破れるような誤りは数回の試行で踏みます。今回も 0 → -52 は 22 ms でした。網羅が要るのは、特定の状態にしか現れない深い誤り、たとえば残高ちょうど 100 でだけ起合です。テストで取れる誤りを安く取り、残りを検証に回す、という分担が自然です。 Quintおもろい

■ HN AIダイジェスト 2026/11/7（agents-radar より） ■ 特に注目 ◆ Claude Code が訪問先サイトにメールアドレスを送信（1554pt / 493コメント） ・Claude Code がアクセスしたサイトに、User-Agent ヘッダー経由でログイン中アカウントのメールアドレスを送っていたという報告。この日の HN AI 系で断トツの1位 ・最新版 v2.1.319 の時点で、アカウントのメールや User-Agent 文字列を含むシェル呼び出しを拒否する修正が動いている模様 ・業務で使っているなら、バージョンと外部アクセスの経路は確認しておきたい ◆ Jev を使った LLM ジャッジで Opus のコストを75%削減 ・ダイジェストの総評で目玉扱い。精度を上げつつコストを大幅に下げたという話。元記事のリンクは未掲載なので要確認 ◆「AI が AI 研究を劇的に加速している」（207pt / 158コメント） ・AI による研究の自己加速を論じた長文 ・同日に「AI の研究開発が独創的だとは信じがたい」という反論（180pt）も上がり、賛否が割れている ■ その他の新着 ◆ モデル・研究 ・Gemini Omni 1.2 Flash（297pt）：低遅延のマルチモーダルモデル。「ベンチ向け最適化では」という声も ・Memorilla（86pt）：潜在意味索引で LLM に長期記憶を持たせる論文 ◆ ツール ・NVKE（122pt）：Nvidia の GPU ワークロード向け Kubernetes ・AegisKernel：AI エージェント向けのゼロトラスト POSIX ランタイム ・LEGO の機構を資料からエージェントが推論してアニメ化する Show HN ◆ 業界・議論 ・Anthropic の IPO、買い手側の想定評価額は1.1兆ドルまで低下（235pt / 492コメント） ・Google が Crusoe のワイオミング州のデータセンター用地を取得 ・OpenAI API で外部への SIP 発信が全組織に開放 ・大学図書館に AI クローラーが殺到し、一般公開が危うい（125pt） ■ 空気感 「何ができるか」から「どう安全に作り、運用するか」へ。ベンダー製品のデータの扱いが不透明なことに、開発者が厳しくなっている。 ■ 参照リンク ・news.ycombinator.com/item?id… ・github.com/anthropics/claude… ・news.ycombinator.com/item?id… ・news.ycombinator.com/item?id… ・news.ycombinator.com/item?id… ・github.com/duanyytop/agents-…

ソフトウェアファクトリーにしたい理由は、CI／CDをしたい動機と全く同じなんだ。 コーディングやレビューがAIのおかげでビルドやデプロイのような単純作業に成り下がったとき、品質検証を強化してビルド・デプロイパイプラインのステップの一つにしたいと言うだけの話。至極当然の話だ。 そうなると、そのパイプラインもソフトウェアシステムなので、対象化され、ISUCONみたいなやり方でチューニング可能になる。これがハーネスエンジニアリング。 注意すべきなのは、2点。 まず一つはファクトリーで開発される対象プロダクトはベルトコンベアにのって通常は手に触れないものになるにせよ、ソフトウェアシステムとしてのファクトリーの開発やデバック、検証は少なくとも当面は手元端末なりで直接開発されることになり、ファクトリーの恩恵はそんなに受けない。ここは人間に律速される。当面は。 2つ目は、ソフトウェアファクトリーは全自動を意味していない。品質の自動検証を努力して強化すればするほど自動に近づくが、それをやらなければ人間がMRレビューを頑張って補う、2つの玉をヒモで結んだ振り子のような関係になる。ヒューマンインザループは残っている。判断と検証をフラグ変数のようにどっちに倒すかは判断になる。責任は逃れられない。そして、検証を頑張るとしたら、その部分は開発対象プロダクト固有になり、ここも手元端末での開発が残る第二の部分だ。 ようはCI/CDを時代に合わせて1段階ブラッシュアップしようぜ、と言うだけのこと。SaaSにする必要なんかもない。

こういうの、運の流れってあるのよね。確率1/2ではない。

■ 形式検証の大まかな歴史と流れ ・形式検証の主流は、もともとカリー・ハワードとは別の流れから来ている ・ただし最近、カリー・ハワード系（Leanなど）が勢いを増しているという変化はある ■ 大まかな歴史 ◆ 1960〜70年代：論理でプログラムを検証する流れ ・FloydやHoareが、プログラムに事前・事後条件を付けて正しさを示す方法（ホーア論理）を提案 ・LemmaScriptやDafnyの直接の祖先で、型ではなく論理式で考える ・Milnerの LCF：タクティクで証明を組み立てる方式。HOL系やIsabelleの祖先で、カリー・ハワードではない ・抽象解釈（Cousot夫妻、1977年）もこの時期 ◆ 同じ頃のカリー・ハワード系 ・de BruijnのAutomath（1960年代末）、Martin-Löfの型理論（1970年代） ・カリー・ハワード対応が広く知られるようになったのも1970年代以降 ・ただしこちらは主に論理学・数学基礎論側の関心で、実用的な検証の主流ではなかった ◆ 1980〜90年代：自動化の流れが本格化 ・モデル検査（Clarke、Emerson、Sifakis）。後にチューリング賞 ・Coq（構成の計算に基づく）が登場し、カリー・ハワード系の証明支援系が実用に近づく ・Pentiumの除算バグ（1994年）をきっかけに、ハードウェア業界でモデル検査や定理証明が本格導入される ◆ 2000〜2010年代：SMTの時代 ・SMTソルバー（Z3など）の性能向上で、Dafny、有界モデル検査、ドライバ検証などの自動化が一気に実用的になる ・同時期に、Coqによる検証済みコンパイラCompCert、IsabelleによるOSカーネルseL4といった、証明支援系の大型成果も出る ・AWSのTLA+活用、MetaのInferなど、産業での採用事例が増える ■ 最近の流れ ◆ Leanの台頭 ・Lean 4と数学ライブラリmathlibを中心に、数学者のコミュニティが大きく育った ・カリー・ハワード系の証明支援系が、初めて広い利用者層を持ち始めている ◆ AIとの組み合わせ ・従来、証明支援系の最大の弱点は「人が証明を書く手間」だった ・最近はAIがLeanの証明を書く研究が急速に進んでいる（数学オリンピックの問題をLeanで解いた例など） ・証明の正しさはカーネルが機械的に検査するので、AIが書いた証明でも信頼できる ・つまり「手間が高すぎる」という、カリー・ハワード系が主流になれなかった理由そのものが崩れつつある ■ 最初の投稿とのつながり ・LemmaScriptがDafnyとLeanの両方を変換先に持ち、「エージェントが迅速にイテレーションできる」と言っているのは、まさにこの流れ ・人には重すぎた証明作業を、AIに回させて、機械が検査する ・形式検証の費用対効果の計算が、AIで変わり始めている、というのが今の状況

オーケストレータと言うより手元の作業端末(個別的だから「ペット」)から、クラウドじゃなくていいから「家畜」開発マシンで開発を回したい。 自動化は元々スキルでやってる話で、自分以外の人もそれに乗せたい。「一人開発」ではなくしたい。そして記録したい。そして数値ベース、根拠ベースで改善したい。