Fast but only "probably correct" functions

[JohnAAbbott]

How should OSCAR offer "probably correct" computations?

Q: Why? A: Because sometimes a "probably correct" result can be obtained much faster. For example

n = factorial(ZZ(379))-1;
@time is_probable_prime(n)  # about  0.02s
@time is_prime(n)           # about 26s  (approx 1300 times slower)

Note that is_probable_prime has one-sided uncertainty: if it returns false then that is surely correct; but if it returns true then that may be incorrect. TBH the documentation could be clearer!

Q: What does "probably correct" mean here? A: That's tricky to quantify. It is likely also tricky to document precisely: e.g. the documentation for is_probable_prime states No counterexamples are known to this test, but it is conjectured that infinitely many exist (and I believe that considerable effort has been expended, by experts in the matter, in trying to construct a counter-example).

Q: Is the "probability of correctness" user controllable? A: Not with is_probable_prime in its current form. Other "probably correct" functions could offer such control (though it is likely impossible to describe accurately how precise the control is)

Q: What happens if the result is wrong? A: It is the caller's responsibility to cater for this eventuality. For instance, the main computation may proceed using the wrong value, and some higher level check can detect that a higher-level value is "impossible" (leading to a recomputation, or maybe returning "failure").

Q: Which other functions might have "probably correct" versions? A: I expect there are many; since I've been looking at linear algebra: rank(...) one-sided: a modular approach will give a lower bound det(...) nature of an incorrect result depends on which internal algorithm was used to obtain the value returned leading_ideal (via groebner_basis) one-sided, but it is a little involved to describe precisely how...

SUMMARY

Sometimes "probably correct" methods can lead to significant speed-ups. Assuming we accept the need for such functions, how can the user give OSCAR permission to use them (rather than the slower, guaranteed versions)? Moreover, the permission could/should include a "verification level" to control the "probability of correctness". This permission may need to be passed down to lower level functions (semi-transparently?). A conceptually simple approach would be to have some global (ugh!) settings; but to make direct interactive calls easier, there should also be the possibility of enabling "probable correctness" without changing global settings (e.g. via optional parameters, or alternative function names).

MY CURRENT THOUGHTS

Currently I do not like the idea of using separate function names to distinguish normal and probably-correct functions (except perhaps for is_prime and is_probable_prime).

My current preference would be to use optional parameters (kwargs) to indicate that a "probably correct" result may be returned, and also to indicate the verification level. For instance, we could have

  r = rank(M)  # guaranteed correct
  r = rank(M; verification_level=3)  # likely faster, possibly wrong

My intention is that the kwarg would have the same name in all functions offering a "probably correct" variant, so that the user need to memorize less.

CERTIFICATION

Here is my opinion about "certification" (or "certified result"). I prefer to use "certification" or "certified result" to mean that the result is accompanied by a separate data-structure which is the certificate for that result. For instance a prime number can be certified by a (recursive) Pratt certificate [see Wikipedia]: a smallish data-structure which permits whoever has it to verify that the number is indeed prime by performing relately few, relatively simple computations. In contrast, a verified result is not accompanied by a separate data-structure -- one must trust whoever or whatever computed the result!

[HechtiDerLachs]

I think @ederc and @RafaelDavidMohr mentioned some computations of Groebner bases modulo primes and probably correct reconstructions of related Groebner bases over QQ from that. This sounds related in the sense that they were also wondering about ways to communicate this to the user.

[JohnAAbbott]

Thanks @HechtiDerLachs Yes, I think it is closely related. Indeed a GB computation normally occurs at a low level, and the user may be quite unaware that a GB is needed at all. i think it would be rather cumbersome for (almost?) every function to have an optional argument about "probably correct" computation, just so that the option could be passed down to lower levels where it may be needed. The obvious alternative seems to be a global setting... which feels unclean (and could be tricky in a multi-threaded computation). I look forward to feedback from/discussions with @ederc and/or @RafaelDavidMohr

