https:\/\/deepmind.google\/discover\/blog\/ai-solves-imo-problems-at-silver-medal-level\/<\/a><\/p>\n(…)<\/p>\n
AlphaProof: a formal approach to reasoning<\/p>\n
AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go.<\/p>\n
Formal languages offer the critical advantage that proofs involving mathematical reasoning can be formally verified for correctness. Their use in machine learning has, however, previously been constrained by the very limited amount of human-written data available.<\/p>\n
In contrast, natural language based approaches can hallucinate plausible but incorrect intermediate reasoning steps and solutions, despite having access to orders of magnitudes more data. We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty.<\/p>\n
When presented with a problem, AlphaProof generates solution candidates and then proves or disproves them by searching over possible proof steps in Lean. Each proof that was found and verified is used to reinforce AlphaProof\u2019s language model, enhancing its ability to solve subsequent, more challenging problems.<\/p>\n
We trained AlphaProof for the IMO by proving or disproving millions of problems, covering a wide range of difficulties and mathematical topic areas over a period of weeks leading up to the competition. The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found….<\/p>\n","protected":false},"excerpt":{"rendered":"
*It plays Go, only instead it does math. More-or-less. https:\/\/deepmind.google\/discover\/blog\/ai-solves-imo-problems-at-silver-medal-level\/ (…) AlphaProof: a formal approach to reasoning AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of […]<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-4851","post","type-post","status-publish","format-standard","hentry","category-uncategorised"],"yoast_head":"\n
AlphaProof | Artmaker Blog<\/title>\n<meta name=\"description\" content=\"AlphaProof | Artmaker Blog\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/\" \/>\n<meta property=\"og:locale\" content=\"en_GB\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"AlphaProof | Artmaker Blog\" \/>\n<meta property=\"og:description\" content=\"AlphaProof | Artmaker Blog\" \/>\n<meta property=\"og:url\" content=\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/\" \/>\n<meta property=\"og:site_name\" content=\"Artmaker Blog\" \/>\n<meta property=\"article:published_time\" content=\"2024-07-31T08:42:03+00:00\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Bruce Sterling\" \/>\n\t<meta name=\"twitter:label2\" content=\"Estimated reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebSite\",\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/#website\",\"url\":\"https:\/\/toshareproject.it\/artmakerblog\/\",\"name\":\"Artmaker Blog\",\"description\":\"on Toshareproject.it - curated by Bruce Sterling\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/toshareproject.it\/artmakerblog\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-GB\"},{\"@type\":\"WebPage\",\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/#webpage\",\"url\":\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/\",\"name\":\"AlphaProof | Artmaker Blog\",\"isPartOf\":{\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/#website\"},\"datePublished\":\"2024-07-31T08:42:03+00:00\",\"dateModified\":\"2024-07-31T08:42:03+00:00\",\"author\":{\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/#\/schema\/person\/6f20726ed2761431f3e0ff4e096c3085\"},\"description\":\"AlphaProof | Artmaker Blog\",\"breadcrumb\":{\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/#breadcrumb\"},\"inLanguage\":\"en-GB\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/toshareproject.it\/artmakerblog\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"AlphaProof\"}]},{\"@type\":\"Person\",\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/#\/schema\/person\/6f20726ed2761431f3e0ff4e096c3085\",\"name\":\"Bruce Sterling\",\"image\":{\"@type\":\"ImageObject\",\"@id\":\"https:\/\/toshareproject.it\/artmakerblog\/#personlogo\",\"inLanguage\":\"en-GB\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/c390e8ed4db57a34278dcf667f928a643cf769a865c8a8632dcd310412bb9a99?s=96&d=mm&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/c390e8ed4db57a34278dcf667f928a643cf769a865c8a8632dcd310412bb9a99?s=96&d=mm&r=g\",\"caption\":\"Bruce Sterling\"},\"description\":\"Art director at Share Festival, author and journalist\",\"sameAs\":[\"http:\/\/toshareproject.it\/tomorrowart\"],\"url\":\"https:\/\/toshareproject.it\/artmakerblog\/author\/brucesterling\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"AlphaProof | Artmaker Blog","description":"AlphaProof | Artmaker Blog","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/","og_locale":"en_GB","og_type":"article","og_title":"AlphaProof | Artmaker Blog","og_description":"AlphaProof | Artmaker Blog","og_url":"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/","og_site_name":"Artmaker Blog","article_published_time":"2024-07-31T08:42:03+00:00","twitter_card":"summary_large_image","twitter_misc":{"Written by":"Bruce Sterling","Estimated reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebSite","@id":"https:\/\/toshareproject.it\/artmakerblog\/#website","url":"https:\/\/toshareproject.it\/artmakerblog\/","name":"Artmaker Blog","description":"on Toshareproject.it - curated by Bruce Sterling","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/toshareproject.it\/artmakerblog\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-GB"},{"@type":"WebPage","@id":"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/#webpage","url":"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/","name":"AlphaProof | Artmaker Blog","isPartOf":{"@id":"https:\/\/toshareproject.it\/artmakerblog\/#website"},"datePublished":"2024-07-31T08:42:03+00:00","dateModified":"2024-07-31T08:42:03+00:00","author":{"@id":"https:\/\/toshareproject.it\/artmakerblog\/#\/schema\/person\/6f20726ed2761431f3e0ff4e096c3085"},"description":"AlphaProof | Artmaker Blog","breadcrumb":{"@id":"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/#breadcrumb"},"inLanguage":"en-GB","potentialAction":[{"@type":"ReadAction","target":["https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/toshareproject.it\/artmakerblog\/alphaproof\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/toshareproject.it\/artmakerblog\/"},{"@type":"ListItem","position":2,"name":"AlphaProof"}]},{"@type":"Person","@id":"https:\/\/toshareproject.it\/artmakerblog\/#\/schema\/person\/6f20726ed2761431f3e0ff4e096c3085","name":"Bruce Sterling","image":{"@type":"ImageObject","@id":"https:\/\/toshareproject.it\/artmakerblog\/#personlogo","inLanguage":"en-GB","url":"https:\/\/secure.gravatar.com\/avatar\/c390e8ed4db57a34278dcf667f928a643cf769a865c8a8632dcd310412bb9a99?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/c390e8ed4db57a34278dcf667f928a643cf769a865c8a8632dcd310412bb9a99?s=96&d=mm&r=g","caption":"Bruce Sterling"},"description":"Art director at Share Festival, author and journalist","sameAs":["http:\/\/toshareproject.it\/tomorrowart"],"url":"https:\/\/toshareproject.it\/artmakerblog\/author\/brucesterling\/"}]}},"_links":{"self":[{"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/posts\/4851","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/comments?post=4851"}],"version-history":[{"count":1,"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/posts\/4851\/revisions"}],"predecessor-version":[{"id":4852,"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/posts\/4851\/revisions\/4852"}],"wp:attachment":[{"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/media?parent=4851"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/categories?post=4851"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/toshareproject.it\/artmakerblog\/wp-json\/wp\/v2\/tags?post=4851"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}