upghost · HackerTrans

28 gün öncediscuss

theprimagen called this[1] like three days ago. That was fast.

[1] https://www.youtube.com/watch?v=m-bT5v5Tm7w&t=164s

If this wasn't CERN tech I would think I was being taken for a ride. Conventional wisdom is that distributed consensus is not possible at this kind of performance, does anyone have a sense for how this is different and how my mental model is wrong?

upghost

2 ay öncediscuss

Thanks. I thought it was interesting choosing arithmetic instead of some other relation because multimodal arithmetic (via CLP) is more of a PhD thesis than a blog post. Other relations might've been easier to demonstrate a general query.

What I couldn't tell from the article was if the author somehow achieved a multimodal arithmetic relation without needing CLP using a stack machine. That would be a neat technique.

upghost

3 ay öncediscuss

Man that is such a bummer. The Naval Support Activity (NSA) "base" is not a hardened military facility. I've never been to the one in Bahrain, but it's usually where you go to play ultimate frisbee, maybe some paintball if you are lucky, and other types of R&R. Usually have a Naval Exchange (NEX) which is like a really discounted 7-11 / gift shop / walmart (depending on where you are).

upghost

3 ay öncediscuss

Great writeup. Only thing I din't see in here was an analysis of the impact of players like Talaas[1] and their stupid faster hardware LLMs.

I feel like it could be majorly disruptive, but idk if it's going to prolong the apocalypse or bring it about sooner -- or if it's a big nothing burger.

But the demo[2] is super cool.

[1]: https://taalas.com

[2]: https://chatjimmy.ai/

upghost

4 ay öncediscuss

> familiarity vs simplicity

Love this, I've never heard it put that way before.

upghost

4 ay öncediscuss

Yeah, this checks out. I wonder what they are doing to prevent semantic collapse. Also, I wonder if the base model would already be instruct and RLHF tuned or only pre-trained. Trying to do additional training without semantic collapse in a way that is meaningful would be interesting to understand. Presumably they are using adapters but I've never had much luck in stacking adapters.

i.e.:

1. Do I start with an RLHF tuned model, "pretrain" on top of that (with adapter or by freezing weights?), then SFT on top of that (stack another adapter, or add layer(s) and freeze weights?) (and where did I get the dataset? synthetic extraction from corpus?), then RL (adapter, add layer(s) and freeze?)

2. or do I start at SF tuned model, ...

3. or do I start at raw pre-trained model, ...

Would love to know what the matrix used was.

upghost

4 ay öncediscuss

> Pre-training allows organizations to build domain-aware models by learning from large internal datasets.

> Post-training methods allow teams to refine model behavior for specific tasks and environments.

How do you suppose this works? They say "pretraining" but I'm certain that the amount of clean data available in proper dataset format is not nearly enough to make a "foundation model". Do you suppose what they are calling "pretraining" is actually SFT and then "post-training" is ... more SFT?

There's no way they mean "start from scratch". Maybe they do something like generate a heckin bunch of synthetic data seeded from company data using one of their SOA models -- which is basically equivalent to low resolution distillation, I would imagine. Hmm.

upghost

4 ay öncediscuss

> We are doing this to self-fund further investment in AI and enterprise sales while strengthening our financial profile.

Some quotes from the video:

> ...at the same time, we're a people company.

> Your work will live on in our products.

> Doing the right thing for Atlassian while acting with humanity and doing the right thing for all those on all sides of this set of decisions.

Wow. There's a lot to unpack here.

upghost

4 ay öncediscuss

In Prolog the syntax is incredibly important. It is designed to be metainterpreted with the same ease in which a for-loop might be written in another language.

https://www.metalevel.at/acomip/

  mi1(true).
  mi1((A,B)) :-
        mi1(A),
        mi1(B).
  mi1(Goal) :-
        Goal \= true,
        Goal \= (_,_),
        clause(Goal, Body),
        mi1(Body).

This can be arbitrarily extended in very interesting, beautiful, and powerful ways. This is extraordinarily hard to achieve and did not happen by accident.

As a challenge, see how easy it is to write a metainterpreter in another language of your choice. Alternately, see if you can think of any way the metainterpretation system in Prolog could be improved.

Finally, think of what would happen to this if we changed the syntax and introduced something like object.field notation.

So while logical programming can be achieved with other syntaxes, the metaintrepretive aspect will be lost. I have yet to see a language that does this better.

upghost

4 ay öncediscuss

Very interesting stuff. Apparently this is the implementation: https://github.com/dicpeynado/prolog-in-forth

