AI most hated by formal verification (Was: Fuzzy Testing is your Swiss Knife)

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.prolog
Subject	AI most hated by formal verification (Was: Fuzzy Testing is your Swiss Knife)
Date	2025-11-26 17:02 +0100
Message-ID	<10g78at$l82g$1@solani.org> (permalink)
References	<106p08a$3b6se$1@solani.org> <107l9om$1hci$1@solani.org> <107oa19$3c0p$1@solani.org> <107oacc$3c8m$2@solani.org>

Show all headers | View raw

Hi,

So Boris the Loris and Nazi Retartd Julio are
not alone. There is now a mobilization of the
kind of rage against the machine,

fighting for methods without randomness. Its
almost like  Albert Einstein ascendet from his
grave and is now preaching,

"God does not play dice"

So how it started:

PIVOT was an interactive program verifier designed by
L. Peter Deutsch for his Ph.D. dissertation.
Posted here by permission of L. Peter Deutsch.
https://softwarepreservation.computerhistory.org/pivot/

How its going:

Formal Methods: Whence and Whither?
The text also highlights the evolving role of formal
methods amidst technological advancements, such as
AI, and explores educational and standardization issues
related to their adoption.
https://de.slideshare.net/slideshow/formal-methods-whence-and-whither-keynote/273708245

Can the Don Quijotes win, and fight the AI windmills?

LoL

Bye

Mild Shock schrieb:
> 
>  > I see it as fuzzy testing of the community.
>  > It is certainly beneficial if used correctly
> 
> Fuzzy Testing goes also by the name QuickCheck.
> You can use Fuzzy Testing also for benchmarking.
> Mathematically it uses the Law of Large Numbers:
> 
> Law of large numbers
> https://en.wikipedia.org/wiki/Law_of_large_numbers
> 
> Means you even don’t need a random generator
> with a programmable seed, so that a comparison
> involves the exact same random number sequences.
> 
> Just assume that your results have a variation σ.
> Then most likely the overall variation decreases
> proportionally to the number n of experiments,
> i.e. gets washed out:
> 
> VAR(X) = σ^2 / n
> 
> A third use case of Fuzzy Testing is to determine
> frequentist probabilities . Like when I determined
> that 25% of a variant of @kuniaki.mukai compare/3
> triples are not transitive.
> 
> 
> Mild Shock schrieb:
>> You can use Fuzzy Testing also for
>> benchmarking. Not only to find faults.
>> For example when I benchmark mercio/3 via
>> fuzzy/1, I find it doesn’t fare extremly bad:
>>
>> ?- time((between(1,100,_), mercio, fail; true)).
>> % 4,386,933 inferences, 0.375 CPU in 0.376 seconds (100% CPU, 11698488 
>> Lips)
>> true.
>>
>> And I am not using some of the optimization
>> that @kuniaki.mukai posted elsewhere and that
>> I posted 06.08.2025 on comp.lang.prolog. Fact is,
>> it only ca. 20% slower than SWI-Prologs compare/3:
>>
>> ?- time((between(1,100,_), swi, fail; true)).
>> % 3,786,880 inferences, 0.312 CPU in 0.325 seconds (96% CPU, 12118016 
>> Lips)
>> true.
>>
>> The test harness was:
>>
>> swi :-
>>      between(1,1000,_),
>>      fuzzy(X), fuzzy(Y),
>>      swi(_, X, Y), fail; true.
>>
>> mercio :-
>>      between(1,1000,_),
>>      fuzzy(X), fuzzy(Y),
>>      mercio(_, X, Y), fail; true.
>>
>> The difficulty was to find a 100% Prolog compare/3
>> that corresponds to SWI-Prolog. But you find a
>> fresh implementation in 100% Prolog using a Union
>> Find structure in the below:
>>
>> % swi(-Atom, +Term, +Term)
>> swi(C, X, Y) :-
>>     swi(X, Y, C, [], _).
>>
>> % swi( -Atom, +Term, +Term,+List, -List)
>> swi(C, X, Y, L, R) :- compound(X), compound(Y), !,
>>     sys_union_find(X, L, Z),
>>     sys_union_find(Y, L, T),
>>     swi_found(C, Z, T, L, R).
>> swi(X, Y, C, L, L) :- compare(C, X, Y).
>>
>> % swi_found(-Atom, +Term, +Term, +List, -List)
>> swi_found(C, X, Y, L, L) :-
>>     same_term(X, Y), !, C = (=).
>> swi_found(C, X, Y, _, _) :-
>>     functor(X, F, N),
>>     functor(Y, G, M),
>>     compare(D, N/F, M/G),
>>     D \== (=), !, C = D.
>> swi_found(C, X, Y, L, R) :-
>>     X =.. [_|P],
>>     Y =.. [_|Q],
>>     foldl(swi(C), P, Q, [X-Y|L], R).
>>
>> % sys_union_find(+Term, +List, -Term)
>> sys_union_find(X, L, T) :-
>>     member(Y-Z, L),
>>     same_term(X, Y), !,
>>     sys_union_find(Z, L, T).
>> sys_union_find(X, _, X).
>

