zero_k

PoC||GTFO is a great magazine :) Yay to Travis Goodspeed! Sorry, I wanted to say Pastor Laphroaig. Just don't get him started on his Tennessee buck belt :D

"Europe's leading AI companies and research institutions" -- order should be reversed, if the EU is serious about AI. It should say: "Europe's leading research institutions and AI companies..."

This is by Edward Tufte. If you haven't had the chance to check out Edward Tufte's other works, in particular, the Visual Display of Quantitative Information [1] then I highly suggest you do. Every time I see a horrible graphic in a research paper, I redirect authors to [1]. It ought to be a must-read for anyone wanting to create a graph. Seriously, if you intend to display information, read that book. It'll open your eyes to make you see the immense amount of waste of space and clutter that people introduce.

It's basically an ode to clear, cutter-less, data visualization. Check out this timetable [2] (horizontal lines: stations, vertical lines: hours, diagonal lines: trains), and your mind will be blown. It's compact, it gives you all the information you need, it can be navigated by your grandma (or your granddaughter) and it likely shows more information than most digital or paper-based system you have ever met, in a smaller format.

[1] https://www.edwardtufte.com/book/the-visual-display-of-quant... [2] https://miro.medium.com/v2/resize:fit:1400/format:webp/0*8zW...

They are effectively unregulated. Most drivers have no clue how to adjust them, and the "modders" replace them randomly with whatever they find is the brightest/coolest. Yeah, you _could_ fine them and claim that the cars are unroadworthy until fixed, but if a rule is not enforced, is it a rule? So, yeah, effectively unregulated, too.

I bicycle a lot and I tell other cyclist that they need to adjust their lights all the time. At least they seem to take feedback. Somehow, drivers think that they, in their multi-ton metal boxes are a band apart, and tend to take zero criticism from anyone outside of their metal boxes.

Publishing in Academia is a scam. Nowadays everyone puts their papers also on arxiv.org so at least we can read each other's papers for free. While of course still paying the fees to these publishers who are doing nothing but messing up the PDF (I have to fight them to fix the mistakes they add every time a paper is published), while claiming to do a value-add, which happens to add value to nobody but their own pockets. It's a scam through and through.

Of course one has to examine why this system is still in place. And it's mostly to do with policies in universities, where certain journals/conferences are valued more, and changing that is hard, because e.g. Springer happens to own the name. So we all pay millions to Springer, for the use of this name (that we, together, made great, not Springer), and in return, they charge us the privilege of reading the papers that we reviewed, edited, and wrote. It's insane, but it can't be changed as long as universities refuse to change.

So the hard truth is, it's not Springer/IEEE/Nature/etc, it's ultimately, us.

It doesn't need to be good at solving the problem. It only needs to be good at translating the problem of "If the unknown x is divided by 3 it has the same value as if I subtracted 9 from it" into "x/3 == x-9 && x is an Real number". The formal method tool will do the rest.

Note that if the LLM gets the implicit assumptions wrong, the solution will be unsatisfactory, and the query can be refined. This is exactly what happens with actual human experts, as per the anecdote I shared in [3]. So the LLM can replace some of the human-in-the-loop that makes it so hard to use formal methods tools. Humans are good at explaining the problem in human language, but have difficulty formulating them in ways that a formal tool can deal with. Humans, i.e. consultants, help with formalizing them in e.g. SMT. We could skip some of that, and make formal methods tools much more accessible.

Correction, Lean4 [1] is sponsored by Amazon, the lead developer, Leonardo de Moura is at AWS now [2]. He was previously at Microsoft Research [3]. Meeting him is a real ride, I only had the chance to talk with him once.

[1] https://lean-lang.org/

[2] https://leodemoura.github.io/about.html

[3] https://www.microsoft.com/en-us/research/blog/the-inner-magi...

Yes, we should use LLMs to translate human requirements that are ambiguous and have a lot of hidden assumptions (e.g. that football matches should preferably be at times when people are not working & awake [3]), and use them to create formal requirements, e.g. generating SMT [1] or ASP [2] queries. Then the formal methods tool, e.g. Z3/cvc5 or clingo can solve these now formal queries. Then we can translate back the solution to human language via the LLM. This does not solve some problems, e.g. the LLM not correctly guessing the implicit requirements. But it does go around a bunch of issues.