Thinking about the amount of thought and energy that went into this, back in 1987 -- mostly preinternet, pre-AI. Damn.

I feel really lucky that we get to build on things like this.

upghost

5 ay öncediscuss

I'm surprised how hard I had to dig for an actual example of syntax[1], so here you go.

[1]: https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extra...

upghost

5 ay öncediscuss

So I have been doing formal specification with TLA+ using AI assistance and it has been very helpful AFTER I REALIZED that quite often it was proving things that were either trivial or irrelevant to the problem at hand (and not the problem itself), but difficult to detect at a high level.

I realize formal verification with lean is a slightly different game but if anyone here has any insight, I tend to be extremely nervous about a confidently presented AI "proof" because I am sure that the proof is proving whatever it is proving, but it's still very hard for me to be confident that it is proving what I need it to prove.

Before the dog piling starts, I'm talking specifically about distributed systems scenarios where it is just not possible for a human to think through all the combinatorics of the liveness and safety properties without proof assistance.

I'm open to being wrong on this, but I think the skill of writing a proof and understanding the proof is different than being sure it actually proves for all the guarantees you have in mind.

I feel like closing this gap is make it or break it for using AI augmented proof assistance.

upghost

5 ay öncediscuss

Anakin: I'm going to save the world with my AI vulnerability scanner, Padme.

Padme: You're scanning for vulnerabilities so you can fix them, Anakin?

Anakin: ...

Padme: You're scanning for vulnerabilities so you can FIX THEM, right, Annie?

upghost

5 ay öncediscuss

tl;dr - All this AI stuff is just Universal Paperclips[1]

I see a lot of comments about folks being worried about going soft, getting brain rot, or losing the fun part of coding.

As far as I'm concerned this is a bigger (albeit kinda flakey) self-driving tractor. Yeah I'd be bored if I just stuck to my one little cabbage patch I'd been tilling by hand. But my new cabbage patch is now a megafarm. Subjectively, same level of effort.

[1]: https://en.wikipedia.org/wiki/Universal_Paperclips

upghost

6 ay öncediscuss

Author: "Not my favorite language"

Prolog: "Mistakes were made"

As an avid Prolog fan, I would have to agree with a lot of Mr. Wayne's comments! There are some things about the language that are now part of the ISO standard that are a bit unergonomic.

On the other hand, you don't have to write Prolog like that! The only shame is that there are 10x more examples (at least) of bad Prolog on the internet than good Prolog.

If you want to see some really beautiful stuff, check out Power of Prolog[1] (which Mr. Wayne courteously links to in his article!)

If you are really wondering why Prolog, the thing about it that makes it special among all languages is metainterpretation. No, seriously, would strongly recommend you check it out[2]

This is all that it takes to write a metainterpreter in Prolog:

  mi1(true).
  mi1((A,B)) :-
          mi1(A),
          mi1(B).
  mi1(Goal) :-
          Goal \= true,
          Goal \= (_,_),
          clause(Goal, Body),
          mi1(Body).

Writing your own Prolog-like language in Prolog is nearly as fundamental as for-loops in other language.

[1] https://www.youtube.com/@ThePowerOfProlog

https://www.metalevel.at/prolog

[2] https://www.youtube.com/watch?v=nmBkU-l1zyc

https://www.metalevel.at/acomip/

upghost

7 ay öncediscuss

Ok what I would really love is something like this but for the damn terminal. No, I don't store credentials in plaintext, but when they get pulled into memory after being decrypted you really gotta watch $TERMINAL_AGENT or it WILL read your creds eventually and it's ever so much fun explaining why you need to rotate a key.

Sure go ahead and roast me but please include full proof method you use to make sure that never happens that still allows you to use credentials for developing applications in the normal way.

upghost

7 ay öncediscuss

A really simple one is traversing a linked list (or any naturally recursive data structure, such as a dictionary or tree). It is very natural to traverse a recursive data structure recursively.

upghost

7 ay öncediscuss

Really impressive! For anyone who's not a pythonista, trying to implement TCO is something akin to solving the Collatz conjecture but for Python. It's often just an exercise in madness. So seeing an elegant solution to this is really cool, I myself was a victim of this madness and was unable to do it so very cool to see someone nail it! This will be a goto tool for sure.

upghost

7 ay öncediscuss

Ok hear me out. It's not particularly obvious to me why plants being easy to replicate suddenly destroyed the rare plant market. Surely they can't be easier to replicate than software. That hasn't seemed to put much of a dent in the software market.