On Monday, August 19, 2024 at 2:34:15 a.m. UTC+2 syle...@gmail.com wrote:
AI achieves silver-medal standard solving International Mathematical Olympiad problems - Google DeepMind <https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/> 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 am a bit skeptical about claims from closed source software developed by big tech. Does that code really generalize or has it been optimized for that specific task? So far, project numina <https://projectnumina.ai/> has won a Kaggle competition <https://www.kaggle.com/competitions/ai-mathematical-olympiad-prize/>about solving Math Olympiad problems with AI... and they won by generating SymPy code to solve the problems... (maybe I'll open a separate thread on this). 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. Maybe we could use AI to generate our algorithms, though I believe this is a really hard task. Current LLMs are good at tasks they have seen in their training dataset, they are not that good when you try to generalize on algorithms they have never seen. But... can we try to set up an agent that generates the nodes of the Risch algorithm by repeatedly interacting with an LLM and feeding it with the proper literature and giving the LLM proper feedback to correct the code it's generated so far? 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. That's a good question. LLMs can do most of the coding stuff, but one should always be careful that the generated code may be wrong, so experience is still required. Furthermore, in corporations software engineers usually spend a lot of time discussion project ideas with business, dealing the security policy / legal auditing of software, bureaucracy to request database access and understanding the mess you find in databases, privacy regulation concerns and so on. It's not just writing code... these jobs will survive AI code generators. 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 will take some time, many developers still aren't used to using AI. It also seems to be deprecating code sharing efforts for open source communities, because code can be generated rather than shared. AI can help you to find other projects that are developing something useful for you. In many cases, people don't use the proper open source tool because they are not aware of its existence. -- 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/5cd788bd-c09e-42bb-a28b-6da812a08c57n%40googlegroups.com.
