Mutating Lean proofs looking for issues

A team at the Noetic X Nebius One Day Hackathon, including Jacky Chen and Claude Open 5.5, built a Python tool that randomly mutates Lean proof source and re-runs the Lean verifier to flag proofs that still validate after changes, a mutation-testing approach to catching bugs in LLM-generated formal proofs. Working within a roughly 5-hour window before a 16:00 deadline, the team added 13 mutants to a small test case that continued to verify, though the author said he has no idea how representative that count is. The effort follows reports that LLM-generated Lean proof programs contain bugs, raising the question of how to check proofs that can run to many thousands of lines.

Home https://shape-of-code.com/ Uncategorized https://shape-of-code.com/category/uncategorized/ Mutating Lean proofs looking for issues Mutating Lean proofs looking for issues A common technique used to bolster confidence that LLM derived proofs of mathematical statements are correct is to supply an associated machine checkable form of the proof written in the Lean language <https://en.wikipedia.org/wiki/Lean proof assistant , i.e., a program that can be interpreted by the Lean proof assistant. Mathematicians have discovered, shock horror, that LLM generated proof-programs contain bugs https://www.lesswrong.com/posts/rhAPh3YzhPoBNpgHg/lies-damned-lies-and-proofs-formal-methods-are-not-slopless . Given the current trajectory of mathematical work, perhaps it should now be considered a field of software development developers have long known that LLM generated code contains bugs . Coding agents can generate programs that appear to work, while containing code having undesirable consequences e.g., security issues and surprising hallucinations, and it is only to be expected the generated Lean programs will contain these features. What can be done to check Lean programs for coding mistakes? The traditional approach to finding issues with source is to read it. Lean proofs can contain many thousands of lines, and depending on your background be more/less easy to read than most programming languages. Reading Lean is the expensive, time-consuming, high value option. The source of an example Lean theorem is below: | theorem core cycle t : Nat → Nat h₀ : t 0 = 7 h₁ : t 1 = 4 h₂ : t 2 = 9 hp : ∀ n, t n + 3 = t n : t 2019 + t 2020 = 11 := by have step : ∀ k, t 3 k = t 0 ∧ t 3 k + 1 = t 1 := by intro k induction k with | zero = simp | succ k ih = have e1 : 3 k + 1 = 3 k + 3 := by omega have e2 : 3 k + 1 + 1 = 3 k + 1 + 3 := by omega constructor · rw e1, hp exact ih.1 · rw e2, hp exact ih.2 have h2019 : 2019 = 3 673 := by decide have h2020 : 2020 = 3 673 + 1 := by decide have a : t 2019 = 7 := by rw h2019, step 673 .1, h₀ have b : t 2020 = 4 := by rw h2020, step 673 .2, h₁ rw a, b | One automated process that might be used to find suspect usage is mutation testing https://en.wikipedia.org/wiki/Mutation testing which was once consigned to the grave https://shape-of-code.com/2021/09/12/mutation-testing-its-days-in-the-limelight-are-over/ . The idea is to mutate e.g., make a non-trivial change to the Lean source, and then check whether the mutated proof still validates. The assumption is that proof source that can be substantially mutated without changing its verification status is suspect. Yesterday I took part in the Noetic X Nebius One Day Hackathon https://luma.com/qa1ds94p , and Team MutationHacker Jacky Chen, yours truly, and Claude Open 5.5 worked towards creating a tool to automatically mutate and check Lean proofs. Our grandiose plans were undermined by a submission deadline of 16:00 we had around 5-hours . An agent based system that learned from past successful mutants was replaced by the MVP of a python program running on a laptop picking mutations at random and running the Lean verifier on the laptop not fast . Successful mutants i.e., no change to verification state accumulated in the proof source. How many mutants can a Lean proof of a theorem accumulate, and still verify, before it’s considered suspect or problematic? The mutation tool managed to add 13 mutants to the small test case that we used. I have no idea how representative this is. The mutant generator specification lists of constructs not to use, e.g., changes that had no effect on the rest of the proof. Perhaps the Lean source contains dead code, or bounding conditions are overly wide https://claude.ai/artifact/9Q3r2Vc7NW3gBTvnvAva9t , e.g., can be replaced by . lean-bugs https://github.com/Derek-Jones/lean-bugs is available on GitHub. Ideally many thousands of mutants are tried, but the time taken to verify a short proof is several seconds, which will require lots of cpu time to check thousands of mutants. There don’t appear to be any benchmarks comparing Lean performance for various proof sizes the timings cited https://lean-lang.org/doc/reference/latest/releases/v4.35.0/ don’t appear to connect to what I am after . OpenAI’s recent Navier-Stokes solution came with 470K LOC of Lean which has been verified by independent researchers in times https://www.kimi.ai/share/1a1750a2-d992-840f-8000-0000c19a58ca ranging from 212 seconds to 15 minutes. The smaller precursor theorems and lemmas could be mutated as stand-alone items, to reduce overheads.