東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Efficient Algorithms for Automated R...

Sheng, Ying,

Linked to FindBook

Google Book

Amazon

博客來

Efficient Algorithms for Automated Reasoning and Large Language Models /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Efficient Algorithms for Automated Reasoning and Large Language Models // Ying Sheng.
Author:	Sheng, Ying,
Description:	1 electronic resource (226 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 86-04, Section: B.
Contained By:	Dissertations Abstracts International86-04B.
Subject:	Computer science. -
Online resource:	https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31520343
ISBN:	9798342114028

Efficient Algorithms for Automated Reasoning and Large Language Models /
Sheng, Ying,

Efficient Algorithms for Automated Reasoning and Large Language Models /Ying Sheng. - 1 electronic resource (226 pages)

Source: Dissertations Abstracts International, Volume: 86-04, Section: B.

This dissertation explores automated reasoning and large language models (LLMs), presenting a study on advancing the efficiency and effectiveness of both domains through innovative algorithms. It comprises three primary parts, each focusing on distinct but interconnected aspects of artificial intelligence.In the first part, the dissertation delves into the realm of automated reasoning, a domain that mimics human logical deduction using computational methods. The work addresses significant challenges in the field, particularly the exponential growth in computational demands as problem complexity increases. Notably, this segment emphasizes advancements in Satisfiability Modulo Theories (SMT), where the focus is on enhancing the efficiency of solving times amidst increasing complexity. The dissertation contributes to this by exploring theory combinations, algebraic datatypes, and sequences, which prove to offer more efficient reasoning frameworks.Transitioning to the second part, the focus shifts to LLMs, which have become pivotal in various applications, from content generation to decision-making support in corporate settings. Despite their capabilities, deploying these models efficiently remains a challenge due to substantial computational resource demands and the variable nature of user prompts. This part of the dissertation presents novel algorithms and serving infrastructure designed to optimize LLM performance, particularly in terms of reducing latency and enhancing throughput in real-time applications. Innovations such as FlexGen and S-LoRA are introduced, aiming to make LLMs more accessible on personal computing devices and to provide personalized, high-throughput services. This part also introduces the Virtual Token Counter (VTC), a novel fair scheduling algorithm that ensures equitable resource allocation among users, addressing the challenge of service fairness in high-demand LLM inference environments.The third and final part of the dissertation bridges the first two by demonstrating preliminary results on integrating formal verification and code generation using LLMs. This integration aims to harness the strengths of both fields to create more robust and versatile AI systems.

English

ISBN: 9798342114028Subjects--Topical Terms:

523869
Computer science.

Efficient Algorithms for Automated Reasoning and Large Language Models /
LDR:03540nmm a22003853i 4500 001 2428601
005 20250414021908.5
006 m o d
007 cr|nu||||||||
008 261011s2024 miu||||||m |||||||eng d
020 $a 9798342114028
035 $a (MiAaPQD)AAI31520343
035 $a (MiAaPQD)Stanfordzb184cc0261
035 $a AAI31520343
040 $a MiAaPQD $b eng $c MiAaPQD $e rda
100 1 $a Sheng, Ying, $e author. $3 3815926
245 1 0 $a Efficient Algorithms for Automated Reasoning and Large Language Models / $c Ying Sheng.
264 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2024
300 $a 1 electronic resource (226 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 86-04, Section: B.
500 $a Advisors: Barrett, Clark Committee members: Aiken, Alex; Gonzalez, Joseph; Stoica, Ion; Yang, Diyi.
502 $b Ph.D. $c Stanford University $d 2024.
520 $a This dissertation explores automated reasoning and large language models (LLMs), presenting a study on advancing the efficiency and effectiveness of both domains through innovative algorithms. It comprises three primary parts, each focusing on distinct but interconnected aspects of artificial intelligence.In the first part, the dissertation delves into the realm of automated reasoning, a domain that mimics human logical deduction using computational methods. The work addresses significant challenges in the field, particularly the exponential growth in computational demands as problem complexity increases. Notably, this segment emphasizes advancements in Satisfiability Modulo Theories (SMT), where the focus is on enhancing the efficiency of solving times amidst increasing complexity. The dissertation contributes to this by exploring theory combinations, algebraic datatypes, and sequences, which prove to offer more efficient reasoning frameworks.Transitioning to the second part, the focus shifts to LLMs, which have become pivotal in various applications, from content generation to decision-making support in corporate settings. Despite their capabilities, deploying these models efficiently remains a challenge due to substantial computational resource demands and the variable nature of user prompts. This part of the dissertation presents novel algorithms and serving infrastructure designed to optimize LLM performance, particularly in terms of reducing latency and enhancing throughput in real-time applications. Innovations such as FlexGen and S-LoRA are introduced, aiming to make LLMs more accessible on personal computing devices and to provide personalized, high-throughput services. This part also introduces the Virtual Token Counter (VTC), a novel fair scheduling algorithm that ensures equitable resource allocation among users, addressing the challenge of service fairness in high-demand LLM inference environments.The third and final part of the dissertation bridges the first two by demonstrating preliminary results on integrating formal verification and code generation using LLMs. This integration aims to harness the strengths of both fields to create more robust and versatile AI systems.
546 $a English
590 $a School code: 0212
650 4 $a Computer science. $3 523869
650 4 $a Large language models. $3 3775019
650 4 $a Vocational education. $3 539232
690 $a 0984
690 $a 0800
690 $a 0747
710 2 $a Stanford University. $e degree granting institution. $3 3765820
720 1 $a Barrett, Clark $e degree supervisor.
773 0 $t Dissertations Abstracts International $g 86-04B.
790 $a 0212
791 $a Ph.D.
792 $a 2024
856 4 0 $u https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31520343