From 3f3a26c53cf65958e835c9d2c9355a686cde54c6 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 19 May 2026 00:15:06 +1000 Subject: [PATCH] feat: filter MePo candidates to theorems and order output by iteration (#13750) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR refines MePo premise selection so that (1) candidates are restricted to theorems, matching the convention already used by `SineQuaNon` and `SymbolFrequency`, and (2) the result is ordered lexicographically by `(iteration, score)` rather than by score alone. Before the theorem filter, `mepoSelector` returned functions, recursors, and casts (e.g. `Int.add`, `Eq.ndrec`, `cast`, `proof_irrel`) alongside real premises. With it, those go away and the obvious lemmas — e.g. `Int.add_comm` for `a + b = b + a` — rank well above the remaining noise. The `(iteration, score)` ordering preserves the iteration priority of the original Meng–Paulson MePo: an iter-1 premise scoring 0.6 always ranks above an iter-2 premise scoring 1.0, since later iterations score against a strictly larger `relevant` set and a higher threshold, so their raw scores are not comparable. Thanks to Xavier Généreux for the report. Further tuning of the score function (the remaining problem: small generic theorems still score 1.0) is tracked in https://github.com/leanprover/lean4/issues/13749. Depends on https://github.com/leanprover/lean4/pull/13747. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.7 (1M context) --- src/Lean/LibrarySuggestions/MePo.lean | 12 ++++++--- .../elab/library_suggestions_mepo_order.lean | 27 ++++++++++--------- ...y_suggestions_mepo_order.lean.out.expected | 2 +- 3 files changed, 25 insertions(+), 16 deletions(-) diff --git a/src/Lean/LibrarySuggestions/MePo.lean b/src/Lean/LibrarySuggestions/MePo.lean index b719f59c59..27c499c29f 100644 --- a/src/Lean/LibrarySuggestions/MePo.lean +++ b/src/Lean/LibrarySuggestions/MePo.lean @@ -57,11 +57,16 @@ def mepo (initialRelevant : NameSet) (score : NameSet → NameSet → Float) (ac |>.partition fun (_, _, s) => p ≤ s if newAccepted.isEmpty then return accepted trace[mepo] m!"Accepted {newAccepted.map fun (n, _, s) => (n, s)}." + -- Scores from different iterations are not comparable: each iteration accepts + -- against a strictly larger `relevant` set and a higher threshold. We order the + -- output by `(iteration, score)`: earlier iterations always rank first, and + -- within an iteration we sort by descending score. + let newAccepted := newAccepted.qsort (fun (_, _, s₁) (_, _, s₂) => s₁ > s₂) accepted := newAccepted.foldl (fun acc (n, _, s) => acc.push { name := n, score := s }) accepted candidates := candidates'.map fun (n, c, _) => (n, c) relevant := newAccepted.foldl (fun acc (_, ns, _) => acc ++ ns) relevant p := p + (1 - p) / c - return accepted.qsort (fun a b => a.score > b.score) + return accepted end MePo @@ -76,7 +81,8 @@ public def mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4) pure <| frequencyScore (fun n => frequency.getD n 0) else pure <| unweightedScore - let accept := fun ci => return !isDeniedPremise env ci.name + let accept := fun ci => + return !isDeniedPremise env ci.name && wasOriginallyTheorem env ci.name let suggestions ← mepo constants score accept config.maxSuggestions p c - -- `mepo` already returns suggestions in score-descending order. + -- `mepo` already returns suggestions ordered by `(iteration, score)`. return suggestions.take config.maxSuggestions diff --git a/tests/elab/library_suggestions_mepo_order.lean b/tests/elab/library_suggestions_mepo_order.lean index 2e9b988e43..e83c1a0ef0 100644 --- a/tests/elab/library_suggestions_mepo_order.lean +++ b/tests/elab/library_suggestions_mepo_order.lean @@ -1,12 +1,13 @@ import Lean.LibrarySuggestions.MePo /-! -Regression test: the MePo premise selector must return suggestions in -score-descending order. +Regression test: the MePo premise selector filters candidates to theorems +(matching the convention already used by `SineQuaNon` and `SymbolFrequency`) +and finds the obvious lemma for an arithmetic equality goal. -A stale `.reverse` in `mepoSelector` (left over from before the selector was -made score-sorting) flipped the order to score-ascending, so `.take` returned -the lowest-scoring premises instead of the best ones. +Output is ordered by `(iteration, score)` rather than by score alone, so the +score sequence is not globally monotonic — a score jump signals an iteration +boundary. -/ open Lean Lean.Elab.Tactic Lean.LibrarySuggestions @@ -15,11 +16,13 @@ example (a b : Int) : a + b = b + a := by run_tac do let sel : Selector := mepoSelector (useRarity := false) let s ← sel (← getMainGoal) {} - let mut prev? : Option Float := none - for x in s do - if let some prev := prev? then - unless prev ≥ x.score do - throwError "MePo suggestions are not score-descending: \ - score {prev} precedes score {x.score}" - prev? := some x.score + let names := s.map (·.name) + if names.contains ``Eq.ndrec then + throwError "Eq.ndrec (a recursor) should be filtered out by the theorem-only \ + accept filter" + if names.contains ``Int.add then + throwError "Int.add (a function) should be filtered out by the theorem-only \ + accept filter" + unless names.contains ``Int.add_comm do + throwError "Int.add_comm should appear in the MePo suggestions for `a + b = b + a`" sorry diff --git a/tests/elab/library_suggestions_mepo_order.lean.out.expected b/tests/elab/library_suggestions_mepo_order.lean.out.expected index bbb4d1c5fb..aa752520f4 100644 --- a/tests/elab/library_suggestions_mepo_order.lean.out.expected +++ b/tests/elab/library_suggestions_mepo_order.lean.out.expected @@ -1 +1 @@ -library_suggestions_mepo_order.lean:14:0-14:7: warning: declaration uses `sorry` +library_suggestions_mepo_order.lean:15:0-15:7: warning: declaration uses `sorry`