In this post, I show that with some tooling help, current LLM reasoning models like Claude Sonnet and Opus can do some quite non-trival tasks, including formalizing mathematical proofs as well as producing code implementations with proofs of correctness.
Proving Alpha-Beta (Episode 2), Sorry Hammer and More | Lean4AI @ Gas Station Secret Lab
GasStationManager
Karma: 6
The next installment on my quest to get AIs to produce a correct implementation of Alpha-Beta with machine-checkable proof of correctness. This time featuring GPT 4.1 and o3. Guess who lies repeatedly...
Proving Alpha-Beta, Episode 1 | Lean4AI @ Gas Station Secret Lab
In a recent series of posts, I explore building a workflow for coding AIs that allows them to detect and recover from their hallucinations:
Property-Based Testing with Dependent Types: Experiment Alpha-Beta | Lean4AI @ Gas Station Secret Lab
Alpha-Beta with Claude Code | Lean4AI @ Gas Station Secret Lab
Alpha-Beta with Goose + Gemini | Lean4AI @ Gas Station Secret Lab
Experiments on Hallucination Detection and Recovery
In this initial post on Hallucination Detection and Recovery and follow-up, I explore the use of the interactive theorem prover Lean and its features to help LLMs detect and recover from hallucinations in solving coding tasks.
Any Lean enthusiasts here? You might be interested to check out Code with Proofs: the Arena. Test your Lean skills with our coding challenges!
Code for the website is open sourced at https://github.com/GasStationManager/CodeProofTheArena
I have written an essay “A Proposal for Safe and Hallucination-free Coding AI” (https://gasstationmanager.github.io/ai/2024/11/04/a-proposal.html), in which I propose an open-source collaboration on a research agenda that I believe will eventually lead to coding AIs that have superhuman-level ability, are hallucination-free, and safe.
Comments are welcome!
http://ProvablyCorrectVibeCoding.com
Vibe coding sometimes gets a bad rap, but I believe it reresents a fundamental desire: I have a brilliant idea, and want to turn that into something concrete that people can use. I know what I want to create but don’t have the programming expertise. Can my AI assistant help implement my idea into software?
However, vibe coding often doesn’t work, because current AIs hallucinate. Even with better and better AIs, vibe coding is unsafe, because a misaligned AI can easily sneak malicious code past the vibe coder.
What if, our AI assistant can produce code that is guaranteed to be safe and correct?
In this demo, you will be able to pose a coding task as a formal specification in Lean, a programming language and theorem prover. The formal specification will take the form of a signature of a function to be implemented, plus theorem statements about the function. Then, an AI coding agent will attempt to solve the task by implementing the function (in Lean) and proving the theorem statements (in Lean). Finally, you can verify whether the submitted solution is valid by sending it to the Lean proof checker. If the solution passes the proof checker, you now have runnable code that is guaranteed to be correct.