Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.physics > #895955

Could ISAMORE anti-unification help? (Re: Buddos Waterloo: Checkpoint McCune)

Cross-posted to 2 groups.

Show all headers | View raw

Hi,

One challenge is that the example has
not only anti-unification, like the c*d\=d*c,
the Mc Cune style model finder implementation

makes also heavy use of backtracking. So
I even don’t know whether ISAMORE papers
with saturation would help:

Finding Reusable Instructions via E-Graph Anti-Unification
Youwei Xiao et al. - ASPLOS ’26
https://github.com/pku-liang/ISAMORE

But I guess ISAMORE also delivers
rewriting challenges. But their subject
matter in the above paper is LLVM/GEM5 (*),

so maybe so maybe I rather buy a new Mac
Neo (only $500) and enjoy local AI.

Bye

(*)
https://en.wikipedia.org/wiki/Basic_Linear_Algebra_Subprograms#Level_3

Mild Shock schrieb:
> Hi,
> 
> Now toying around with a model finder,
> for some rewritng problems. Not bad, I
> didn't see that before on my computer:
> 
> ?- time(mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, _)).
> % Zeit 166.140 ms, GC 0.000 ms, Lips 18616 k
> true
> 
> ?- mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, R).
> R = [d-2, c-1, 5*2-3, 5*5-4, 4*3-2, 3*5-2, 3*2-5, 4*4-5, 2*4-3,
> 2*3-4, 3*4-1, 3*1-4, 5*3-1, 4*1-3, 1*5-3, 1*3-5, 2*1-5, 2*5-1,
> 5*1-2, 4*2-1, 1*4-2, 1*2-4, 5*0-5, 4*0-4, 4*5-0, 5^ -1-4, 5*4-0,
> 4^ -1-5, 3*0-3, 3*3-0, 3^ -1-3, 2*0-2, 2*2-0, 2^ -1-2, 1*0-1,
> 1*1-0, 1^ -1-1, 0^ -1-0, 0*5-5, 0*4-4, 0*3-3, 0*2-2,
> 0*1-1, 0*0-0, e-0]
> 
> But still not as good as Mc Cune, wo reported
> 0.010 seconds , so 10 ms (*). I guess I need to
> explore more heuristics. But will it include
> 
> union find? The payback of union find in such
> search examples is so low. If |D| = n is the
> domain size, then although |D x D| has size n^2,
> 
> the diagonal E_D, namely E_D = { (x,y) | x e D,
> y e D, x = y } has only size n. So the probability
> of a pair in certain problem domains, is around 1/n,
> 
> getting smaller and smaller with larger and larger n.
> 
> Bye
> 
> (*)
> https://www.mcs.anl.gov/research/projects/AR/mace4/July-2005/doc/mace4.pdf
> 
> Mild Shock schrieb:
>> Hi,
>>
>> This is a nice example how the young generation
>> doesn't understand systems that were developed
>> 30 years ago:
>>
>> Example 1:
>> No clue that SWI-Prolog does have JIT indexes,
>> which explain mysterious differene between
>> cold and warm run.
>> https://arxiv.org/pdf/2511.13600
>>
>> Example 2:
>> No clue that subsumption could make a difference,
>> claims left recursion is fastest, with referene
>> to [TL10] and a bogus node argument.
>> https://arxiv.org/abs/2504.21291
>>
>> Maybe the Prolog eduction group should organize
>> a summer school about tabling?
>>
>> Sad news: It will not help to keep up with
>> the AI boom. Whats behind the AI boom and
>> computing transitive closures?
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Ok, thats noice:
>>>
>>> "On a GPU cluster, the ratio of high computing
>>> power to communication bandwidth makes scaling
>>> breadth-first search (BFS) on a scale-free
>>> graph extremely challenging."
>>>
>>> Scalable Breadth-First Search on a GPU Cluster
>>> Yuechao Pan, Roger Pearce, John D. Owens
>>> 2018 - Lawrence Livermore National Laboratory
>>> https://arxiv.org/abs/1803.03922
>>>
>>> Sniff, still passed the deadline Q1 2026 for
>>> my GigaLIPS Prolog. There were so many other
>>> improvements , more low hanging fruits to cover.
>>>
>>> Bye
>>>
>>> P.S.: Wanna rent some GPUs?
>>>
>>> Cloud GPU Index
>>> Compare 2,542 GPU prices across 57 cloud providers
>>> https://getdeploying.com/gpus
>>>
>>> Mild Shock schrieb:
>>>> Well its called "artificial" intelligence.
>>>> Like "atificial" flowers made from plastic
>>>> try to share the look and feel of natural flowers,
>>>>
>>>> articial intelligence tries to share the
>>>> look and feel of natural intelligence.
>>>> AI is not really genetic engineering of
>>>>
>>>> bioforms, right? However, there is a research
>>>> frontier sometimes called biocomputing or
>>>> synthetic biology AI.
>>>>
>>>> Kunstblumen
>>>> https://www.xxxlutz.ch/kunstblumen-C22C8C1
>>>>
>>>> The convergence of AI and synthetic biology: the looming deluge
>>>> https://www.nature.com/articles/s44385-025-00021-1
>>>>
>>>> x schrieb:
>>>>> On 3/7/26 03:08, Mild Shock wrote:
>>>>>> Hi,
>>>>>>
>>>>>> Resolution of Erd˝os Problem #728
>>>>>> We provide a writeup of a resolution of Erd˝os
>>>>>> Problem #728; this is the first Erd˝os problem
>>>>>> (a problem proposed by Paul Erd˝os which has
>>>>>> been collected in the Erd˝os Problems website [3])
>>>>>> regarded as fully resolved autonomously by an AI
>>>>>> system. The system in question is a combination of
>>>>>> GPT-5.2 Pro by OpenAI and Aristotle by Harmonic,
>>>>>
>>>>> I guess there is something called 'logic' and then
>>>>> there is something called 'semantics'.
>>>>>
>>>>> Does it matter if words have meaning?  If the
>>>>> answer is no - then of course you can generate
>>>>> the look and feel of meaning through 'AI'.
>>>>>
>>>>>
>>>>
>>>
>>
> 

