> ChatGPT Premium uses SymPy as a backend if asked to do mathematical tasks because a computer algebra system is guaranteed to be correct.
Actually, the reason that ChatGPT still depends on SymPy on some feature, but Google may not cited SymPy, over Lean or other solution is something we should definitely worry about influence though, if Google engineers had decided their own reason to not use algebraic steps of SymPy because it can be slow, buggy, or difficult to customize, or they even had skipped any usage of computer algebra systems, and connect Lean and AI system directly to achieve same algebraic system. On Monday, August 19, 2024 at 10:22:27 PM UTC+2 Oscar wrote: > It is a lot easier to use a computer algebra system than lean but the > goals are different. I was thinking about the idea of making an AI > that could talk to a theorem prover like lean. The idea would be that > you have an AI that hallucinates lots of proofs that may or may not be > correct but then you filter out the correct ones with lean. Then the > answer given to the user is generated by the generative AI but also > proven correct by the theorem prover. It is also presumably > straight-foward to train a generative AI that writes proofs if you can > score its output with a theorem prover. > > I haven't read the cited paper yet but it sounds like they have done > something similar to what I was imagining. The flip side is that > suddenly lean becomes a much easier thing to use because you don't > have to write the lean code yourself: the AI does it and translates > the results to/from natural language. Then you're using the theorem > prover for proving theorems and a computer algebra system for doing > algebra and the large language model can focus on language-based tasks > as it should. The LLM doesn't replace lean/SymPy: it uses them much > like humans do. > > On Mon, 19 Aug 2024 at 20:19, Maaz Muhammad <[email protected]> wrote: > > > > "research reinforces that solve or simplify, or integral is losing > competition" > > > > I really don't think so. It's way easier to use a computer algebra > system to do the things that these functions do than use Lean. Every step > in Lean has to be "handwritten" by the user as its an interactive theorem > prover, i.e. it has to be justified by some appeal to a ring axiom or > something. Simplifying algebraic expressions in Lean is much more tedious > than just calling "simplify" in SymPy because SymPy will do a lot of things > automatically. As well, Lean works by using "goals", i.e. you have to > pre-specify the end result, as its made to prove theorems. Much more could > be said but overall my point is that Lean and SymPy are meant for different > purposes. > > > > And for what it's worth, ChatGPT Premium uses SymPy as a backend if > asked to do mathematical tasks because a computer algebra system is > guaranteed to be correct. > > On Sunday, August 18, 2024 at 11:26:52 PM UTC-4 [email protected] > wrote: > >> > >> I am not a trained mathematician. > >> My question: would Gödel's incompleteness theorem not set a limit to > what can be proven 'automatically'? > >> > >> [email protected] schrieb am Montag, 19. August 2024 um 02:34:15 UTC+2: > >>> > >>> 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 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. > >>> > >>> 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. > > > > -- > > 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 [email protected]. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/sympy/dda943a9-f23d-41b4-9014-5b5cd50c0f70n%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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/e0b6a2aa-7fbb-478e-9261-e4bf162c3652n%40googlegroups.com.
