WingNews logo WingNews
top | item 46401423

(no title)

frotaur | 2 months ago

I don't know much about Lean, but I attended an introductory talk at some point and I was particularly bothered by these partial function definitions. The example was sqrt, which would give 0 on the negatives.

Now, of course, if you're careful with the definitions you use, there is no problem. But in the (increasingly relevant) context of automatic theorem proving with LLMs, this seems to defeat the 'groundtruthness' of Lean!

How do you make sure that the LLM doesn't reward hack a proof using these workarounds?

discuss

order

akoboldfrying|2 months ago

I don't understand why they would make such footgun functions either, especially because (IIUC, and I probably don't) in a way the whole point of Lean's dependent type system is to be able to express arbitrary constraints on the inputs of these functions so that they can be total -- e.g., to be able to define a subtraction function on the nonnegative integers that takes one integer and one {integer that is less than or equal to the first integer}. And to even call this function, you (or perhaps Lean itself) would need to first prove that its second argument is less than or equal to its first.

Smaug123|2 months ago

You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.)

The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives!

The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.

markusde|2 months ago

This is a topic of contention in formalized math with no universal right answer. Some libraries go heavy on the dependent types, and some like mathlib try to avoid them. I do math in both Rocq and Lean and I find I like the latter style a lot more for my work for a couple reasons:

- Fewer side conditions: Setting a / 0 = 0 means that some laws hold even when a denominator is 0, and so you don't need to prove the denominator is nonzero. This is super nice when the denominator is horrible. I heard once that if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions (though I didn't track down this paper to find out for sure).

- Some of the wacky junk arithmetic values, especially as it relates to extended reals, do show up in measure theory. Point being: "junk arithmetic" is a different mathematical theory than normal math, but it's no less legitimate, and is closely related.

- Definition with Hilbert's epsilon operator. If I want to define a function that takes eg. a measurable set S as an argument, I could do the dependent types way

def MyDef (S) (H : measurable S) := /-- real definition -/

but then I need to write all of my theorems in terms of (MyDef S H) and this can cause annoying unification problems (moreso in Rocq than in Lean, assuming H is a Prop). Alternatively, I could use junk math

def MyDef' (S) := if (choose (H : measurable S)) then /-- real definition -/ else /-- junk -/

I can prove (MyDef' S = MyDef S H) when I have access to (H : measurable S). And the property H here can be be really complex, convergence properties, existence properties, etc. It's nice to avoid trucking them around everywhere.

nextaccountic|2 months ago

If your language isn't ergonomic then people will not use it (or use it less). Maybe another theorem prover will arise that makes "correct" definitions more ergonomic

Note that the same thing happens in Rust. Rather than putting trait bounds in structs (like struct Aa<T: Something> { .. }, people are encouraged to make the structs more generic (struct Aa<T> { .. }) and put restrictions on impls instead (impl<T: Something> Aa<T> { .. }). The rationale being that this is more ergonomic because it doesn't require you to repeat bounds in places you don't need them, and if every impl requires a Something bound, you will need the bound to make anything with this type (doubly so if the fields of Aa are private and so you need to build one using a method with T: Something)

sebzim4500|2 months ago

>How do you make sure that the LLM doesn't reward hack a proof using these workarounds?

I'm not sure what you mean exactly? There is no soundness issue here, the fact that `sqrt -1` is defined to be 0 does not have any impact on what statements about `sqrt x` can be proved when `x` is positive.

It just means that if you are working on an intermediate step of a proof and you need the result that `sqrt y >= 0` you don't need to provide a proof that `y >= 0`. If you wanted an intermediate result that `(sqrt y) * 2 = y` then you would still need to provide a proof that `y >= 0`, though.

munchler|2 months ago

If sqrt -1 = 0, then (by squaring both sides) -1 = 0, which is clearly unsound.