LLMに「本物のインタプリタ」と一致する証明を書かせ、検証済みソフトウェアの土台を作る

Ship Your Interpreter

Basisの研究者らは、小さな言語WHILEの形式的意味論をLLMに書かせ、その規則が実際のCインタプリタをRISC-Vにコンパイルしたバイナリの挙動と全プログラムで一致することをLeanで証明した。テストでは見逃す59文字の関数名による文字列化の差異も、証明の過程で発見・修正された。検証のボトルネックは定理証明から仕様記述へ移りつつある。