定理証明ガードレールで AI エージェントに業務ルールを守らせる - freee Developers Hub

仕様を Lean の論理式に翻訳するのは LLM に任せる。その翻訳の正確性は誰が保証するの？OpenAI の数学の論文を見ればわかるように、LLM は普通にその翻訳を間違えるよ。やろうとしている方向性は正しい