LLMはコードの正しさを証明できないが、証明のための定型作業は書ける
クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。
クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。…
2 posts
クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。
クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。…
大規模言語モデルは驚くほど質の高いRustコードを書くが、形式的証明を求めると、不変条件を幻覚で見つけ、どの検証器も受け付けない構文をでっち上げる。それらが実際に正しい部分、壊れる部分、それでも使う方法を解説する。
LLMはコンパイルできても通るRustを書ける。しかし、すべての可能な入力に対してコードが正しいことを保証する形式的証明を書くのは、今のところ信頼できない。…