東華大學圖書館 |

語系: 繁體中文

說明(常見問題)

回圖書館首頁

手機版館藏查詢

登入

回首頁

切換: 標籤 | MARC模式 | ISBD

FindBook

Google Book

Amazon

博客來

Learning and Logic for Formal Synthesis.

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Learning and Logic for Formal Synthesis./
作者:	Caulfield, Benjamin.
出版者:	Ann Arbor : ProQuest Dissertations & Theses, : 2021,
面頁冊數:	89 p.
附註:	Source: Dissertations Abstracts International, Volume: 83-03, Section: B.
Contained By:	Dissertations Abstracts International83-03B.
標題:	Computer science. -
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28540371
ISBN:	9798535551852

Learning and Logic for Formal Synthesis.
Caulfield, Benjamin.

Learning and Logic for Formal Synthesis. - Ann Arbor : ProQuest Dissertations & Theses, 2021 - 89 p.

Source: Dissertations Abstracts International, Volume: 83-03, Section: B.

Thesis (Ph.D.)--University of California, Berkeley, 2021.

This item must not be sold to any third party vendors.

Program synthesis is the use of algorithms to derive programs that satisfy given specifications. These specifications are usually given in some form of computer-understandable logic. Specifications are usually much easier to write than the programs themselves. By 'filling in the details' given by the specification, program synthesis opens the possibility of creating simple programs to both lay people and non-programming domain experts.Recent work in program synthesis has used techniques from 'exact active learning', where learning algorithms are able to pose queries to oracles. In the case of program synthesis, these oracles are implemented by checking potential programs against the given specification or asking a user for more inputs.Another recent development in the field is Syntax-Guided Synthesis (SyGuS), where the space of potential programs is given by a tree-grammar (or context-free grammar). Specifications are given in the logic of SMT (satisfiability modulo theories) problems.This thesis further develops the theory behind exact active learning, program synthesis, and their intersection. We provide upper and lower bounds, including undecidability results, for SyGuS problems defined on various SMT theories. We introduce the subject of actively learning equational theories and show how it can be used to learn constrained EUF formulas. We expand the problem of learning symbolic automata to use different types of symbolic counterexamples. We study the problem of exact active learning of concepts that are comprised of independent components, and show when the knowledge that components work independently can significantly reduce learning complexity. Finally, we introduce new methods for SyGuS solving with respect to cost, where the goal is to find the minimal cost program satisfying a specification.

ISBN: 9798535551852Subjects--Topical Terms:

523869
Computer science.
Subjects--Index Terms:

Concept learning

Learning and Logic for Formal Synthesis.
LDR:02944nmm a2200361 4500 001 2342359
005 20220318093122.5
008 241004s2021 ||||||||||||||||| ||eng d
020 $a 9798535551852
035 $a (MiAaPQ)AAI28540371
035 $a AAI28540371
040 $a MiAaPQ $c MiAaPQ
100 1 $a Caulfield, Benjamin. $3 3680708
245 1 0 $a Learning and Logic for Formal Synthesis.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2021
300 $a 89 p.
500 $a Source: Dissertations Abstracts International, Volume: 83-03, Section: B.
500 $a Advisor: Seshia, Sanjit A.
502 $a Thesis (Ph.D.)--University of California, Berkeley, 2021.
506 $a This item must not be sold to any third party vendors.
520 $a Program synthesis is the use of algorithms to derive programs that satisfy given specifications. These specifications are usually given in some form of computer-understandable logic. Specifications are usually much easier to write than the programs themselves. By 'filling in the details' given by the specification, program synthesis opens the possibility of creating simple programs to both lay people and non-programming domain experts.Recent work in program synthesis has used techniques from 'exact active learning', where learning algorithms are able to pose queries to oracles. In the case of program synthesis, these oracles are implemented by checking potential programs against the given specification or asking a user for more inputs.Another recent development in the field is Syntax-Guided Synthesis (SyGuS), where the space of potential programs is given by a tree-grammar (or context-free grammar). Specifications are given in the logic of SMT (satisfiability modulo theories) problems.This thesis further develops the theory behind exact active learning, program synthesis, and their intersection. We provide upper and lower bounds, including undecidability results, for SyGuS problems defined on various SMT theories. We introduce the subject of actively learning equational theories and show how it can be used to learn constrained EUF formulas. We expand the problem of learning symbolic automata to use different types of symbolic counterexamples. We study the problem of exact active learning of concepts that are comprised of independent components, and show when the knowledge that components work independently can significantly reduce learning complexity. Finally, we introduce new methods for SyGuS solving with respect to cost, where the goal is to find the minimal cost program satisfying a specification.
590 $a School code: 0028.
650 4 $a Computer science. $3 523869
650 4 $a Grammar. $3 899712
650 4 $a Active learning. $3 527777
650 4 $a Syntax. $3 897045
650 4 $a Logic. $3 529544
650 4 $a Neural networks. $3 677449
650 4 $a Maps. $3 544078
650 4 $a Variables. $3 3548259
650 4 $a Algorithms. $3 536374
650 4 $a Advisors. $3 3560734
650 4 $a Queries. $3 3564462
650 4 $a Apologies. $3 3562890
650 4 $a Artificial intelligence. $3 516317
653 $a Concept learning
653 $a Exact active learning
653 $a Formal synthesis
653 $a Program synthesis
690 $a 0984
690 $a 0395
690 $a 0800
710 2 $a University of California, Berkeley. $b Electrical Engineering & Computer Sciences. $3 1671057
773 0 $t Dissertations Abstracts International $g 83-03B.
790 $a 0028
791 $a Ph.D.
792 $a 2021
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28540371