Trivet combines LLMs and Lean to validate LLVM compiler transformations