12 posts
Seerはtrace tree、関連付けられたエラー、プロファイリングデータを取り込んで分散問題を診断する。実際にどう機能するか、どこで輝き、どこでまだ人間の助けを必要とするかを解説する。
フロントエンドが500エラーを投げる。stack traceはReactコンポーネントを指す。本当の問題は3つ先のサービスにあり、リークしているバックグラウンドジョブによって使い果たされたデータベース接続プールにある。 trace…
大規模言語モデルはtest oracleの発見において悪くないブレインストーミングパートナーだが、性質を幻覚し、ドメイン制約を見落とす。それらを、怪しいテストをリリースすることなく使う方法を解説する。
事前に正しい出力がわからない関数をテストする必要がある。経路最適化器、感情分類器、物理シミュレーション。Metamorphic testingについて読んだ：入力と出力の間に成り立つはずのrelationを見つけ、正確な値の代わりにそれらのrelationをテストするのだ。…
大規模言語モデルは静的解析の偽陽性の選別に役立つが、抽象解釈のようにプログラムの意味論を理解しているわけではない。両者を組み合わせる方法を解説する。
あなたの静的解析ツールは金曜日の午後に847件の警告を出力した。統計的には、そのうち5%から15%が実際のバグだ。残りは偽陽性だ：生成コード内のデッドストア、ツールには怪しく見えるが人間には明らかなヌルチェック、関係のないハッシュ関数内の整数オーバーフロー。 手作業で仕分けするのは精神的に exhausting…
クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。
クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。…
30日間、LLMにコードを依頼する前に設計の説明を書き続けた。その結果は、私のrubber-duckingに対する考え方を変えた。
ほとんどの開発者はLLMを逆さまに使っている。5語ほどで欲しいものを説明し、200行のコードを受け取り、次の1時間はモデルが行った仮定をデバッグすることに費やす。…
LLMの対話には意図、却下された代替案、そして動作するコードが含まれています。これこそがドキュメントであるべきものです。以下に、短寿命なチャットをナラティブを失うことなく、永続的で検索可能なドキュメントに変換する方法を説明します。
あなたはClaudeと45分かけてリトライ回路を設計しました。失敗モードを説明し、カスケード圧力を隠してしまうため指数関数的バックオフを却下し、jitter付きtoken-bucket rate limitingで決着し、動作する実装を生成しました。説明は明快で、推論は妥当であり、コードは実際にテストをパスしました。…
フェイガン査読は250行をレビューするのに4〜6人と2時間を要する。大規模言語モデルは準備作業とチェックリストの遵守を担うことでそのコストを削減できるが、最も高価な欠陥を見つける人間の役割は代替できない。
本格的なフェイガン査読には、進行役、読み手、2〜4人の査読者、そして著者が必要だ。チームは1時間あたり125行のペースで、おおむね250行のコードを2時間かけてレビューする。小さな変更でも、8〜12人時の工数がかかるのだ。…
大規模言語モデルは驚くほど質の高いRustコードを書くが、形式的証明を求めると、不変条件を幻覚で見つけ、どの検証器も受け付けない構文をでっち上げる。それらが実際に正しい部分、壊れる部分、それでも使う方法を解説する。
LLMはコンパイルできても通るRustを書ける。しかし、すべての可能な入力に対してコードが正しいことを保証する形式的証明を書くのは、今のところ信頼できない。…
LLMはトークンを確率的にサンプリングするため、構文を幻覚させる。文法制約付きデコーディングは各ステップで語彙をフィルタリングし、構文的妥当性を保つトークンのみを出力する。
LLMにJSONオブジェクトの生成を依頼すると、最終的に末尾カンマ、文字列内のエスケープされていない改行、あるいはquoted keyがあるべき場所にbare wordが出現する。これはモデルのバグではない。autoregressive…
英語の平易な記述からデザイントークンを生成できるが、その記述をスキーマ契約とスナップショットテストを伴う限界付きコンテキストDSLとして扱う場合に限る。
はい、英語でテーマを記述し、動作するデザインシステムを得ることはできる。ただし、その英語の記述はプロンプトではない。ソースファイルなのだ。そしてあらゆるソースファイルと同様、コンパイラ、型システム、テストが必要だ。…
複数のLLMを並列実行すると、どの単一モデルも見逃すエラーを捕捉できる。実際に機能する不一致解決システムの構築方法を解説する。
GPT-4oにプロンプトを投げる。confidence 0.97のJSON blobが返ってくる。同じプロンプトをClaude 3.5 Sonnetに投げる。異なるJSON…
LLMによるN-version programmingに複数のモデルは不要。プロンプト、ペルソナ、推論の制約を変えることで、単一モデルから多様で正しい実装を引き出せる。
N-version programmingでは、多様性は異なる作成者から生まれるものだと想定されている。LLMの場合、それは異なるモデル、異なるプロバイダー、あるいは異なる学習実行を意味する。だがこの前提は間違っている。同じモデルから、問う内容ではなく問い方を変えることで、意味のある多様性を得られる。…