Thread

Mercio’s Algorithm for Rational Tree Compare in Prolog Mild Shock <janburse@fastmail.fm> - 2025-08-04 02:52 +0200
  The Original Ganster (OG) of Gameification: IEEE 1044.1-1995 (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-04 13:48 +0200
    The Bitrot called Math Stack Exchange (Re: The Original Ganster (OG) of Gameification: IEEE 1044.1-1995) Mild Shock <janburse@fastmail.fm> - 2025-08-04 14:00 +0200
      I guess its back to Hopcroft and Karp.Re: The Bitrot called Math Stack Exchange) Mild Shock <janburse@fastmail.fm> - 2025-08-04 14:11 +0200
  Szpilrajn Theorem and Suzumura Consistency (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-06 01:50 +0200
    The good thing is we have at least Mercio’s Algorithm (Re: Szpilrajn Theorem and Suzumura Consistency) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:10 +0200
      Hopcroft and Karp’s is just Contraction (Was: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:13 +0200
        Re: Hopcroft and Karp’s is just Contraction (Was: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:23 +0200
      Should we use minimum_coa/3 ? (Was: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-08 23:45 +0200
        Perfectly balanced , as all things should be! (Was: Should we use minimum_coa/3 ?) Mild Shock <janburse@fastmail.fm> - 2025-08-08 23:49 +0200
  Mercios decidability was already attested in 2012 (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-14 20:26 +0200
    Performance of Mercio’s Total Order (Was: Mercios decidability was already attested in 2012) Mild Shock <janburse@fastmail.fm> - 2025-08-15 23:49 +0200
      Fuzzy Testing is your Swiss Knife (Re: Performance of Mercio’s Total Order) Mild Shock <janburse@fastmail.fm> - 2025-08-15 23:55 +0200
        Yeah, we have another name! (Was: Fuzzy Testing is your Swiss Knife) Mild Shock <janburse@fastmail.fm> - 2025-08-16 12:38 +0200
        Monte Carlo sampling the frontier version (Was: Yeah, we have another name!) Mild Shock <janburse@fastmail.fm> - 2025-08-16 12:42 +0200
        AI most hated by formal verification (Was: Fuzzy Testing is your Swiss Knife) Mild Shock <janburse@fastmail.fm> - 2025-11-26 17:02 +0100
  An NPU could give 1000x more LIPS (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-11-27 14:19 +0100
    Neural Network based dif/2 respectively (#\=)/2 (Re: An NPU could give 1000x more LIPS) Mild Shock <janburse@fastmail.fm> - 2025-11-27 14:51 +0100
      Zeus: A Language for Expressing Algorithms in Hardware (Re: Neural Network based dif/2 respectively (#\=)/2) Mild Shock <janburse@fastmail.fm> - 2025-11-27 15:03 +0100
        Googles TPU muscle in 2017 [Prolog Community is Sleepy Joe] (Re: Zeus: A Language for Expressing Algorithms in Hardware) Mild Shock <janburse@fastmail.fm> - 2025-11-27 15:23 +0100
    100% serious Giga Logical Inferences per Second (GLIPS) (Was: An NPU could give 1000x more LIPS) Mild Shock <janburse@fastmail.fm> - 2025-11-28 14:50 +0100
      The tables have turned: GigaLIP on the Laptop? (Re: 100% serious Giga Logical Inferences per Second (GLIPS) Mild Shock <janburse@fastmail.fm> - 2025-11-28 15:12 +0100

csiph-web