Symbolic mathematics finally yields to neural networks
quantamagazine.org
quantamagazine.org
Professor Patrick Winston pointed out that most of the AI programs we were going to look at in his class (chess, natural language, 3D vision in block world, etc.) ended up, like integration, as simple code plus a database of facts.
Back then, there was general optimism about the future of AI. No one anticipated how slow progress would be while the capabilities of the hardware grew a million-fold.
The work referenced in the article is interesting. It appears to be another small step in advancing AI. It's a small, but difficult, step like almost every other advance in AI, and I admire the work done by those working in this field.
The problems of solving simple differential equations and symbolic integration at the first year calculus level are not really advanced math. Humans solve these problems with a relatively small bag of tricks that transform a symbolic integral into a simpler form. A program can do the same thing with an even more detailed database of transforms that can be attempted at each point in the search tree until a simple solution is reached.
The article claims that the new program can solve difficult integrals. This is interesting because hard to solve integrals are often associated with real physical phenomena. See for example the triple integrals of W. F. van Peype which arose while he was studying magnetism in different materials. These, relatively, plain looking definite integrals stumped some of the world's most famous mathematicians. See [1] and/or [2] for their interesting history.
[1] Paul J. Nahin, Inside Interesting Integrals, Springer, 2015. Section 6.5, The Watson/van Peype Triple Integrals.
[2] I.J. Zucker, 70+ Years of the Watson Integrals, http://www.inp.nsk.su/~silagadz/Watson_Integral.pdf
From where I sit, the bad outweighs the good.
We are so far away from GAI at the moment that I don't for one second actually worry about the moral implications of General Artifical Intelligence.
I don't see the point in worrying about something when we know literally nothing about that thing, and barely have a path to making it. It's very likely that by the time we are capable of making GAI (Excusing the very probable idea that we will be able to simulate a brain, but not at any proper speed -- see the three body problem and the challenges with simulating literally any other physical systems), there will be half a dozen problems we do need to worry about, that we cannot forsee. There will also be half a dozen limitations that mean that our current worries are essentially worthless. It's the same with all new technology.
It's also interesting that people who tend to worry about GAI never worry about current levels of AI, especially in a military context. They seem entirely unconcerned with being worried about literally crappy and half-baked neural networks being deployed for use in drones. They seem entirely unconcerned with the lack of proper dataset balancing and sorting that ensures that current AI models do not have racial bias (or, indeed other types of bias).
Just last year I saw a twitter post about a startup that was re-creating literal phrenology, using AI to try and profile whether people were criminals or not based on facial shape. The typical Less Wrong / MIRI folks never seem to be worried about that, no, they spend their time in fear of Roko's Baselisk and other currently-impossible scenarios. They literally purged posts, threads, and comments that made any mention of that under the utter and complete fear that maybe in the far flung future a very bad simulation (Unless, their brains are cryogenically frozen, I guess, but it's very likely that brain structure would degrade under the immense timespan anyway) of them would be tortured for their current actions, by a good AI, that had apparently gone so insane that it thought that torturing low-fidelity simulations of people in the future could affect the past and cause it to be created faster.
Speculating about the future can be a positive thing, but I don't see how this is at all useful or healthy.
Worrying about the future of surgical technology is very different. The end goal of surgery is to save a life or improve the quality of life, and it involves restoring a single person back to working order.
The end goal of AI is to _think_. The upper bound on that is horrifying. Once something can think it can build. Once something can build it can multiply. The upper bound on AI is replacing the human species.
I’m not saying I’m nervous about this happening next year. I know how terribly inept we are at true GAI. I’m thinking purely abstractly, and in that light I think we should more serious about ground rules for AI.
It can't even evaluate the answer numerically, it just freezes for minutes!
Edit: about 10 minutes later it spat out 1.393203930, so it can solve the integral, but not easily.
Update: This paper reminds me why I vehemently hate modern mathematical notation, with subscripts and superscripts can mean anything at all and everyone's idea of "convention" is different. On the second page there's an algebraic expression for the solution, which at first glance seems to be:
4/Pi^2 * EllipticK[Sqrt[1/2 - Sqrt[1 - w^(-2)]/2]]^2
But this evaluates to 1.76351 not 1.39320 as given in the paper. The "K^2" in the paper is not the "complete elliptic integral of the first kind" squared, it's some other function that squares its input somehow. Or something. But that begs the question of why formulate this in terms of a function of a square root squared!?
Helpfully, they provide the definition in terms of the hypergeometric function a bit lower down, but that appears to be wrong as well, providing yet another result if evaluated numerically.
Print[ NIntegrate[ 1/(1 - Cos[x] Cos[y] Cos[z]), {x, 0, Pi}, {y, 0, Pi}, {z, 0, Pi}, Method -> "LocalAdaptive"] / Pi^3 // Timing]
{0.121543, 1.3932012917627028}
Print[ NIntegrate[ Pi Csc[x/2]^2 EllipticK[-Cos[x] Csc[x/2]^4], {x, 0, Pi}] / Pi^3 // Timing]
{0.021917, 1.3932039076998044}
Print[ Gamma[1/4]^4 / (4 Pi^3) // N // Timing]
{0.000029, 1.3932039296856769}
Print[ 4 / Pi^2 EllipticK[1/2]^2 // N // Timing]
{0.000375, 1.3932039296856764}
For `NIntegrate` the default method is `GlobalAdaptive`. You can try different methods and rules to optimize for the function and bounds.
It's a bit of a challenge to get either the first or second forms you provided to converge if requesting 10 or 15 digits of precision. However, your third form involving the Gamma function evaluates to very high numerical precision quickly. I can get 1,000 digits in under 50 milliseconds, which is "good enough"!
Your usage of NIntegrate tuning options shows a few things:
1) That these days I only use Mathematica as a glorified calculator, evoking a mental image of a 500-ton press being used to crack walnuts.
2) Even the best symbolic CAS in the world isn't magic, and requires hand-holding.
3) With the right knowledge even a very hard nut can be easily cracked!
I wonder why Wolfram Research hasn't added some basic multi-threading capabilities to Mathematica to try different "flags" in parallel, racing the various approaches on each CPU core to see which one wins...
If anyone is working on AI+programming languages, please send me a message. I'd love to work with others on this problem.
That would be great. If you could guess, how would you go about using symbolic math and neural nets to create a more abstract programming language?
If it could be used to greatly accelerate SMT solving/constraint solving, perhaps it would be possible to run a formal model as if it were code, i.e. fast and scalable constraint-based programming. That's about as high-level as you can get, short of a requirements document. I'm not sure if that's the kind of symbolic mathematics that's being studied here, as they seem to be looking at mathematically interesting expressions, rather than boring-but-enormous constraints.
Or, somewhat related, perhaps it could be used to help scale formal verification with languages like SPARK and ZZ.
To me, more exciting is some kind of joint collaboration between modern ml systems & formal solvers.
* Martin Vechev, ETH Zurich
* Dawn Song, University of California Berkeley
* Eran Yahav, Technion
* Miltiadis Allamanis, Microsoft Research Cambridge
If anyone knows other advisors looking for graduate students in this area, please let me know. Due to personal circumstances I can most likely not apply to ETH Zurich or Technion (I don't speak Hebrew anyway), which leaves me with only one potential advisor in a program that I really want.
There is also the Python writing model that Open AI showed recently at the Microsoft Build conference, so maybe there is some interest growing at other places as well.
I was also recently working on a deep learning decompiler but was unable to get my transformer model to learn well enough to actually decompile x64 assembly. I have the source code for the entire Linux kernel as training data, so it's not an issue with quantity. If anyone is interested in helping out with this project, please let me know in a comment.
Also general advice, after finding a few papers you like go through the papers they cite that are relevant to the subfield and also papers that cite them. That's one of the best ways of finding other related research that interests you.
* Swarat: https://blog.sigplan.org/2020/04/15/synthesizing-neurosymbol... <- probably heaviest on the math side wrt PL people
* Ras Bodik (Berkeley -> UW): esp. w/ Pedro Domingos and all the MSR collaborators (Sumit Gulwani, ...) <- a bit biased b/c I was in the group while at Berkeley; Ras + Dawn are crazy creative
* Percy Liang (Stanford): Coming from the ML side and w/ a long-running interest here
You should also check out professors at Ben Gurion University, Tel Aviv University and the Hebrew University who might have similar interests, IIRC. Feel free to hit me up if there's some page in Hebrew that doesn't translate well.
Linux kernel is only ~30M LOC. That's a really small dataset. For comparison, the reddit based dataset for GPT-2 is 100 times larger. Try using all C code posted on Github.
decompile x64 assembly
You can't "decompile" assembly. Either you decompile machine code, or you disassemble assembly code. The latter is easier than the former, so if you're trying to decompile executables, then perhaps you should train two models: one to convert machine code to assembly, and the other to convert assembly to C. Assembly code produced by an optimizing compiler might differ significantly from assembly code which closely corresponds to C code.
Is the step of going from machine code to gcc-produced assembly not trivial? Is gcc actually producing assembly code that an assembler needs to do more with than convert to the corresponding opcodes?
My colleagues and I run the SEFCOM lab at Arizona State University (https://sefcom.asu.edu/). Most relevant to your interests, Fish Wang (fellow SEFCOM professor) and I (Yan Shoshitaishvili) founded the angr program analysis framework (https://angr.io/) back in our gradschool days and have continued to evolve it together with our students in the course of our research at ASU. We're actually currently undertaking a concerted push into decompilation research, using both PL and ML techniques. This research direction is a passion of ours, and there's plenty of room for you here if you're interested!
Of course, we also do quite a bit of work in other areas of program analysis (including less overtly "mathy" techniques, like fuzzing) as well as other areas of cybersecurity. We are also quite active in the Capture the Flag community, if that is something that interests you!
Other places that do research in program analysis off the top of my head:
- Chris Kruegel (https://sites.cs.ucsb.edu/~chris/) and Giovanni Vigna (https://sites.cs.ucsb.edu/~vigna/) at UCSB (disclaimer: I got my PhD from them!)
- Davide Balzarotti (http://s3.eurecom.fr/~balzarot/) and Yanick Fratantonio (https://reyammer.io/) at EURECOM
- Antonio Bianchi (https://antoniobianchi.me/) (and, soon, Aravind Machiry) at Purdue
- Alexandros Kapravelos (https://kapravelos.com/) at NCSU
- Taesoo Kim (https://taesoo.kim/) at Georgia Tech
- Yeongjin Jang (https://www.unexploitable.systems/) at O(regon)SU
- Zhiqiang Lin (http://web.cse.ohio-state.edu/~lin.3021/) at O(hio)SU
- Brendan Dolan-Gavitt (https://engineering.nyu.edu/faculty/brendan-dolan-gavitt) at NYU
- Wil Robertson (https://wkr.io/) and Engin Kirda (https://www.ccs.neu.edu/home/ek/) at Northeastern
If you have questions about the PhD process or this research area, feel free to reach out: yans@asu.edu or @Zardus on twitter!
How theoretically feasible would it be to create Meta-AI.
My naive (incredibly over-simplified) notion goes something like this:
- You convert open-source code into a generic/universal AST/IR format, and figure out a means to represent function inputs and outputs (behavior)
- You use all of the OSS code in the world as data for this, to train a neural network to start making predictions about what kind of AST inputs in a program lead to what kinds of outputs (function synthesis)
- You tell the program to look at other deep learning/ML code, and to attempt to optimize it's own code, while running, inside of isolated processes/VM's.
Something like Erlang/Elixir or Lisp should be capable of this meta-programming and self-code modification while still running. And the BEAM would theoretically be able to isolate actors in the event that the epoch doesn't pan out very well and just kill that branch/lineage off.
Is this insane? I've wondered about this for years.
I think this alone is a herculean task.
https://en.wikipedia.org/wiki/Genetic_programming#Meta-genet...
Although it uses genetic programming instead of neural networks. Those approaches are equivalent in power, the difference is only that neural networks are more amenable to parallelization and we know a very good baseline optimization algorithm (gradient descent and friends).
The problem is that coming up with an optimizer/architecturer is hard. So the benefit of running a meta-optimizer to solve a problem is difficult to realize versus a handmade neural network. The problem needs to be so large the network would need to re-engineer itself to solve it -- but think how many resources have already been spent in engineering neural networks (by humans no less, which are quite powerful optimizers!). Unless the problem is truly titanic (w.r.t. other current problems) the yields might be small.
What you can do in a similar vein is gather a large set of problems and train a 'Neural architect' or something like that that then can be applied many times to new problems. This allows sharing this cost over many new networks. I think it could make sense for governments and large organizations to get together and create this sort of thing. If you know the costs of training a large neural network, imagine the cost of training hundreds of millions to train some kind of neural architect (NA).
There are milder versions of this, where the architecture search itself isn't trained:
https://en.wikipedia.org/wiki/Neural_architecture_search
https://en.wikipedia.org/wiki/Automated_machine_learning
Of course even this approach has limitations (even if you theoretically allow it to create essentially arbitrary architectures), because it will still have difficulty "thinking outside the box" like we do using huge amounts of mathematical expertise and intuition (see EfficientNet -- the insight in that paper would be difficult to arise from a NA network) -- it's not the thing that will solve all of our problem forever; but it would be pretty significant (perhaps towards making large AI-based systems with multiple components, say self-driving cars and robots of the future).
I really hope to see something happen in this area before I die, just for the sake of seeing it happen.
I often wonder about whether neural networks might need to meet at a crossroads with other techniques.
Inductive Logic/Answer Set Programming or Constraints Programming seems like it could be a good match for this field. Because from my ignorant understanding, you have a more "concrete" representation of a model/problem in the form of symbolic logic or constraints and an entirely abstract "black box" solver with neural networks. I have no real clue, but it seems like they could be synergistic?
There's a really oddball repo I found that took this approach:
https://github.com/921kiyo/symbolic-rl
"Symbolic Reinforcement Learning using Inductive Logic Programming"
No, in fact I belive some variant of this approach is what will eventually lead to AGI. (you can probably do a similar type of solution but approaching from the direction of neural networks where you can use backprop)
We are working both on synthesizing programs from scratch (see https://arxiv.org/abs/2002.09030 for example) and on understanding computer programs using machine learning (see e.g. https://arxiv.org/abs/1911.01205).
I'm always happy to correspond with people about these topics.
One topic which is feel is neglected is a good GCN (or any GNN) to operate on existing code trees. Most approaches seem to prefer seq or at most tree inputs.
Is this simply not finding yet a good network architecture, or is it a performance issue ?
They express everything in reverse polish notation, exactly so the transformer network can work on streams and not care about the nesting levels.
It's a bit odd that this article doesn't talk about that.
[1] https://arxiv.org/abs/1902.07282 (an AST translation system)
[2] https://arxiv.org/abs/1609.02907 (GCNN)
The AI approaches always had one great problem: if they can't find an integral you still have no idea whether an integral exists or not. The Risch algorithm, on the other hand, can tell you for sure if an (elementary) integral doesn't exist. Axiom is fully capable of saying "no", but can't always tell you what the integral is if it does exist.
Using an AST to represent expressions isn't novel, by the way. I implemented such a system as an undergrad computer science student (I also implemented complete integration of rational functions).
The problem was rather that they tested on the same distribution the model had just seen 80 million examples from.
That's the gem of the review.
> It goes without saying that LC has no understanding of the significance of an integral or a derivativeor even a function or a number. In fact, occasionally, it outputs a solution that is not even a well-formed expression. LC is like the worst possible student in a calculus class: it doesn’t understandthe concepts, it doesn’t learned the rules, it has no idea what is the significance of what it is doing,but it has looked at 80 million examples and gotten a feeling of what integrands and their integralslook like.
If I understand correctly, mathematical solutions can be verified, while neural network solutions would be very hard, if not impossible to verify in reasonable time.
For integration, you can just derive.
For infinitely many other problems... verification is way harder.
1) if you get a solution, can you be sure that it's right? in this case, the neural network might spit out a wrong solution to the integral. However, this solution is easy to verify by just differentiating (which they do in the paper), so I don't think there's a problem here.
2) will the method always return a good answer? I don't think this is a requirement; Mathematica sometimes fails to integrate but people accept that.
3) Does the method work for larger, more interesting families of functions than the limited families tried in the paper? I think this is what Gibou is talking about, and seems like the strongest objection. This technique might just fail in some circumstances for reasons that are hard to anticipate.
> [...] it only included equations with one variable, and only those based on elementary functions. “It was a thin slice of possible expressions,”
> The neural net wasn’t tested on messier functions often used in physics and finance, like error functions or Bessel functions. (The Facebook group said it could be, in future versions, with very simple modifications.)
> Other critics have noted that the Facebook group’s neural net doesn’t really understand the math; it’s more of an exceptional guesser.
> Still, they agree that the new approach will prove useful.
> Another unsolved problem where this approach shows promise is one of the most disturbing aspects of neural nets: No one really understands how they work. Training bits enter at one end and prediction bits emerge from the other, but what happens in between — the exact process that makes neural nets into such good guessers — remains a critical open question.
> Symbolic math, on the other hand, is decidedly less mysterious. “We know how math works,” said Charton. “By using specific math problems as a test to see where machines succeed and where they fail, we can learn how neural nets work.”
XOR and Spiral benchmark was studied in neural networks since 70's.
Considering neural networks are inherently maximizing probabilities and statistical descriptions of data, this should come as no surprise. This work has not dissolved the dichotomy between rules-based and statistical methods, but rather transmuted the syntax of rules-based expressions into a representation that can be exploited by statistical machines in a way that makes "guessing" more fruitful.
There are some examples near the end of the paper showing how the authors take an initially intractable expression and are able to simplify it with their approach so that Mathematica can actually perform the integral for them. It seems much more appropriate to market this method as a preprocessor for massive expressions to a more chewable size.
This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink a lot of time into formal verification.
The process is essentially: a) Find an interesting conjecture that you've got a strong guess to be true. b) Check for obvious (or less obvious) counterexamples, or conflicting theorems. c) Prove the thing is true.
A large part of the art of being a working mathematician is in part (a): you need to make a really good guess. An ideal conjecture is correct AND proveable AND leads to other interesting results, or says interesting things about bigger problems.
So what happens when we apply really good versions of current AI to this area? Picking out an 'interesting' conjecture is still Strong-AI-Complete: it requires lots of domain knowledge, and an understanding of what this particular conjecture would 'unlock.' But we could perhaps come up with good 'guessers' which quickly tell us whether a given idea might work out, perhaps saving a bunch of effort. Perhaps we could even get to the point of generating a proposed proof which can be fed to an automated proof checking system, allowing for inspection and modification by the human in the loop.
This quote seems to be massively misleading:
But it’s clear that the team has answered the decades-old question — can AI do symbolic math? — in the affirmative. “Their models are well established. The algorithms are well established. They postulate the problem in a clever way,” said Wojciech Zaremba, co-founder of the AI research group OpenAI.
“They did succeed in coming up with neural networks that could solve problems that were beyond the scope of the rule-following machine system,” McClelland said. “Which is very exciting.”
So best case this system gives black box answers that may or may not hold up in verification. That does not seem to be a very useful way to do mathematical research.
Going algorithmicly step by step is the clutches you use till you have built a strong enough intuition.
On issue I have with it, and that automated proof tools based on ML are going to have to solve, is that it's quite unpredictable. Even if it finds stunning proofs from time to time, it is hard to use an unpredictable tool efficiently.
Here is a gource visualization of metamath proofs overtime in the set.mm database: https://m.youtube.com/watch?v=LVGSeDjWzUo
Note that near the end, one of the contributors is OpenAI, who is not a human contributor.
Then you have http://www.scp-wiki.net/scp-914 for programs.
While working in enterprise I see plenty of code that after some massaging collapses into a much simpler form (for the programmer) and equivalent for the computer.
(fix typo)