This talk was recorded at Lambda Days in June 2024. If you’re curious about our upcoming event, check https://lambdadays.org
Everyone is talking about new advances in Artificial Intelligence (AI): texts written by ChatGPT, images drawn by Midjourney, and self-driving cars from Tesla.
When I was a sophmore I learned the fundamentals of my subject from John McCarthy, a founders of AI and a pioneer of programming. In the early days, AI debated the merits of two complementary methods: logic vs heuristics. Typical of the first is proving properties of programs, which became my research interest. Typical of the second is machine learning, the foundation of ChatGPT, Midjourney, and self-driving.
This talk will contrast the two approaches, discussing the benefits and risks of each, and how the first may curb shortcomings of the second.
Artists and writers are worried that AI will put them out of a job. One of the next professions on the list is programmers. Already, ChatGPT and related systems can do a credible job of generating simple programs, such as code for web pages. However, also already, such systems have demonstrated that they routinely write code containing known security bugs.
One possible scenario is that heuristic techniques will prove as adequate as humans—and far cheaper—at simple tasks, putting writers, artists, and programmers out of work. Bereft of new data to learn from, the machine learning applications will then fall into stagnation. They will be fine at producing articles, art, and code close to what has been produced before, but unable to produce anything original. And by then there may no longer be writers, artists, or programmers to hire, as who would study for a profession where no one can find work because they’ve been displaced by machines?
A different scenario is to pass laws to ensure that writers and artists are fairly recompensed when AI generates artifacts based on their work. Regarding code, the logical techniques have shown they can vastly improve reliability. Synthesising logical and heuristic techniques may lead to code that is both cheaper and more reliable. Programmers would shift from writing code to writing logical specifications, with AI helping to generate code proved to meet those specifications.
REFERENCES
AI machines aren’t ‘hallucinating’, but their makers are. Naomi Klein. The Guardian, 8 May 2023.
AI machines aren’t ‘hallucinating’. But their makers are | Naomi Klein | The Guardian
The problem with counterfeit people. Daniel Dennett. The Atlantic, 16 May 2023.
The Problem With Counterfeit People - The Atlantic
Will AI become the new McKinsey? Ted Chiang. The New Yorker (online), 4 May 2023.
Will A.I. Become the New McKinsey? | The New Yorker
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, July 2009, 52(7), pages 107–115. https://dl.acm.org/doi/pdf/10.1145/1538788.1538814
Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff. How Amazon Web Services Uses Formal Methods. Communications of the ACM, April 2015, 58(4), pages 66–73. https://dl.acm.org/doi/pdf/10.1145/2699417
