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