MARC

 008260126s2025        us                              c    eng  d
■001000017360833
■00520260202105626
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798265428790
■035    ▼a(MiAaPQ)AAI32316551
■035    ▼a(MiAaPQ)Stanfordnj670jf3453
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a794.8
■1001  ▼aDong,  Kefan.
■24510▼aMathematical  Aspects  of  Deep  Reinforcement  Learning
■260    ▼a[Sl]▼bStanford  University▼c2025
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2025
■300    ▼a285  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  87-05,  Section:  A.
■500    ▼aAdvisor:  Ma,  Tengyu;Brunskill,  Emma;Roy,  Benjamin  Van.
■5021  ▼aThesis  (Ph.D.)--Stanford  University,  2025.
■520    ▼aThe  recent  decade  has  witnessed  a  wave  of  empirical  success  in  deep  reinforcement  learning  (deep  RL)-RL  with  neural  networks  as  the  backbone  function  approximators-in  solving  complex  decision-making  problems  and  achieving  superhuman  performance  in  domains  such  as  video  games,  board  games,  competitive  programming,  and  mathematical  reasoning.  This  thesis  studies  the  mathematical  aspects  of  deep  reinforcement  learning.In  Part  I  of  the  thesis,  we  focus  on  the  theoretical  analysis  of  deep  RL  algorithms.  The  main  technical  challenge  is  that,  unlike  supervised  learning,  analyzing  the  RL  algorithms  in  the  traditional  sense  seems  to  require  much  stronger  guarantees  on  the  extrapolation  power  of  function  approximations,  such  as,  e.g.,  l_inf  error  guarantees  for  learning  the  Q-function,  which  may  not  hold  even  for  simple  two-layer  neural  networks.  In  fact,  we  construct  hard  instances  where  the  reward  function  is  represented  by  a  single  ReLU  neuron  and  show  that  finding  a  near-optimal  policy  is  statistically  hard  in  these  cases.Hence,  Chapter  2  proposes  an  alternative  paradigm  for  analyzing  deep  RL  algorithms  inspired  by  the  nonconvex  optimization  literature:  we  first  design  an  algorithm,  ViOlin,  that  converges  to  a  local  maximum  of  the  reward  function  with  a  sample  complexity  determined  by  the  sequential  Rademacher  complexity  of  the  model  class,  and  then  prove  that  for  particular  instances,  all  local  maxima  are  also  global.  This  new  paradigm  allows  us  to  design  algorithms  that  achieve  better  regret  on  instances  with  better  reward  landscapes  while  gracefully  giving  up  on  fundamentally  hard  instances.  In  Chapter  3,  we  develop  asymptotic  instance-optimal  algorithms  for  general  bandit  and  RL  problems  with  finite  action  spaces.  Our  algorithm  adapts  to  the  complexity  of  each  problem  instance  and  achieves  lower  regret  on  easier  instances  compared  to  the  worst-case  scenario.  We  determine  the  exact  leading  term  of  the  optimal  asymptotic  regret  for  every  instance,  and  prove  that  our  algorithm,  T2C,  matches  the  optimal  regret  asymptotically.  When  applied  to  concrete  problems,  our  results  recover  the  classical  gap-dependent  bounds  for  multi-armed  bandits  and  prior  work  on  linear  bandits,  and  improve  upon  the  previous  best  instance-dependent  upper  bounds  for  reinforcement  learning.In  Part  II  of  the  thesis,  we  apply  deep  RL  algorithms  to  train  large  language  model  formal  theorem  provers.  The  main  technical  challenge  is  the  reward  sparsity  issue,  which  significantly  slows  down  the  training  process.  In  particular,  the  model  can  only  observe  a  positive  reward  when  every  step  of  the  proof  is  correct.  Therefore,  the  complexity  of  finding  a  correct  proof  increases  exponentially  with  the  number  of  required  proof  steps.In  Chapter  4,  we  develop  an  algorithm,  ProD,  that  encourages  the  model  to  decompose  the  proof  into  lemmas,  and  then  recursively  prove  them.  Inspired  by  how  mathematicians  train  themselves,  we  reward  correct  novel  lemmas  that  are  proposed  and  proved  even  if  the  original  theorem  is  too  challenging  to  be  proved  by  the  current  model,  providing  dense  intermediate  training  signals.  In  Chapter  5,  we  design  STP,  Self-play  Theorem  Prover,  that  simultaneously  assigns  the  model  two  roles:  conjecturer  and  prover.  The  conjecturer  is  trained  iteratively  on  previously  generated  conjectures  that  are  barely  provable  for  the  current  prover,  incentivizing  it  to  generate  increasingly  challenging  conjectures  over  time.  The  prover  attempts  to  prove  these  conjectures  using  standard  expert  iteration.  We  empirically  evaluate  both  methods  and  demonstrate  their  efficiency  on  carefully  curated  test  datasets  and  standard  formal  proof  benchmarks.
■590    ▼aSchool  code:  0212.
■650  4▼aComputer  &  video  games
■650  4▼aDeep  learning
■650  4▼aHuman  performance
■650  4▼aLarge  language  models
■650  4▼aVisualization
■650  4▼aDistance  learning
■650  4▼aDecision  making
■650  4▼aNeural  networks
■650  4▼aEducational  technology
■690    ▼a0800
■690    ▼a0710
■71020▼aStanford  University.
■7730  ▼tDissertations  Abstracts  International▼g87-05A.
■790    ▼a0212
■791    ▼aPh.D.
■792    ▼a2025
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17360833▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

미리보기

내보내기

chatGPT토론

Ai 추천 관련 도서