MARC

 008250123s2024        us                              c    eng  d
■001000017164274
■00520250211152941
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798384493778
■035    ▼a(MiAaPQ)AAI31565384
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aTao,  Runzhou.
■24510▼aFormal  Verification  of  Quantum  Software
■260    ▼a[Sl]▼bColumbia  University▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a143  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  86-04,  Section:  B.
■500    ▼aAdvisor:  Gu,  Ronghui.
■5021  ▼aThesis  (Ph.D.)--Columbia  University,  2024.
■520    ▼aReal  applications  of  near-term  quantum  computing  are  around  the  corner  and  quantum  software  is  a  key  component.  Unlike  classical  computing,  quantum  software  is  under  the  threat  of  both  quantum  hardware  errors  and  human  bugs  due  to  the  unintuitiveness  of  quantum  physics  theory.  Therefore,  trustworthiness  and  reliability  are  critical  for  the  success  of  quantum  computation.  However,  most  traditional  methods  to  ensure  software  reliability,  like  testing,  do  not  transfer  to  quantum  at  scale  because  of  the  destructive  and  probabilistic  nature  of  quantum  measurement  and  the  exponential-sized  state  space.In  this  thesis,  I  introduce  a  series  of  frameworks  to  ensure  the  trustworthiness  of  quantum  computing  software  by  automated  formal  verification.  First,  I  present  Giallar,  a  fully-automated  verification  toolkit  for  quantum  compilers  to  formally  prove  that  the  compiler  is  bug-free.  Giallar  requires  no  manual  specifications,  invariants,  or  proofs,  and  can  automatically  verify  that  a  compiler  pass  preserves  the  semantics  of  quantum  circuits.  To  deal  with  unbounded  loops  in  quantum  compilers,  Giallar  abstracts  three  loop  templates,  whose  loop  invariants  can  be  automatically  inferred.  To  efficiently  check  the  equivalence  of  arbitrary  input  and  output  circuits  that  have  complicated  matrix  semantics  representation,  Giallar  introduces  a  symbolic  representation  for  quantum  circuits  and  a  set  of  rewrite  rules  for  showing  the  equivalence  of  symbolic  quantum  circuits.  With  Giallar,  I  implemented  and  verified  44  (out  of  56)  compiler  passes  in  13  versions  of  the  Qiskit  compiler,  the  open-source  quantum  compiler  standard,  during  which  three  bugs  were  detected  in  and  confirmed  by  Qiskit.  The  evaluation  shows  that  most  of  Qiskit  compiler  passes  can  be  automatically  verified  in  seconds  and  verification  imposes  only  a  modest  overhead  to  compilation  performance.Second,  I  introduce  Gleipnir,  an  error  analysis  framework  for  quantum  programs  that  enable  scalable  and  adaptive  verification  of  quantum  error  through  the  application  of  tensor  networks.  Giallar  introduces  the  (\uD835\uDF0C,  \uD835\uDEFF)-diamond  norm,  an  error  metric  constrained  by  a  quantum  predicate  consisting  of  the  approximate  state  \uD835\uDF0C  and  its  distance  \uD835\uDEFF  to  the  ideal  state  \uD835\uDF0C.  This  predicate  (\uD835\uDF0C,  \uD835\uDEFF)  can  be  computed  adaptively  using  tensor  networks  based  on  Matrix  Product  States.  Giallar  features  a  lightweight  logic  for  reasoning  about  error  bounds  in  noisy  quantum  programs,  based  on  the  (\uD835\uDF0C,  \uD835\uDEFF)-diamond  norm  metric.  The  experimental  results  show  that  Giallar  is  able  to  efficiently  generate  tight  error  bounds  for  real-world  quantum  programs  with  10  to  100  qubits,  and  can  be  used  to  evaluate  the  error  mitigation  performance  of  quantum  compiler  transformations.Finally,  I  present  QSynth,  a  quantum  program  synthesis  framework  that  synthesizes  verified  recursive  quantum  programs,  including  a  new  inductive  quantum  programming  language,  its  specification,  a  sound  logic  for  reasoning,  and  an  encoding  of  the  reasoning  procedure  into  SMT  instances.  By  leveraging  existing  SMT  solvers,  QSynth  successfully  synthesizes  10  quantum  unitary  programs  including  quantum  arithmetic  programs,  quantum  eigenvalue  inversion,  quantum  teleportation  and  Quantum  Fourier  Transformation,  which  can  be  readily  transpiled  to  executable  programs  on  major  quantum  platforms,  e.g.,  Q#,  IBM  Qiskit,  and  AWS  Braket.
■590    ▼aSchool  code:  0054.
■650  4▼aComputer  science
■650  4▼aQuantum  physics
■650  4▼aTheoretical  physics
■653    ▼aQuantum  software
■653    ▼aGiallar
■653    ▼aQiskit  compiler
■653    ▼aQuantum  programs
■690    ▼a0984
■690    ▼a0599
■690    ▼a0753
■71020▼aColumbia  University▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g86-04B.
■790    ▼a0054
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17164274▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books