Home>
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, 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. 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 (which was once consigned to the grave). 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, 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, e.g., can be replaced by .
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 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 ranging from 212 seconds to 15 minutes. The smaller precursor theorems and lemmas could be mutated as stand-alone items, to reduce overheads.