GregarianChild

9 ms·

31.
by GregarianChild 2y ago
That remains to be seen. SMT solvers such as Z3 and CVC5 tend to be good at theory solving (the T in SMT) but not so good at handling quantification. OTOH, the ATPs (= automatic theorem provers) used in 'hammers, like E, Spass, Vampire
32.
by GregarianChild 2y ago
Google stopped publishing interesting AI work since they had their AI lead taken away by OpenAI, and mostly with tech that was pioneered, but not monetised by Google like transformers. I imagine they are under pressure not to make this mist
33.
by GregarianChild 2y ago
We know that any theorem that is provable at all (in the chosen foundation of mathematics) can be found by patiently enumerating all possible proofs. So, in order to evaluate AlphaProof's achievements, we'd need to know how much o
34.
by GregarianChild 2y ago
A different world, but Verilog has in, out and inout parameters, too.
35.
by GregarianChild 2y ago
Can you point me to reading material about how the CUDA runtime does this with hardware assistance? I looked but I have been unable to find any thing persuasive in this direction.
36.
Reevaluating Google's Reinforcement Learning for IC Macro Placement (AlphaChip)(cacm.acm.org)
4 points by GregarianChild 2y ago|1 comments
37.
by GregarianChild 2y ago
We had previous discussions on HN about the Alphachip paper ( https://deepmind.google/discover/blog/how-alphachip-transfor... ) for example https://news.ycombinator.com/item?id=41672110 Short video
38.
by GregarianChild 2y ago
Thanks, I had not noticed this.
39.
by GregarianChild 2y ago
For those interested in the history of computing: the article mentions that the algorithm "seems to have been discovered independently multiple times over the years" . Interestingly, it also seems to have been discovered by Max
40.
by GregarianChild 2y ago
Could you give an example of an apples-to-apples comparison between (symbolic) program synthesis and LLMs that the latter wins? The reason I am asking is because, in my experience, LLMs never match the 100% precision (relative to the spec
41.
by GregarianChild 2y ago
If you understand the STLC (= simply typed lambda calculus) and why it is also a HOL (= higher-order logic) then you understand most of topoi already (although the match is not perfect). Topos theory is a branch of mathematics which applies
42.
by GregarianChild 2y ago
I don't know, but given that AWS has 1000s if note millions of servers that may have idle cycles, it makes sense to use them for automatic theorem proving. And there is no existing ITP or even SMT solver that was specifically designed
43.
by GregarianChild 2y ago
Yes. A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.
44.
by GregarianChild 2y ago
HOL is a classical (i.e. non-constructive) logic based on simple type theory, and that makes proof automation much easier. Adapting the kind of proof automation that classical logic with simple types enables to a Curry-Howard based prove
45.
by GregarianChild 2y ago
> "verification aware Rust" ... building such a language from the ground up could Could you sketch in a few bullet point what you think is missing and how to fix the gaps? In my experience a core problem is that adding rich
46.
by GregarianChild 3y ago
Did you work with Ernst Dickmanns or his students on self-driving cars @ Daimler, they were (arguably) the first?
47.
by GregarianChild 3y ago
Among the ML descendants, I suggest Scala 3, because it has essentially all the power that we like in Haskell, (HTKs, good support for ad-hoc polymorphism), but runs on the JVM, a mainstream platform with a vast library ecosystem.
48.
by GregarianChild 3y ago
> PL that is essentially OCaml but with a better syntax. Scala 3! Python-ish syntax, much larger library ecosystem (due to JVM) than either Haskell or Ocaml. Better integration of OO and FP than Ocaml. So similar to Ocaml that idiomati
49.
by GregarianChild 3y ago
Could you point towards a paper that does precise and minimal regular expression (or finite state automaton) inference?
50.
by GregarianChild 3y ago
> genetic programming There is no magic in GP. It is just another form of searching the space of programs, i.e. program synthesis. The search mechanism is a local, stochastic search, known to be especially inefficient (for example you
51.
by GregarianChild 3y ago
The paper claims that there is no neural / deep learning based solver that performs well on regular expression inference. Calls to Coq and Z3 will be very slow and not competitive with GPU compute.
52.
by GregarianChild 3y ago
> backpropagation, and its polynomial time complexity How do you reconcile the NP-completeness result in [1] about training neural networks with your claim? [1] A. L. Blum, R. L. Rivest, Training a 3-Node Neural Network is NP-Complete.
53.
by GregarianChild 3y ago
There is no agreement on the exact meaning of ML and AI. They are often used interchangeably. And for good reason, because it's all about getting computers to learn. We should not squabble about semantics. Can you point towards papers
54.
by GregarianChild 3y ago
Exactly. It's easy to see in retrospect, but hard in prospect: the original paper [1] on GPU acceleration of NNs reports a measly 20x speedup. Assuming a bit of cherry-picking on the author's side to make get the paper published,
55.
by GregarianChild 3y ago
Can you point me to papers with reproducible benchmarking that achieves big speedups on those? Modern GPUs are GP -GPUs: where GP means "general purpose" : you can run any code on GPGPUs. But if you want to gain real speed-ups y
56.
by GregarianChild 3y ago
Good question. All supervised learning is a form of search with three components: - Specification: what are you are looking for? - Search space: were are you looking? - Search mechanism: how are you going through the search space? Pro
57.
by GregarianChild 3y ago
Someone managed to GPU-accelerate program synthesis, a form of symbolic ML. First time for ML that is not deep learning: https://dl.acm.org/doi/10.1145/3591274 Deep learning took off precisely when the ImageNet p
58.
by GregarianChild 3y ago
Because all known SAT algorithms rely heavily on data-dependent branching based on non-local data. That makes the existing algorithms slow on GPUs. An algorithmic breakthrough is needed to change this.
59.
by GregarianChild 3y ago
I found the description of CDCL as an abstract rewrite system illuminating. It's much shorter than an implementation. See e.g. [1]. There is/was a more readable version online, but I can't find it now. [1] https://
60.
by GregarianChild 3y ago
It's worth mentioning Mathias Fleury work who first verified a CDCL implementation [1]. He has written follow-up stuff. [1] https://fmv.jku.at/fleury/papers/Fleury-thesis.pdf

More ›