Fields Mathematical AI Seminar

AI works best exactly where success has a checkable criterion. Mathematics has proof checkers, and that is why AI is good at mathematics. Code has tests, but a test is a lossy proxy for what the person actually meant: in our experiments, at least 15 percent of AI-generated code that passed every test was provably wrong. This talk argues that the missing criterion for computing is proof, that AI has just removed the last obstacle to using it, and that this changes what programming is. I will cover three stages of one argument:

-Mathematics. Two foundational questions about matching logic, the logical foundation of the K Framework, which my group left open years ago and have now settled with AI as a genuine collaborator: global completeness of the basic logic, and the impossibility of any complete proof system once fixpoints are added.

• Code. Generating code together with its formal specification and a machine-checked proof connecting them, over executable formal semantics of real programming languages. The unexpected finding: asked for the specification and the proof as well, AI writes better code and solves more tasks. Like humans, it does better when it reflects.
• Intent Computing. Once every answer carries a proof of accomplishment, programming languages sink below the surface, the way assembly, registers, and memory management already did. What remains is human intent: a specification the human approves in their own words, and a fixed point, in Dana Scott’s sense, where intent, specification, code, and proof agree.

I recently founded Intent Computing Inc. to bring this to the real world.