[YueRen]

(As mentioned in the Oscar meeting) I think we need to distinguish between different kinds of "probably correct":

a. Algorithms for which no known wrong example exists (e.g., @JohnAAbbott 's example) b. Algorithms which theoretically work with probability 1 (e.g., relying on a random choice being generic) c. Algorithms which theoretically work with probability 0<p<1

[thofma]

b. Algorithms which theoretically work with probability 1 (e.g., relying on a random choice being generic)

Since we don't (and can't) take random elements from infinite fields (but only in some finite subset), I don't think we could rigorously claim that our implementation works with probability 1 for any input. I would argue that this also falls under category c). (I am alluding to an algebro-geometric algorithm. If you were thinking about some other "generic" situation, please correct me.)

[fieker]

there is the all important case d. Algorithms in categories a-c, where the result of the total computation can be verified, possibly not an individual step

[JohnAAbbott]

I am not sure of the practical benefits of making the distinctions @YueRen proposes. As @thofma points out, we do not really compute with truly random values, just pseudo-random values from some finite set. Regardless of theoretical probabilities, we must cater for a wrong result (or at least warn the user) -- in a sense, the probability does not say much about a single computation! I wonder what happens if someone discovers a counter-example to a class (a) algorithm, but the counter-example happens to be an illegal number [yes, there is a Wikipedia page about these!]

[JohnAAbbott]

I forgot to mention earlier that several functions offer an optional boolean kwarg check. This is used to check that the arguments supplied to the call are "sane" (e.g. compatible, within range, etc.). It does not signify that a "probably correct" result is to be fully checked for correctness. My intention was to propose a similar optional kwarg name (in CoCoALib we called it verification_level) for specifying how carefully "probably correct" results should be verified; it also needs an "infinite value" to indicate that an absolute verification must be conducted (regardless of computational cost). The default value would be either "infinite" or maybe obtained from the global settings, I presume.

[fieker]

On Mon, Dec 18, 2023 at 09:08:53AM -0800, JohnAAbbott wrote:

I forgot to mention earlier that several functions offer an optional boolean kwarg check. This is used to check that the arguments supplied to the call are "sane" (e.g. compatible, within range, etc.). It does not signify that a "probably correct" result is to be fully checked for correctness. My intention was to propose a similar optional kwarg name (in CoCoALib we called it verification_level) for specifying how carefully "probably correct" results should be verified; it also needs an "infinite value" to indicate that an absolute verification must be conducted (regardless of computational cost). The default value would be either "infinite" or maybe obtained from the global settings, I presume.

I think this is partly iverthinking and mostly the wrong way round

