On Sun, Aug 18, 2024 at 6:34 PM Sangyub Lee <sylee...@gmail.com> wrote: > > AI achieves silver-medal standard solving International Mathematical Olympiad > problems - Google DeepMind > > Recently, Google had announced the result that their AI model, AlphaProof and > AlphaGeometry can silver medal in IMO problems. Their system is hybrid of > symbolic models, and uses proof assistant Lean as backend, which guarantees > that the proof can be verified automatically. > ChatGPT had many problems that it can hallucinate the steps of proof, and > keep human verifying their result, as well as understaing the steps, so > expressing proof as formal proof statements is a gain. > > I think that the research reinforces that solve or simplify, or integral is > losing competition. Because a lot of them are written with heuristics that > won't win with AI, and we also have concerns about code around them are > getting messy. > > I think that if we want to avoid the losing competition, and make AI systems > work collaborative, symbolic computation should be focused to solve only a > few 'formal' problems in 100% precision and speed.
I tend to agree. I think there's really two types of computing, precise computing and fuzzy computing. The traditional computing paradigm is precise, where the computer computes exactly what it is told to and always gives the exact same answer. This works really well for problems where there is an exact correct answer. For example, computing arithmetic falls into this category because there is only one correct answer to . Fuzzy computing is where there isn't necessarily a single "correct" answer, and the "best" thing that could be returned is subjective. This has traditionally been done by applying heuristics on top of precise computing, but with the advent of machine learning and now more advanced AI models, one can often get results that are better than any possible precisely defined heuristic. Many language and image processing tasks fall into this category, which is why those are the most popular uses of AI models. But there are also a lot of "heuristics" that get applied even in a computer algebra system. For example, to compute an indefinite integral of a function f(x), one just needs to "guess" somehow a function g(x) such that g'(x) = f(x) (or more generally, guess an ansatz g(x, a1, ..., an) with (typically linear) parameters a1, ..., an such that the parameters a1, ..., an can be solved in the equation d/dx g(x, a1, ..., an) = f(x)). There are precise algorithms for making these guesses in cases where f(x) has a specific form (for example, Risch applies whenever g(x) is elementary), and one can definitely use smart mathematics to make better guesses. But there's also an "art" to guessing that can't really be encoded in heuristics. But a sufficiently trained AI model could learn this art and potentially make better guesses. The great thing about indefinite integration is that it doesn't matter how you get your "guess" g(x). As long as it differentiates back to f(x), you know it's the correct answer. This also applies to other types of problems where heuristics are applied like solving equations, solving ODEs, and simplification. So I would say that SymPy should focus on the "precise" parts of symbolic computing, i.e., the parts that you would use to actually verify the output of an AI model. Maybe one day a theorem prover like Lean will be able to do all of this and SymPy won't be needed. That would be hard to achieve, though, because Lean is a formal theorem prover, so everything in it has to be completely mathematically correct down to the last detail. A symbolic system like SymPy is much more lenient. For example, SymPy can sometimes return an expression that is only technically correct for some subset of the input domain because of things like division by 0 or branch cuts. In Lean, you'd have to formally account for all these cases for the proof to verify. With that being said, some algorithms like the Risch algorithm, and even some of the more sophisticated heuristic type algorithms in SymPy are still useful because they employ more sophisticated mathematical knowledge than just plain guessing. A good AI model would more or less have to internalize the equivalent of Risch to match its performance, for instance. I'm also hopeful that AI systems can benefit the development of SymPy itself. I was happy to see that SymPy was one of the projects whose issues are part of the SWE-Bench dataset, which is a dataset to benchmark how well AI systems can solve real issues in open source projects. If a bot can automatically produce fixes for some of the more trivial SymPy issues that could improve the quality of the code. (But it needs to be done in a way that is done with human intervention, not by just spamming AI generated PRs. It needs to reduce maintainer time and energy, not increase it) > > I already notice that there is research to connect Wu's method to > AlphaGeometry > [2404.06405] Wu's Method can Boost Symbolic AI to Rival Silver Medalists and > AlphaGeometry to Outperform Gold Medalists at IMO Geometry (arxiv.org) > Although symbolic system would no longer competitive solution to general math > problems, the 'formal' symbolic systems can still be valued. (I also hear > that AlphaGeometry2 is using Wu's method, but I'm trying to verify the > sources) > > I also think that such advances in AI systems can raise concerns about > software engineering careers, or educational system, which may be interesting > for some readers in the forum. > > For example, math exams can be pointless in the future, even to identify and > train good science or engineers in the future, because trained AI models can > beat IMO. I think that in AI age, the education should change, such that it > is not bearing through boring and repetitive systems, which does not even > reflect the capability of future engineers or scientists. It can still be worth it for people to learn mathematics, because it provides a better understanding of the world. Just as we still teach children how to do addition and multiplication, even though pocket calculators have existed for decades. > > Also, I notice that software engineering is changing, because AI models can > complete a lot of code, and precision is improving, or people are improving > the skills of prompting. > It also seems to be deprecating code sharing efforts for open source > communities, because code can be generated rather than shared. It certainly hasn't reached that point yet. I think the reasons for code sharing still apply even in a world where AI could rewrite an entire framework from scratch. For instance, common code and protocols allow systems to communicate with one another. At the same time, there are a lot of software systems that are very centralized right now because they are effectively the only real option. For example, everyone on this thread (so far) uses Gmail as their email system. If AI means that things can become more decentralized, I think that would ultimately be a good thing. Aaron Meurer > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sympy+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sympy/e7898bdb-d1e4-49fd-94c7-66ba8a840511n%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6LwOJYXqGw_ZCVzy-r63rk%2B-UvQSEv5F8DdTVovmy21cw%40mail.gmail.com.
