Is hallucination-free AI code possible? (kucharski.substack.com)

In July 2024, DeepMind showcased its AlphaProof and AlphaGeometry models, which successfully solved four out of six problems from the prestigious International Mathematical Olympiad (IMO), marking a significant milestone in AI's capability to tackle complex mathematical challenges. This achievement illustrates the potential for AI to not only operate within mathematical logic but also suggests that similar methods could be extended to other areas like computer programming, raising questions about the feasibility of "hallucination-free" AI-generated code. The process involved translating problems into a formal mathematical representation using the Lean language, allowing AlphaProof to construct proofs in a clear, machine-verifiable format. While initial AI outputs in coding may run without errors, the transition to evaluating "correct" code introduces complexities. Researchers propose several automated checks—from basic operational correctness to more nuanced qualitative assessments, ensuring models behave as expected. Despite advancements, achieving truly robust models necessitates more than structural checks; it requires understanding the underlying assumptions and design decisions made by the AI—highlighting the ongoing interplay between human oversight and machine learning in complex tasks.