We do need to pump up the jam when it comes to formal methods tools, though. And academia is still rife with quantum and AI buzzword generators if you wanna get funding. Formal methods doesn't get enough funding from Academia. Amazon has put a bunch of money into it (hiring all good talent :sadface:), and Microsoft is funding both Z3 and Lean4. Industry is ahead of the game, again. This is purely failure of Academic leadership, nothing else.

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

[2] https://en.wikipedia.org/wiki/Answer_set_programming

[3] Anecdotal, but this was a "bug" in a solution offered by a tool that optimally schedules football matches in Spain.

Wow, nice work [1] ! I used to work on CryptoMiniSat a lot. Nowadays I'm doing model counting and maybe synthesis, if all goes well [2]

[1] https://github.com/leanprover/lean4/pulls/bollu [2] https://x.com/SoosMate/status/1827308967208317241

Other than cryptography? Like, you see a use-case for it there? Please do educate me! IMO there's nothing there. It's a barren landscape. The desert is more alive.

Cadence is a good one. There are also bus/train schedule optimization startups/companies. AWS is also hiring in this field, a lot, but I wouldn't recommend it. Even though many people there are very good, and I respect some of the individual people there very much.

I mean, I wish. I have met these so-called giants of the field when I was at conference (they had a yearly big-brains meeting the same time, same place). I bet they talk about classic stuff because otherwise they wouldn't get funding. Quantum mechanics and using quantum computers for quantum problems actually would have convinced me. But who cares about me. What they need this is this thing called MONEY and that doesn't come with intellectually interesting problems -- it comes with overinflated claims over things that the committee understands. So classical problems it is. Can't blame them playing the game, but at the same time, I wonder how they look into the mirror at night.

By the way, if you truly care about NP-optimization, e.g. MaxSAT algorithms, there's a lot of good work being done, just check out [1]. It's fun, and useful. You could make >$1B just by slightly improving global logistics via such algorithms. Yes, scalability can be an issue, but it only takes some work to cut the problems into chunks, and do local optimization at each level, rather than total global optimization. Yes, it won't be a global optimum, but likely significantly better than what's out there right now. They already use these algorithms for e.g. train and bus schedule optimization.

[1] https://maxsat-evaluations.github.io/

Random k-SAT is useless. I won a number of awards at SAT competitions over the years -- not in random k-SAT, they don't even run that track anymore [1] And I'm pretty damned certain whatever that paper is saying, could be fixed with classical algorithms, if anyone cared about random k-SAT. But nobody does, for a good reason. I could go on ranting about quantum, but I'll stick to the one thing I actually know about, SAT solving.

I think there are some really cool things out there, if you wanna dump research money into. For example SMT, model counting, symbolic execution, automated invariant finding, CHC, BMC, function synthesis, programming language research.

Academia will one day wake up, and realize that they've been awarding tenure to people who have done nothing but a quantum buzzword generator, while the people working hard at important topics are left behind. Like the dude (Victor Ambros) who recently got the Nobel only to be previously declined tenure at Harvard. Big fail.

[1] https://satcompetition.github.io/2024/results.html

You are actively advocating for the death of people. This must be deleted by the OPs ASAP. What is even going on.

It's hard to find, sorry. The contact info is here: https://www.hs-augsburg.de/searchwing/de/standorte/

Best to contact: philipp.borgers@searchwing.org

Search And Rescue (SAR) is sometimes VERY political. We build long-range RC airplanes to help find boats in distress at sea on the Mediterranean [1]. As you might expect, we could do 10x better, with less resources, if the powers that be wouldn't make it impossible to e.g. launch from an island and return to an island. So we launch from a boat, because it's not national territory and they can't make it impossible.

Shameless Plug: If you wanna join, let us know. We definitely would benefit from better on&off-board image recognition. But there are many, less buzzword-y, challenges as well: designing, building & testing airplanes, training pilots, delivering planes & batteries (challenging due to Watt-Hour restrictions), remote issue debugging, etc.

[1] https://tha.de/searchwing/

Honestly, I'm very excited about zig. Lean and mean, and it's written by someone who isn't sitting in an ivory tower, not caring about actual usability. It wasn't designed by a team of PhDs (like, e.g. Haskell), while it's clearly inspired by very useful ideas in e.g. Rust, Haskell, etc. I think it'll be very exciting to write code in zig.

