GregarianChild

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, have the opposite strengths and weaknesses: they are good at handling quantification, but not so good at theory solving. Moreover, all widely used ATPs tend to be for first-order classical logic, while Lean is based on higher-orders constructive logic. So there is still a gap to be bridged.

It is great to see that people work on this problem.

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 mistake again.

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 of a shortcut AlphaProof achieved. A good proxy for that would be the total energy usage for training and running AlphaProof. A moderate proxy for that would be the number of GPUs / TPUs that were run for 3 days. If it's somebody's laptop, it would be super impressive. If it's 1000s of TPUs, then less so.

A different world, but Verilog has in, out and inout parameters, too.

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.

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 from the ACM: https://www.youtube.com/watch?v=H7u4MbXonwA

Thanks, I had not noticed this.

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 Newman [1] , who, at some point, was Alan Turing's supervisor. See [2, 3].

[1] M. H. Newman, Stratified Systems Of Logic. https://www.classes.cs.uchicago.edu/archive/2007/spring/3200...

[2] J. R. Hindley, M. H. Newmans Typability Algorithm for Lambda-Calculus.

[3] H. Geuvers, Newmans Typability Algorithm. https://www.cs.ru.nl/~herman/computing2011.pdf

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 specification that is synthesised against), which program synthesis effortlessly matches.

On the apples-to-apples comparisons, LLMs often only obtain 70% - 80% precision, which means they are effectively solving a simpler synthesis problem. (Yes they have other benefits, like being able to extract knowledge from natural language, which conventional synthesis can't do, but that's offen not needed.)

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 what programmers would call an aggressive refactoring to the category of sets and functions - a foundational workspace within which almost all of conventional math is conducted (whether the practitioners realise it or not). Math is refactored in a way reminiscent of how HOL refactors math (but constructively).

Set theory is a legacy platform like MS-DOS (!) with many limitations and anomalies which topos theory can explain and perhaps alleviate. A topos is a "virtual machine, for math ... Definitions, constructions, theorems "run" in a topos just as apps run on a VM, or SQL statements run on a database. The promise of topos theory is to cleanly separate language from implementation (just as webdesigners separate HTML from business logic) A lot of math can easily be "refactored" to apply in a much wider context.

The steps in building this refactoring are:

• Define the concept of category, a workspace of dots and composable arrows between them

• Identify the category Sets as fundamental

• Abstract out the operations and laws that make Sets useful (think CCCs (= cartesian closed categories) with some extras)

• Axiomatise a topos as a category equipped with operations obeying these laws

• Find other naturally occurring examples of topoi

• Via internal categories, understand topoi as a complete foundation for math

• Specify a language for describing constructions and deductions in a topos

Note, if you don't care about foundations, then topos theory gives you nothing new, except labour of re-learning what you already know in a new form that is awkward if you heavily rely on non-constructive reasoning.

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 for efficient use of so much parallelism.

AWS certainly hired a lot of senior STM and ITP guys, such as John Harrison.

Yes.

A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.

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 prover with dependent types (like Lean, Coq or Adga) is not a fully solved problem.

For industrial-scale program verification, proof automation is everything! Nothing else matters.

I conjecture, but don't know, that Amazon write their HOL-based prover from scratch, to take into account their cloud resources. So it might well be the most modern prover of all.

Note that Leonardo de Moura, who initiated Lean, is now at AWS. To add even more complications, AWS does also use Lean, e.g. https://github.com/leanprover/SampCert

> "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 specifications slows down rapid evolution of programs, since the proliferate transitively along the control flow graphs. We can see this most prominently with Java's checked exceptions, but most effect annotations (to give an example of simple specification annotations) suffer from the same cancerous growth. This is probably at least partly intrinsic, but it could be improved by better automation.

Did you work with Ernst Dickmanns or his students on self-driving cars @ Daimler, they were (arguably) the first?

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.

> 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 idiomatic Ocaml has a simple transliteration.

Could you point towards a paper that does precise and minimal regular expression (or finite state automaton) inference?

> 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 may hit the same program multiple times). What's good about GP is how simple it is, so it's a good starting point.

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.

> 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. https://proceedings.neurips.cc/paper/1988/file/3def184ad8f47...

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 that report substantial GPU acceleration on what you call "non-deep ML"?

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, the 'real-world speedup' will have been assumed by the readership to be less. But this triggered a virtuos cycle of continuous improvements at all levels that has been dubbed "winning the hardware lottery" [2].

[1] K.-S. Oh, K. Jung, GPU implementation of neural networks.

[2] S. Hooker, The Hardware Lottery. https://arxiv.org/abs/2009.06489

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 you will have to program in an awkward style ("data parallel"). I am not aware of GPU acceleration of the work-horses of symbolic AI, such as Prolog, or SMT solving. There has been a lot of work on running SAT-solvers on GPUs, but I don't think this has really succeeded so far.

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?

Program synthesis is simply learning where the search space is syntax. In deep learning, taking the ImageNet paper as an example, the specification a bunch of photos with annotations, the search space is multi-variate real functions (encoded as matrix of floats) and the search mechanisms is gradient descent (implemented as backprop) with a loss function.

I think this paper uses regular expressions an example of how to search fast over syntax. It claims not to be tied to regular expressions.

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 paper dropped around 2010. Before nobody believed that backprop can be GPU-accelerated.

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.

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://easychair.org/publications/open/b7Cr

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

(Unlike Haskell,) Scala does not force monadic composition on you at all. You can use Scala as a pure OO language, or for old-skool ML-like FP where you don't use monadic context abstraction. I've done both successfully in production. Indeed I strongly advise against a monadic programming style for programmers with a mainstream programming background (imperative and OO).

In my (considerable) experience of teaching programming, imperative programmers find jumping straight from imperative programmers to a monadic style extremely difficult, the more experienced, the more difficult.