• by default, all output should be mathematically correct, unless explicitly disabled by name or argument
• verifcation level and kwargs are always critical as in most interesting applications I do not interact with the unverified function directly, e.g. I am working with ModuleFP's to compute cohomology. This will involve an unknown number of calls to GB or various linear algebra functions, so passing a rich family of KW args to the cohomology to affect a functions 5 levels down does not sould good. In particular as I do not want to add this to every function calling s.th. that will eventually call GB...
• I could see some global preferences (no verification, accept 0.001% error or however
• the low-level functions need some for of orverride in cases where I can verify a large block of computations, but not every step.
• I was bitten by global preferences (check = false and similar) before... -- Reply to this email directly or view it on GitHub: https://github.com/oscar-system/Oscar.jl/issues/3110#issuecomment-1861083319 You are receiving this because you commented.

Message ID: @.***>

[JohnAAbbott]

A quick response:

• I'd like to know more about the unhappy experience @fieker had with global settings (to help guide us toward a better design)
• I quite agree with @fieker that the default behaviour should be guaranteed correct results (within the limits practical imposed by reality, hardware, etc.).
• assuming we do offer an option for "likely correct" faster computation, I think it could make sense to offer several levels of verification: e.g. low, medium, high, and absolute/fully-guaranteed.... perhaps even without "medium"?
• in most cases we cannot determine a good estimate of the probability of a wrong result (because we would also need a probability distribution for the inputs)
• [Perfect is the enemy of good] I hope soon to make a "good" concrete proposal which we can discuss, and perhaps implement, bearing in mind that it may need to be replaced by something better.

[fieker]

On Wed, Dec 20, 2023 at 06:03:47AM -0800, JohnAAbbott wrote:

A quick response:

• I'd like to know more about the unhappy experience @fieker had with global settings (to help guide us toward a better design) That was global option to bypass the irreducibility check of the polynomial in creating a number field. A particular person fought for it, stating that
• it is costly (for extension of number fields)(was true)
• anyway: all polys are irreducible He came back a couple of months later with a weird error do to zero divisors due to a bad poly He was cured afterwards
• I quite agree with @fieker that the default behaviour should be guaranteed correct results (within the limits practical imposed by reality, hardware, etc.).
• assuming we do offer an option for "likely correct" faster computation, I think it could make sense to offer several levels of verification: e.g. low, medium, high, and absolute/fully-guaranteed.... perhaps even without "medium"?
• in most cases we cannot determine a good estimate of the probability of a wrong result (because we would also need a probability distribution for the inputs)
• [Perfect is the enemy of good] I hope soon to make a "good" concrete proposal which we can discuss, and perhaps implement, bearing in mind that it may need to be replaced by something better.

At this point, I think the proposal is more limited

• global option to allow modular methods with "proof by stabilization" (possibly taking level + 3 primes)
• global option for GRH

possibly a framework that can tell you afterwards if non-verified results were used by recording calls (and backtraces) to the bottom functions that do (or not do) the verification. (So a user can check if (s)he was affected - and why and where)(this is also more safe than hoping that the documentation stays correct and would mention this)

Functions with "probable" or similar in the name will not be switched to verified mode.

A function/ situation where verification is always cheap can of course ignore this (and then also not record)

That does not preclude anyone to add more and more complicated options to specific calls (Groebner with deg bound, ...), but at this point, I don't see any more situations where a user could make top-level choices that are vaguely meaningful.

-- Reply to this email directly or view it on GitHub: https://github.com/oscar-system/Oscar.jl/issues/3110#issuecomment-1864529079 You are receiving this because you were mentioned.

Message ID: @.***>

[JohnAAbbott]

Here is an example implementation (with emphasis on simplicity). First there is a GlobalSettings module which exports two functions for setting and getting the global setting relating to verification level; then there is an example of a function designed to use the setting; and finally some example calls.

module GlobalSettings

export set_verification_level;
export get_verification_level;

# Permitted values:  :LOW, :HIGH,  :GUARANTEED
global const verification_level = Ref{Symbol}(:GUARANTEED)

function set_verification_level(s::Symbol)
  if  s != :LOW  &&  s != :HIGH  &&  s != :GUARANTEED
    error("Permitted verification_levels are :LOW, :HIGH, :GUARANTEED")
  end
  prev = verification_level[]
  global verification_level[] = s
  return prev
end

function get_verification_level()
  return verification_level[]
end

end #module

The example function has a kwarg which takes its default value from the global setting, but this may be overwritten in any specific call. The function prints out a message to highlight which branch it took:

using .GlobalSettings;

function IsPrime(n; verification_level=get_verification_level())
  if verification_level == :GUARANTEED
    println("IsPrime: guaranteed test");
    return is_prime(n)
  else
    println("IsPrime: probable test");
    return is_probable_prime(n)
  end
end

And finally some examples how to call this function:

julia> IsPrime(ZZ(999))
IsPrime: guaranteed test
false

julia> IsPrime(ZZ(999); verification_level=:LOW)
IsPrime: probable test
false

julia> set_verification_level(:HIGH)
:GUARANTEED

julia> IsPrime(ZZ(999))
IsPrime: probable test
false

julia> IsPrime(ZZ(999); verification_level=:LOW)
IsPrime: probable test
false

julia> IsPrime(ZZ(999); verification_level=:GUARANTEED)
IsPrime: guaranteed test
false

We see that:

• by default the behaviour is :GUARANTEED
• each individual call may optionally have its own verification level (which does not alter the global setting)
• the global setting can easily be changed (it also reports the previous setting... might be confusing?)
• without the optional kwarg the behaviour is determined by the global setting
• I think this ought to scale easily

[thofma]

I understand why this could be useful in general, but I have some reservations about this.

• Exposing anything like "verification_level" looks very bad IMHO, even if the default is "guaranteed". Makes me wonder whether the developers take mathematical rigour serious.
• Why is there more than one verification level? Anything that goes beyond yes/no will be too complex and inconsistent.
• It is a global option.
• It is intransparent to what actually is effected.
• Is there a problem with doing if verification_level[] = :LOW; return rand(Bool); end if;?
• If think there are many places, where an is_prime(p) call needs to be rigorous and anything non-prime will produce errors/segmentation faults? Is there a way to guard against this? Is this intended?

[fieker]

I'd just add, at this point, two or three options: Grh Modular algo (mainly groeber, but maybe mpoly gcd and friends) Schreier Sims in group theory

This affects only few basic functions and untold indirectly.

If set, I'd record the stack trace of the calls to allow a user to see if this was used

I would not mess with is_prime at this point

On Wed, 20 Dec 2023, 17:02 Tommy Hofmann, @.***> wrote:

I understand why this could be useful in general, but I have some reservations about this.

• Exposing anything like "verification_level" looks very bad IMHO, even if the default is "guaranteed". Makes me wonder whether the developers take mathematical rigour serious.
• Why is there more than one verification level? Anything that goes beyond yes/no will be too complex and inconsistent.
• It is a global option.
• It is intransparent to what actually is effected.
• Is there a problem with doing if verification_level[] = :LOW; return rand(Bool); end if;?
• If think there are many places, where an is_prime(p) call needs to be rigorous and anything non-prime will produce errors/segmentation faults? Is there a way to guard against this? Is this intended?

— Reply to this email directly, view it on GitHub https://github.com/oscar-system/Oscar.jl/issues/3110#issuecomment-1864741259, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA36CV376FOMTZGUUFCP3HLYKMDZ5AVCNFSM6AAAAABAWPWTECVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRUG42DCMRVHE . You are receiving this because you were mentioned.Message ID: @.***>

[JohnAAbbott]

Apologies for the delay: somehow I did not notice your comments from around 3 weeks ago. The IsPrime example was just intended as an illustrative example, showing how verification_level could be used; it was not a proposal to mess with is_prime.

The idea of @fieker to record when/whether "probable" results were computed seems to be important -- this should also resolve @thofma doubts about lack of transparency. Right now I do not have a sane proposal for how this might be achieved. We could try recording stack-traces, but I wonder how large the record might become. I need to think about this... but there are other more urgent matters for me at the moment.

The last point of @thofma is interesting. It could readily be solved in C++ using RAII; not sure how to model this in Julia (perhaps via a macro?) I share @thofma doubt about using globals unless absolutely necessary; in this case i do believe it is necessary, and even "desirable"... of course fiddling with globals in a multi-threaded setting is asking for trouble. I can see the case for just having a 2-state setting (rather than 3-state as in my example), especially since we cannot make any meaningful claims about probabilities without knowing the input distribution.

Regarding mathematical rigour: the point is that it may be infeasible to obtain a fully rigorous result (within a reasonable time-frame), but it may be possible to obtain a "probably correct" (?or "possibly wrong"?) result tolerably quickly. This may be perfectly acceptable in some application areas outside pure mathematics.

[JohnAAbbott]

I suggest we let this issue sleep until March 2024, when the important deadlines are past.