If you wanna do it in a flexible way that is very easy to use and essentially the future of ZK, use Powdr [1]. Just write your code in rust nostd and be done with it. It's a compiler, basically. Once you use it, you'll never go back to hand-massaging polynomials. It'd be like writing assembly. Sure, some can do it, and it can be fun, but why do it if there are compilers out there to do the heavy lifting for you? :)

[1] https://github.com/powdr-labs/powdr

Exactly. See Sidney Dekker's Field Guide to Understanding Human Error. The posters do (almost) nothing -- other than covering the backside of those who put them up, and doing safety theatre. Looks good, does nothing for safety.

The same author, Sidney Dekker, has a very good book about how to deal with someone like this whistleblower. It's called "Just Culture". Well worth a read. Spolier: It's not to silence them, not this way. You can silence the person by, you know, actually doing something useful. But that requires actual change, and more importantly, a change in attitude. And you need to convince the crowds that you are doing better by NOT putting up posters. You'll be surprised how many people really think the posters help.

Proofs and proof checking is also big in SAT solving (think: MiniSat) and SMT (think: z3, cvc5). It's also coming to model counting (counting the number of solutions). In fact, we did one in Isabelle for an approximate model counter [1], that provides probabilistically approximate count (a so-called PAC guarantee), which is a lot harder to do, due to the probabilistic nature.

[1] https://github.com/meelgroup/approxmc

100% agree

The guarantees would not hold, I'm pretty sure ;) Maybe one of the authors could chip in, but my hunch is that with that you could actually introduce arbitrarily large errors. The beauty of this algorithm really is its simplicity. Of course, simple is.. not always easy. This absolute masterpiece by Knuth should demonstrate this quite well:

https://www.sciencedirect.com/science/article/pii/0022000078...

It's an absolutely trivial algorithm. Its average-case analysis is ridiculously hard. Hence why I think this whole Ordo obsessions needs to be refined -- worst case complexity has often little to do with real-world behavior.

Not me, the authors -- I'm a fly on the wall compared to them ;) This is some serious work, I just did a fast implementation. Re implementation -- it turns out that there are parts of some standard libraries that this problem pushes to its limits, that we had to go around during implementation. So there were still some cool challenges involved. I was also pretty happy about the late binding/lazy evaluation thing I came up with. Of course Knuth just did it (check his notes), without even thinking about it :D What is an achievement for me is a lazy Monday coffee for him, but oh well!

What made me realize is that I saw some snippets of emails he wrote to a colleague. It was... insane. You could see his mind race. He recognized patterns in minutes that would take me days, if not weeks, to recognize. Also, he actually writes and runs code, overnight if need be. It was as bit of a shock to me. He's not in an ivory tower. He's very much hands on, and when he's behind the wheel, you're in for a ride.

I was involved with implementing the DNF volume counting version of this with the authors. You can see my blog post of it here:

https://www.msoos.org/2023/09/pepin-our-probabilistic-approx...

And the code here: https://github.com/meelgroup/pepin

Often, 30% of the time is spent in IO of reading the file, that's how incredibly fast this algorithm is. Crazy stuff.

BTW, Knuth contributed to the algo, Knuths' notes: https://cs.stanford.edu/~knuth/papers/cvm-note.pdf

He actually took time off (a whole month) from TAOCP to do this. Also, he is exactly as crazy good as you'd imagine. Just mind-blowing.

I am 100% with you. I have infinite admiration for von Neumann's talents. He was the genius of the geniuses. I wish I could have a 10 minute chat with him. He'd blow my mind, I'm sure. I'd love to explain some of the research issues I'm working on to him, I have a feeling he'd nail them to the ground. His resume is absolutely insane. The dude invented merge sort and it's an effin' side-note to his work. Like, WAT. His achievements could fill the resume of 50 Nobel Laureate scientists. Plus apparently he had a CHARACTER, like a real one. Would have loved to shoot the sh&t with him.

Just go to an RC field near you, you'll see people flying like that.

But don't forget, an RC heli is an accident waiting for a place to happen.

Wow, yes, so true! I didn't realize how powerful this kind of fear is. You put it quite well. I'll now have to think about this...

Yeah, it's a bulls**t comment. Fools are dime a dozen :(