Cadence lance l’IA g\u00e9n\u00e9rative pour la conception de circuits imprim\u00e9s<\/a><\/li>\n<\/ul>\n\u00ab\u00a0Nous nous sommes malheureusement habitu\u00e9s \u00e0 ce que nos logiciels soient bogu\u00e9s, bien qu’ils soient omnipr\u00e9sents et que nous les utilisions tous quotidiennement\u00a0\u00bb, explique Yuriy Brun (ci-dessus, \u00e0 droite), professeur au Manning College of Information and Computer Sciences de l’UMass Amherst.<\/p>\n
Les bogues dans les logiciels peuvent \u00eatre potentiellement catastrophiques lorsqu’il s’agit de failles de s\u00e9curit\u00e9 ou de logiciels de pr\u00e9cision utilis\u00e9s pour l’exploration spatiale ou pour contr\u00f4ler les appareils de soins de sant\u00e9.<\/p>\n
Les m\u00e9thodes formelles pour des logiciels sans bogues peuvent g\u00e9n\u00e9rer une preuve math\u00e9matique montrant que le code fait ce qu’il est cens\u00e9 faire, puis utiliser un prouveur de th\u00e9or\u00e8me pour s’assurer que la preuve est \u00e9galement correcte.<\/p>\n
Mais la r\u00e9daction manuelle de ces preuves prend \u00e9norm\u00e9ment de temps et n\u00e9cessite une grande expertise. \u00ab\u00a0Ces preuves peuvent \u00eatre plusieurs fois plus longues que le code du logiciel lui-m\u00eame\u00a0\u00bb, explique Emily First (ci-dessus), l’auteur principal de l’article, qui a effectu\u00e9 cette recherche dans le cadre de sa th\u00e8se de doctorat \u00e0 l’UMass Amherst.<\/p>\n
Un mod\u00e8le de langage \u00e9tendu est un moyen possible de g\u00e9n\u00e9rer automatiquement de telles preuves.<\/p>\n
Cependant, \u00ab\u00a0l’un des plus grands d\u00e9fis des LLM est qu’ils ne sont pas toujours corrects\u00a0\u00bb, d\u00e9clare M. Brun. \u00ab\u00a0Au lieu de se planter et de vous faire savoir que quelque chose ne va pas, ils ont tendance \u00e0 ‘\u00e9chouer silencieusement’, en produisant une r\u00e9ponse incorrecte mais en la pr\u00e9sentant comme si elle \u00e9tait correcte. Or, souvent, la pire chose \u00e0 faire est d’\u00e9chouer silencieusement\u00a0\u00bb.<\/p>\n
L’\u00e9quipe a utilis\u00e9 Minerva, un LLM form\u00e9 sur un vaste corpus de textes en langue naturelle, puis l’a affin\u00e9 sur 118 Go d’articles scientifiques math\u00e9matiques et de pages web contenant des expressions math\u00e9matiques.<\/p>\n
Ensuite, le LLM a \u00e9t\u00e9 affin\u00e9 sur un langage, appel\u00e9 Isabelle\/HOL, dans lequel les preuves math\u00e9matiques sont \u00e9crites. Baldur a ensuite g\u00e9n\u00e9r\u00e9 une preuve compl\u00e8te et a travaill\u00e9 en tandem avec le prouveur de th\u00e9or\u00e8mes pour v\u00e9rifier son travail.<\/p>\n
Lorsque le prouveur de th\u00e9or\u00e8mes a d\u00e9tect\u00e9 une erreur, il a renvoy\u00e9 la preuve, ainsi que les informations relatives \u00e0 l’erreur, au LLM, afin qu’il puisse tirer les le\u00e7ons de son erreur et g\u00e9n\u00e9rer une nouvelle preuve, que l’on esp\u00e8re exempte d’erreurs.<\/p>\n
Ce processus permet d’obtenir une am\u00e9lioration remarquable de la pr\u00e9cision. L’outil de pointe pour la g\u00e9n\u00e9ration automatique de preuves s’appelle Thor, qui peut g\u00e9n\u00e9rer des preuves dans 57 % des cas. Lorsque Baldur (le fr\u00e8re de Thor, selon la mythologie nordique) est associ\u00e9 \u00e0 Thor, les deux peuvent g\u00e9n\u00e9rer des preuves dans 65,7 % des cas.<\/p>\n
Bien qu’il y ait encore un grand nombre d’erreurs, Baldur est de loin le moyen le plus efficace et le plus performant jamais con\u00e7u pour v\u00e9rifier l’exactitude d’un logiciel exempt de bogues.<\/p>\n
www.umass.edu<\/a><\/p>\n <\/p>\n","protected":false},"excerpt":{"rendered":"
Des chercheurs am\u00e9ricains ont mis au point une m\u00e9thode de v\u00e9rification automatique des logiciels avec un taux d’efficacit\u00e9 de pr\u00e8s de 66 % en utilisant de grands mod\u00e8les linguistiques LLM. L’\u00e9quipe d’informaticiens dirig\u00e9e par l’universit\u00e9 du Massachusetts Amherst a mis au point une m\u00e9thode permettant de g\u00e9n\u00e9rer automatiquement des preuves compl\u00e8tes qui peuvent \u00eatre utilis\u00e9es […]<\/p>\n","protected":false},"author":2,"featured_media":440548,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[883],"tags":[4039,4603],"domains":[47],"ppma_author":[3640],"class_list":["post-440561","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-technologies","tag-ia-generative","tag-llm-fr","domains-electronique-eci"],"acf":[],"yoast_head":"
L'IA g\u00e9n\u00e9rative permet de supprimer les bogues ...<\/title>\n<meta name=\"description\" content=\"Une \u00e9quipe du Massachusetts Amherst a mis au point la m\u00e9thode Baldur pour g\u00e9n\u00e9rer des preuves compl\u00e8tes de logiciels sans bogues.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts\/440561\/\" \/>\n<meta property=\"og:locale\" content=\"fr_FR\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"L'IA g\u00e9n\u00e9rative permet de supprimer les bogues\" \/>\n<meta property=\"og:description\" content=\"Une \u00e9quipe du Massachusetts Amherst a mis au point la m\u00e9thode Baldur pour g\u00e9n\u00e9rer des preuves compl\u00e8tes de logiciels sans bogues.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts\/440561\/\" \/>\n<meta property=\"og:site_name\" content=\"EENewsEurope\" \/>\n<meta property=\"article:published_time\" content=\"2024-01-07T15:04:52+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2024-01-07T15:06:39+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.eenewseurope.com\/wp-content\/uploads\/2024\/01\/First.Brun-collage-e1704485179504.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"700\" \/>\n\t<meta property=\"og:image:height\" content=\"453\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"author\" content=\"Nick Flaherty\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"NicolasR\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"3 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/#article\",\"isPartOf\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/\"},\"author\":{\"name\":\"NicolasR\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/person\/78961bf5e4a331d3b8b2d58fdfef976c\"},\"headline\":\"L’IA g\u00e9n\u00e9rative permet de supprimer les bogues\",\"datePublished\":\"2024-01-07T15:04:52+00:00\",\"dateModified\":\"2024-01-07T15:06:39+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/\"},\"wordCount\":731,\"publisher\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#organization\"},\"keywords\":[\"IA g\u00e9n\u00e9rative\",\"LLM\"],\"articleSection\":[\"Technologies\"],\"inLanguage\":\"fr-FR\"},{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/\",\"url\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/\",\"name\":\"L'IA g\u00e9n\u00e9rative permet de supprimer les bogues -\",\"isPartOf\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#website\"},\"datePublished\":\"2024-01-07T15:04:52+00:00\",\"dateModified\":\"2024-01-07T15:06:39+00:00\",\"description\":\"Une \u00e9quipe du Massachusetts Amherst a mis au point la m\u00e9thode Baldur pour g\u00e9n\u00e9rer des preuves compl\u00e8tes de logiciels sans bogues.\",\"breadcrumb\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/#breadcrumb\"},\"inLanguage\":\"fr-FR\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/test.eenewseurope.com\/fr\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"L’IA g\u00e9n\u00e9rative permet de supprimer les bogues\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#website\",\"url\":\"https:\/\/www.eenewseurope.com\/fr\/\",\"name\":\"EENewsEurope\",\"description\":\"Just another WordPress site\",\"publisher\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.eenewseurope.com\/fr\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"fr-FR\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#organization\",\"name\":\"EENewsEurope\",\"url\":\"https:\/\/www.eenewseurope.com\/fr\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/www.ecinews.fr\/wp-content\/uploads\/2022\/02\/logo-1.jpg\",\"contentUrl\":\"https:\/\/www.ecinews.fr\/wp-content\/uploads\/2022\/02\/logo-1.jpg\",\"width\":283,\"height\":113,\"caption\":\"EENewsEurope\"},\"image\":{\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/logo\/image\/\"}},{\"@type\":\"Person\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/person\/78961bf5e4a331d3b8b2d58fdfef976c\",\"name\":\"NicolasR\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/person\/image\/1113513d73c6c997fc7ac1ecedfff8d9\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/8c46107760468ab8a00c814c26c19ab4?s=96&d=mm&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/8c46107760468ab8a00c814c26c19ab4?s=96&d=mm&r=g\",\"caption\":\"NicolasR\"}}]}<\/script>","yoast_head_json":{"title":"L'IA g\u00e9n\u00e9rative permet de supprimer les bogues ...","description":"Une \u00e9quipe du Massachusetts Amherst a mis au point la m\u00e9thode Baldur pour g\u00e9n\u00e9rer des preuves compl\u00e8tes de logiciels sans bogues.","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:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts\/440561\/","og_locale":"fr_FR","og_type":"article","og_title":"L'IA g\u00e9n\u00e9rative permet de supprimer les bogues","og_description":"Une \u00e9quipe du Massachusetts Amherst a mis au point la m\u00e9thode Baldur pour g\u00e9n\u00e9rer des preuves compl\u00e8tes de logiciels sans bogues.","og_url":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts\/440561\/","og_site_name":"EENewsEurope","article_published_time":"2024-01-07T15:04:52+00:00","article_modified_time":"2024-01-07T15:06:39+00:00","og_image":[{"width":700,"height":453,"url":"https:\/\/www.eenewseurope.com\/wp-content\/uploads\/2024\/01\/First.Brun-collage-e1704485179504.jpg","type":"image\/jpeg"}],"author":"Nick Flaherty","twitter_card":"summary_large_image","twitter_misc":{"Written by":"NicolasR","Est. reading time":"3 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/#article","isPartOf":{"@id":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/"},"author":{"name":"NicolasR","@id":"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/person\/78961bf5e4a331d3b8b2d58fdfef976c"},"headline":"L’IA g\u00e9n\u00e9rative permet de supprimer les bogues","datePublished":"2024-01-07T15:04:52+00:00","dateModified":"2024-01-07T15:06:39+00:00","mainEntityOfPage":{"@id":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/"},"wordCount":731,"publisher":{"@id":"https:\/\/www.eenewseurope.com\/fr\/#organization"},"keywords":["IA g\u00e9n\u00e9rative","LLM"],"articleSection":["Technologies"],"inLanguage":"fr-FR"},{"@type":"WebPage","@id":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/","url":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/","name":"L'IA g\u00e9n\u00e9rative permet de supprimer les bogues -","isPartOf":{"@id":"https:\/\/www.eenewseurope.com\/fr\/#website"},"datePublished":"2024-01-07T15:04:52+00:00","dateModified":"2024-01-07T15:06:39+00:00","description":"Une \u00e9quipe du Massachusetts Amherst a mis au point la m\u00e9thode Baldur pour g\u00e9n\u00e9rer des preuves compl\u00e8tes de logiciels sans bogues.","breadcrumb":{"@id":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/#breadcrumb"},"inLanguage":"fr-FR","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.eenewseurope.com\/fr\/lia-generative-permet-de-supprimer-les-bogues\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/test.eenewseurope.com\/fr\/"},{"@type":"ListItem","position":2,"name":"L’IA g\u00e9n\u00e9rative permet de supprimer les bogues"}]},{"@type":"WebSite","@id":"https:\/\/www.eenewseurope.com\/fr\/#website","url":"https:\/\/www.eenewseurope.com\/fr\/","name":"EENewsEurope","description":"Just another WordPress site","publisher":{"@id":"https:\/\/www.eenewseurope.com\/fr\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.eenewseurope.com\/fr\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"fr-FR"},{"@type":"Organization","@id":"https:\/\/www.eenewseurope.com\/fr\/#organization","name":"EENewsEurope","url":"https:\/\/www.eenewseurope.com\/fr\/","logo":{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/logo\/image\/","url":"https:\/\/www.ecinews.fr\/wp-content\/uploads\/2022\/02\/logo-1.jpg","contentUrl":"https:\/\/www.ecinews.fr\/wp-content\/uploads\/2022\/02\/logo-1.jpg","width":283,"height":113,"caption":"EENewsEurope"},"image":{"@id":"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/logo\/image\/"}},{"@type":"Person","@id":"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/person\/78961bf5e4a331d3b8b2d58fdfef976c","name":"NicolasR","image":{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.eenewseurope.com\/fr\/#\/schema\/person\/image\/1113513d73c6c997fc7ac1ecedfff8d9","url":"https:\/\/secure.gravatar.com\/avatar\/8c46107760468ab8a00c814c26c19ab4?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/8c46107760468ab8a00c814c26c19ab4?s=96&d=mm&r=g","caption":"NicolasR"}}]}},"authors":[{"term_id":3640,"user_id":0,"is_guest":1,"slug":"nick-flaherty","display_name":"Nick Flaherty","avatar_url":"https:\/\/secure.gravatar.com\/avatar\/?s=96&d=mm&r=g","0":null,"1":"","2":"","3":"","4":"","5":"","6":"","7":"","8":""}],"_links":{"self":[{"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts\/440561"}],"collection":[{"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/comments?post=440561"}],"version-history":[{"count":0,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/posts\/440561\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/media\/440548"}],"wp:attachment":[{"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/media?parent=440561"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/categories?post=440561"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/tags?post=440561"},{"taxonomy":"domains","embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/domains?post=440561"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/www.ecinews.fr\/fr\/wp-json\/wp\/v2\/ppma_author?post=440561"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}