LLMはRustコードを生成できる。形式的証明は全く別の問題だ。
大規模言語モデルは驚くほど質の高いRustコードを書くが、形式的証明を求めると、不変条件を幻覚で見つけ、どの検証器も受け付けない構文をでっち上げる。それらが実際に正しい部分、壊れる部分、それでも使う方法を解説する。
LLMはコンパイルできても通るRustを書ける。しかし、すべての可能な入力に対してコードが正しいことを保証する形式的証明を書くのは、今のところ信頼できない。…
アイデアとインサイト
AI ファースト開発、コーディングガードレール、使い捨て前提のアーキテクチャを探求します。
race conditionを待つのは最悪のテスト戦略だ
model checkingが、concurrency bugを発見するためにアプリを数日間実行することをどう凌駕するか、そして自分のコードにどう応用するか。
productionでrace conditionが出るのを待つのは、テストじゃない。勤勉のフリをした希望だ。 アプリを何週間も走らせ、metrics dashboardを見張っていても、2つのrequestがまさに同じcache eviction windowに突入したときだけ発火するconcurrency…
時相論理を学ばずにコードのモデル検査ができる
Kaniのような境界付きモデル検査器やAlloyのような関係モデルファインダーは、通常のアサーションと制約で性質を検証できる。活性の証明を諦める代わりに、学習曲線は週ではなく時間単位で測られる。
モデル検査器を使うために線形時相論理を学ぶ必要はない。Kani、CBMC、Alloyのようなツールは、通常のアサーションと関係制約で性質を検証できる。活性を証明する能力と引き換えに、学習曲線は週ではなく時間単位で測られ、ほとんどのソフトウェアのバグに対してそれは見合う交換だ。…
一行の証明も書かずに Rust コードの正しさを証明できるが、状態空間が代償となる
Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。
一行の証明も書かずに Rust コードの正しさを証明できる。その仕事をするのがモデル検査器であり、現時点で Rust に最も実用的なものは AWS が開発した Kani だ。通常の Rust の表明を書けばよい。Kani…
分散プロトコルは単体テストできないが、モデル検証はできる
分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。
分散プロトコルは単体テストできない。単体テストは1台のマシン上で1つのプロセスを決まった順序で実行する。分散プロトコルは5台のマシン上で10個のプロセスを、制御できない順序で実行する。この2つの現実の間に、バグが潜んでいる。…
環境間で `.env` ファイルをコピーすることは設定戦略ではない
インフラストラクチャチームが、環境間の差異を明示的かつ型安全にする文脈単位のDSLを使って、dev、staging、production間の設定を管理する方法。
staging環境は動作している。production環境は動作していない。両者のファイルの差分は400行で、その半数はもう誰も信じていないコメントだ。先月、誰かがstagingにを追加した。productionには誰も追加しなかった。アプリケーションはそれでも起動し、ハードコードされたデフォルト値を使用して、今や機能…
文法制約付きデコーディング: すべてのトークンでLLMに有効な構文を出力させる
LLMはトークンを確率的にサンプリングするため、構文を幻覚させる。文法制約付きデコーディングは各ステップで語彙をフィルタリングし、構文的妥当性を保つトークンのみを出力する。
LLMにJSONオブジェクトの生成を依頼すると、最終的に末尾カンマ、文字列内のエスケープされていない改行、あるいはquoted keyがあるべき場所にbare wordが出現する。これはモデルのバグではない。autoregressive…
英語からテーマへの翻訳は簡単だ。決定論的にすることが本当の課題だ。
英語の平易な記述からデザイントークンを生成できるが、その記述をスキーマ契約とスナップショットテストを伴う限界付きコンテキストDSLとして扱う場合に限る。
はい、英語でテーマを記述し、動作するデザインシステムを得ることはできる。ただし、その英語の記述はプロンプトではない。ソースファイルなのだ。そしてあらゆるソースファイルと同様、コンパイラ、型システム、テストが必要だ。…
Grammarファイルは捨てろ：DSLパーサーを普通のTypeScriptで書く
Bounded Context向けの小さなDSLに、パーサージェネレータは大げさすぎる。パーサーコンビネータなら、アプリケーションと同じ言語で動作するパーサーを、生成コードもビルドステップもなしに構築できる。
Yaccのgrammarファイルを開いて、なぜ言語を作るのに第二の言語を学ぶ必要があるのかと思ったことがあるなら、あなただけではない。パーサージェネレータは強力だが、bounded contextの中で自然に生まれる小さなDSLには、ほとんどの場合大げさすぎる。…
ランタイムの設定エラーは、あなたが許容した本番環境の障害である
スキーマ検証とビルド時チェックを用いて、アプリケーションがトラフィックを処理し始める前に設定ミスを捕捉する方法。
金曜日の夜、3時間経った頃、アプリケーションが を投げた。スタックトレースは設定オブジェクトの深くネストされたプロパティを指している。値は だ。誰かが の変更を本番環境にプッシュし、検証ロジックを更新しなかった。…