Back to sci.physics | Previous | Next — Previous in thread | Find similar | Unroll thread

Thread

Re: AI solves probl;em Knuth was/is working on! Mild Shock <janburse@fastmail.fm> - 2026-03-04 08:29 +0100
  Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728 (Re: AI solves probl;em Knuth was/is working on!) Mild Shock <janburse@fastmail.fm> - 2026-03-07 11:58 +0100
    Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-07 12:08 +0100
      Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-03-07 07:21 -0800
        Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-03-07 07:36 -0800
          Only, three decades in software engineering? Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:00 +0100
            Re: Only, three decades in software engineering? Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:19 +0100
              Amazing Visual Perception, even for ASCII Input [GPT 5.3] (Was: Only, three decades in software engineering?) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:34 +0100
                Visual Perception helps reading Matrices, Fractions, etc.. (Re: Amazing Visual Perception, even for ASCII Input [GPT 5.3]) Mild Shock <janburse@fastmail.fm> - 2026-03-08 20:21 +0100
      Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) x <x@x.net> - 2026-03-08 19:10 -0700
        Biobrain cannot digest "Artificial" in AI (Was: Aristotle: The Era of Vibe Proving is Here) Mild Shock <janburse@fastmail.fm> - 2026-03-09 11:21 +0100
          Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS) Mild Shock <janburse@fastmail.fm> - 2026-04-04 14:10 +0200
            Buddos Waterloo: Checkpoint McCune (Re: Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS) Mild Shock <janburse@fastmail.fm> - 2026-05-10 16:20 +0200
              Could ISAMORE anti-unification help? (Re: Buddos Waterloo: Checkpoint McCune) Mild Shock <janburse@fastmail.fm> - 2026-05-10 16:48 +0200

csiph-web