Leanで業務ルールの整合性を機械検証するアプローチは胸熱。確率的なLLMを決定論的に制御するハックとして面白すぎる
仕様を Lean の論理式に翻訳するのは LLM に任せる。その翻訳の正確性は誰が保証するの？OpenAI の数学の論文を見ればわかるように、LLM は普通にその翻訳を間違えるよ。やろうとしている方向性は正しい
書いてあることは面白いけど、イメージがわかない。
ブコメの「やろうとしている方向性は正しい」ってコメント、前段で「正確性は誰が保証するの？」って言ってるのと比較すると変な事に気付いている？この人が記事の著者の指導者的な立場か何かならまだ理解はできるが
"公開します（2026-11-5 時点では未公開）。"かっこが混在してるのと、日付のゼロ埋めしてない。内容は興味深そう。
定理証明ガードレールで AI エージェントに業務ルールを守らせる - freee Developers Hub
Leanで業務ルールの整合性を機械検証するアプローチは胸熱。確率的なLLMを決定論的に制御するハックとして面白すぎる
仕様を Lean の論理式に翻訳するのは LLM に任せる。その翻訳の正確性は誰が保証するの？OpenAI の数学の論文を見ればわかるように、LLM は普通にその翻訳を間違えるよ。やろうとしている方向性は正しい
書いてあることは面白いけど、イメージがわかない。
ブコメの「やろうとしている方向性は正しい」ってコメント、前段で「正確性は誰が保証するの？」って言ってるのと比較すると変な事に気付いている？この人が記事の著者の指導者的な立場か何かならまだ理解はできるが
"公開します（2026-11-5 時点では未公開）。"かっこが混在してるのと、日付のゼロ埋めしてない。内容は興味深そう。