Connect with us

Quantum

Optimal fermion-to-qubit mapping via ternary trees with applications to reduced quantum states learning

Published

on

Zhang Jiang1, Amir Kalev2, Wojciech Mruczkiewicz1, and Hartmut Neven1

1Google Research, Venice, CA 90291
2Joint Center for Quantum Information and Computer Science, University of Maryland, College Park, MD 20742-2420, USA

Find this paper interesting or want to discuss? Scite or leave a comment on SciRate.

Abstract

We introduce a fermion-to-qubit mapping defined on ternary trees, where any single Majorana operator on an $n$-mode fermionic system is mapped to a multi-qubit Pauli operator acting nontrivially on $lceil log_3(2n+1)rceil$ qubits. The mapping has a simple structure and is optimal in the sense that it is impossible to construct Pauli operators in any fermion-to-qubit mapping acting nontrivially on less than $log_3(2n)$ qubits on average. We apply it to the problem of learning $k$-fermion reduced density matrix (RDM), a problem relevant in various quantum simulation applications. We show that one can determine individual elements of all $k$-fermion RDMs in parallel, to precision $epsilon$, by repeating a single quantum circuit for $lesssim (2n+1)^k epsilon^{-2}$ times. This result is based on a method we develop here that allows one to determine individual elements of all $k$-qubit RDMs in parallel, to precision $epsilon$, by repeating a single quantum circuit for $lesssim 3^k epsilon^{-2}$ times, independent of the system size. This improves over existing schemes for determining qubit RDMs.

► BibTeX data

► References

[1] R. P. Feynman, “Simulating physics with computers,” International Journal of Theoretical Physics 21, 467 (1982).
https:/​/​doi.org/​10.1007/​BF02650179

[2] S. Lloyd, “Universal Quantum Simulators,” Science 273, 1073 (1996).
https:/​/​doi.org/​10.1126/​science.273.5278.1073

[3] I. Georgescu, S. Ashhab, and F. Nori, “Quantum simulation,” Reviews of Modern Physics 86, 153 (2014).
https:/​/​doi.org/​10.1103/​RevModPhys.86.153

[4] D. Wecker, M. B. Hastings, N. Wiebe, B. K. Clark, C. Nayak, and M. Troyer, “Solving strongly correlated electron models on a quantum computer,” Physical Review A 92, 062318 (2015).
https:/​/​doi.org/​10.1103/​PhysRevA.92.062318

[5] R. Babbush, N. Wiebe, J. McClean, J. McClain, H. Neven, and G. K.-L. Chan, “Low-Depth Quantum Simulation of Materials,” Physical Review X 8, 011044 (2018).
https:/​/​doi.org/​10.1103/​PhysRevX.8.011044

[6] Z. Jiang, K. J. Sung, K. Kechedzhi, V. N. Smelyanskiy, and S. Boixo, “Quantum Algorithms to Simulate Many-Body Physics of Correlated Fermions,” Physical Review Applied 9, 044036 (2018).
https:/​/​doi.org/​10.1103/​PhysRevApplied.9.044036

[7] J. I. Cirac and P. Zoller, “Quantum computations with cold trapped ions,” Physical Review Letters 74, 4091 (1995).
https:/​/​doi.org/​10.1103/​PhysRevLett.74.4091

[8] D. Kielpinski, C. Monroe, and D. J. Wineland, “Architecture for a large-scale ion-trap quantum computer,” Nature 417, 709 (2002).
https:/​/​doi.org/​10.1038/​nature00784

[9] H. Häffner, C. F. Roos, and R. Blatt, “Quantum computing with trapped ions,” Physics Reports 469, 155 (2008).
https:/​/​doi.org/​10.1016/​j.physrep.2008.09.003

[10] M. H. Devoret, A. Wallraff, and J. M. Martinis, “Superconducting Qubits: A Short Review,” arXiv:0411174 (2004).
arXiv:cond-mat/0411174

[11] G. Wendin, “Quantum information processing with superconducting circuits: a review,” Reports on Progress in Physics. Physical Society (Great Britain) 80, 106001 (2017).
https:/​/​doi.org/​10.1088/​1361-6633/​aa7e1a

[12] A. Peruzzo, J. McClean, P. Shadbolt, M.-H. Yung, X.-Q. Zhou, P. J. Love, A. Aspuru-Guzik, and J. L. O’ÄôBrien, “A variational eigenvalue solver on a photonic quantum processor,” Nature Communications 5, 4213 (2014).
https:/​/​doi.org/​10.1038/​ncomms5213

[13] J. R. McClean, J. Romero, R. Babbush, and A. Aspuru-Guzik, “The theory of variational hybrid quantum-classical algorithms,” New Journal of Physics 18, 023023 (2016).
https:/​/​doi.org/​10.1088/​1367-2630/​18/​2/​023023

[14] M. A. Nielsen, “The Fermionic canonical commutation relations and the Jordan-Wigner transform,” Tech. Rep. University of Queensland (2005).
http:/​/​michaelnielsen.org/​blog/​archive/​nones/​fermions_and_jordan_wigner.pdf

[15] J. T. Seeley, M. J. Richard, and P. J. Love, “The Bravyi-Kitaev transformation for quantum computation of electronic structure,” The Journal of Chemical Physics 137, 224109 (2012).
https:/​/​doi.org/​10.1063/​1.4768229

[16] S. B. Bravyi and A. Y. Kitaev, “Fermionic Quantum Computation,” Annals of Physics 298, 210 (2002).
https:/​/​doi.org/​10.1006/​aphy.2002.6254

[17] A. Tranter, S. Sofia, J. Seeley, M. Kaicher, J. McClean, R. Babbush, P. V. Coveney, F. Mintert, F. Wilhelm, and P. J. Love, “The Bravyi-Kitaev transformation: Properties and applications,” International Journal of Quantum Chemistry 115, 1431 (2015).
https:/​/​doi.org/​10.1002/​qua.24969

[18] V. Havlíček, M. Troyer, and J. D. Whitfield, “Operator locality in the quantum simulation of fermionic models,” Physical Review A 95, 032332 (2017).
https:/​/​doi.org/​10.1103/​PhysRevA.95.032332

[19] F. Arute, K. Arya, R. Babbush, D. Bacon, J. C. Bardin, R. Barends, R. Biswas, S. Boixo, F. G. S. L. Brandao, D. A. Buell, B. Burkett, Y. Chen, Z. Chen, B. Chiaro, R. Collins, W. Courtney, A. Dunsworth, E. Farhi, B. Foxen, A. Fowler, C. Gidney, M. Giustina, R. Graff, K. Guerin, S. Habegger, M. P. Harrigan, M. J. Hartmann, A. Ho, M. Hoffmann, T. Huang, T. S. Humble, S. V. Isakov, E. Jeffrey, Z. Jiang, D. Kafri, K. Kechedzhi, J. Kelly, P. V. Klimov, S. Knysh, A. Korotkov, F. Kostritsa, D. Landhuis, M. Lindmark, E. Lucero, D. Lyakh, S. Mandr??, J. R. McClean, M. McEwen, A. Megrant, X. Mi, K. Michielsen, M. Mohseni, J. Mutus, O. Naaman, M. Neeley, C. Neill, M. Y. Niu, E. Ostby, A. Petukhov, J. C. Platt, C. Quintana, E. G. Rieffel, P. Roushan, N. C. Rubin, D. Sank, K. J. Satzinger, V. Smelyanskiy, K. J. Sung, M. D. Trevithick, A. Vainsencher, B. Villalonga, T. White, Z. J. Yao, P. Yeh, A. Zalcman, H. Neven, and J. M. Martinis, “Quantum supremacy using a programmable superconducting processor,” Nature 574, 505 (2019).
https:/​/​doi.org/​10.1038/​s41586-019-1666-5

[20] A. Y. Vlasov, “Clifford algebras, Spin groups and qubit trees,” arXiv:1904.09912 (2019).
arXiv:1904.09912

[21] M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, 1st ed. (Cambridge University Press, 2000).

[22] S. Sharma, J. K. Dewhurst, N. N. Lathiotakis, and E. K. U. Gross, “Reduced density matrix functional for many-electron systems,” Physical Review B 78, 201103 (2008).
https:/​/​doi.org/​10.1103/​PhysRevB.78.201103

[23] M. Fagotti and F. H. L. Essler, “Reduced density matrix after a quantum quench,” Physical Review B 87, 245107 (2013).
https:/​/​doi.org/​10.1103/​PhysRevB.87.245107

[24] N. C. Rubin, R. Babbush, and J. McClean, “Application of fermionic marginal constraints to hybrid quantum algorithms,” New Journal of Physics 20, 053020 (2018).
https:/​/​doi.org/​10.1088/​1367-2630/​aab919

[25] G. Gidofalvi and D. A. Mazziotti, “Molecular properties from variational reduced-density-matrix theory with three-particle N-representability conditions,” The Journal of Chemical Physics 126, 024105 (2007).
https:/​/​doi.org/​10.1063/​1.2423008

[26] C. Overy, G. H. Booth, N. S. Blunt, J. J. Shepherd, D. Cleland, and A. Alavi, “Unbiased reduced density matrices and electronic properties from full configuration interaction quantum Monte Carlo,” The Journal of Chemical Physics 141, 244117 (2014).
https:/​/​doi.org/​10.1063/​1.4904313

[27] T. E. O’Brien, B. Senjean, R. Sagastizabal, X. Bonet-Monroig, A. Dutkiewicz, F. Buda, L. DiCarlo, and L. Visscher, “Calculating energy derivatives for quantum chemistry on a quantum computer,” npj Quantum Information 5, 1 (2019).
https:/​/​doi.org/​10.1038/​s41534-019-0213-4

[28] J. R. McClean, M. E. Kimchi-Schwartz, J. Carter, and W. A. de Jong, “Hybrid quantum-classical hierarchy for mitigation of decoherence and determination of excited states,” Physical Review A 95, 042308 (2017).
https:/​/​doi.org/​10.1103/​PhysRevA.95.042308

[29] T. Takeshita, N. C. Rubin, Z. Jiang, E. Lee, R. Babbush, and J. R. McClean, “Increasing the Representation Accuracy of Quantum Simulations of Chemistry without Extra Quantum Resources,” Physical Review X 10, 011004 (2020).
https:/​/​doi.org/​10.1103/​PhysRevX.10.011004

[30] J. Cotler and F. Wilczek, “Quantum Overlapping Tomography,” Physical Review Letters 124, 100401 (2020).
https:/​/​doi.org/​10.1103/​PhysRevLett.124.100401

[31] X. Bonet-Monroig, R. Babbush, and T. E. O’Brien, “Nearly optimal measurement scheduling for partial tomography of quantum states,” arXiv:1908.05628 (2019).
arXiv:1908.05628

[32] J. Řeháček, B.-G. Englert, and D. Kaszlikowski, “Minimal qubit tomography,” Phys. Rev. A 70, 052321 (2004).
https:/​/​doi.org/​10.1103/​PhysRevA.70.052321

[33] I. Hamamura and T. Imamichi, “Efficient evaluation of quantum observables using entangled measurements,” arXiv:1909.09119 (2019).
arXiv:1909.09119

[34] A. F. Izmaylov, T.-C. Yen, R. A. Lang, and V. Verteletskyi, “Unitary Partitioning Approach to the Measurement Problem in the Variational Quantum Eigensolver Method,” Journal of Chemical Theory and Computation 16, 190 (2020).
https:/​/​doi.org/​10.1021/​acs.jctc.9b00791

[35] A. Zhao, A. Tranter, W. M. Kirby, S. F. Ung, A. Miyake, and P. Love, “Measurement reduction in variational quantum algorithms,” arXiv:1908.08067 (2019).
arXiv:1908.08067

[36] W. J. Huggins, J. McClean, N. Rubin, Z. Jiang, N. Wiebe, K. B. Whaley, and R. Babbush, “Efficient and Noise Resilient Measurements for Quantum Chemistry on Near-Term Quantum Computers,” arXiv:1907.13117 (2019).
arXiv:1907.13117

[37] D. A. Mazziotti, ed., Reduced-Density-Matrix Mechanics: With Application to Many-Electron Atoms and Molecules (Wiley-Interscience, 2009).

[38] M. Steudtner and S. Wehner, “Quantum codes for quantum simulation of fermions on a square lattice of qubits,” Physical Review A 99, 022308 (2019).
https:/​/​doi.org/​10.1103/​PhysRevA.99.022308

[39] K. Setia and J. D. Whitfield, “Bravyi-Kitaev Superfast simulation of electronic structure on a quantum computer,” The Journal of Chemical Physics 148, 164104 (2018).
https:/​/​doi.org/​10.1063/​1.5019371

[40] Z. Jiang, J. McClean, R. Babbush, and H. Neven, “Majorana Loop Stabilizer Codes for Error Mitigation in Fermionic Quantum Simulations,” Physical Review Applied 12, 064041 (2019).
https:/​/​doi.org/​10.1103/​PhysRevApplied.12.064041

[41] C. A. Fuchs, M. C. Hoang, and B. C. Stacey, “The SIC question: History and state of play,” Axioms 6, 21 (2017).
https:/​/​doi.org/​10.3390/​axioms6030021

[42] H. B. Dang, K. Blanchfield, I. Bengtsson, and D. M. Appleby, “Linear dependencies in Weyl–Heisenberg orbits,” Quantum Information Processing 12, 3449 (2013).
https:/​/​doi.org/​10.1007/​s11128-013-0609-6

Cited by

[1] Alexander Yu. Vlasov, “Clifford algebras, Spin groups and qubit trees”, arXiv:1904.09912.

[2] Sam McArdle, Suguru Endo, Alán Aspuru-Guzik, Simon C. Benjamin, and Xiao Yuan, “Quantum computational chemistry”, Reviews of Modern Physics 92 1, 015003 (2020).

[3] Hsin-Yuan Huang, Richard Kueng, and John Preskill, “Predicting Many Properties of a Quantum System from Very Few Measurements”, arXiv:2002.08953.

[4] Adrian Chapman and Steven T. Flammia, “Characterization of solvable spin models via graph invariants”, arXiv:2003.05465.

[5] Ikko Hamamura and Takashi Imamichi, “Efficient evaluation of quantum observables using entangled measurements”, arXiv:1909.09119.

The above citations are from SAO/NASA ADS (last updated successfully 2020-06-04 09:05:06). The list may be incomplete as not all publishers provide suitable and complete citation data.

Could not fetch Crossref cited-by data during last attempt 2020-06-04 09:05:04: Could not fetch cited-by data for 10.22331/q-2020-06-02-276 from Crossref. This is normal if the DOI was registered recently.

Source: https://quantum-journal.org/papers/q-2020-06-04-276/

Quantum

Proof Assistant Makes Jump to Big-League Math

Published

on

Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field.

But a new result, completed in early June, has the feel of a rookie’s first hit in the big leagues: At last, a proof assistant has made a real contribution to the leading edge of mathematical research by verifying the correctness of a complicated, modern proof.

“It demonstrates that modern maths can be formalized in a theorem prover,” said Bhavik Mehta, a graduate student at the University of Cambridge who contributed to the work.

The proof in question is by Peter Scholze of the University of Bonn, one of the most widely respected mathematicians in the world. It is just one piece of a larger project called “condensed mathematics” that he and Dustin Clausen of the University of Copenhagen have been working on for several years.

Their goal is to create new foundations for topology, replacing the traditional notion of a topological space — whose examples include the sphere and the doughnut — with more versatile objects that the authors call condensed sets. In this new perspective, topological spaces are thought of as being assembled from infinite points of dust glued together.

That project includes a particularly important, difficult proof that Scholze worked out himself during a consuming week in July 2019. It establishes that an area of math called real functional analysis still works if you replace topological spaces with condensed sets.

Scholze began the proof on a Monday. He worked entirely in his head, barely writing anything down, let alone using a computer. By Thursday afternoon he’d nearly figured it out, save one piece that he just couldn’t get right. He was also feeling the strain of the intense concentration required to hold such a complicated argument in his active memory. So that night he unwound with some friends at a bar. He paid for it the next morning, Friday.

“I was completely hungover,” said Scholze.

But he also knew that he wouldn’t have time to work over the weekend, making Friday his best chance to finish the proof. The thought of losing touch with everything he’d built up in his mind over the past week, then having to start again fresh on Monday, was more than he wanted to consider.

“I didn’t think I’d have the mental capacity to rebuild this in my head again,” said Scholze.

So he powered through and finished the proof. But afterward, he wasn’t certain that what he had done was correct. The reason was more than the hazy circumstances in which he’d cleared the final hurdle. The proof was so complicated Scholze knew it was possible he had missed something.

“It’s some very convoluted thing with many moving parts. It’s hard to know which parts move by how much when you shift one of these parameters,” said Scholze.

Scholze didn’t find time to actually write down the proof until November 2019. A year later he contacted Kevin Buzzard, a mathematician at Imperial College London and a prominent evangelist for a proof assistant program called Lean. Scholze wanted to know whether it would be possible to type his proof into Lean — turning it into lines of code like a software program — so that the program could verify whether it was really true.

Buzzard shared Scholze’s inquiry with a handful of other members of the Lean community including Johan Commelin, a postdoctoral researcher at the University of Freiburg. Commelin had the perfect background for the job — he’d been using Lean for several years and was familiar with condensed mathematics — and he was convinced that verifying Scholze’s proof would do a lot to legitimize the proof assistant’s standing in the mathematical community.

“Being able to collaborate with Peter on such a project and having his name attached to it would be an enormous boost for Lean,” said Commelin.

But he also thought it could take a year or more to do it, which gave him pause. Commelin was worried he might spend all that time verifying the proof and, at the end, the rest of the math world would just shrug.

“I thought that if I spend two years working on this and I come out of my cave and say, ‘This is fine,’ the rest of the world is going to say, ‘Wow, we already knew this, Peter proved it,’” said Commelin. It wouldn’t matter that Scholze himself wasn’t entirely sure.

So Commelin asked Scholze if he’d be willing to make a public statement vouching for the importance of the work. Scholze agreed, and on Dec. 5, 2020, he wrote a post on Buzzard’s blog.

They called it the “Liquid Tensor Experiment,” a nod to mathematical objects involved in the proof called liquid real vector spaces, and to a progressive rock band he and Commelin enjoy called Liquid Tension Experiment. In the 4,400-word primer, Scholze explained some technical aspects of the result and then added a note testifying in plain language to what he saw as the importance of checking it with a computer.

“I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change,)” Scholze wrote. “Better be sure it’s correct…”

Assurance in place, Commelin set to work. After explaining to Lean the mathematical statement whose proof he ultimately wanted the program to check, he brought more mathematicians into the project. They identified a few lemmas — intermediate steps in the proof — that seemed most approachable. They formalized those first, coding them on top of the library of mathematical knowledge that Lean draws on to determine if a given statement is true or not.

Last October, Quanta wrote that the collective effort to write mathematics in Lean has the “air of a barn raising.” This project was no different. Commelin would identify discrete parts of the proof and post them to Zulip, a discussion board that serves as a hub for the Lean community. When mathematicians saw a part of the proof that fit their expertise, they’d volunteer to formalize it.

Mehta was one of about a dozen mathematicians who contributed to the work. In May he saw a post from Commelin asking for help formalizing the proof of a statement called Gordan’s lemma, which related to Mehta’s work in the area of combinatorial geometry. He spent a week coding the proof in terms that were consistent with the larger proof the mathematicians were building. It was emblematic, he said, of the way Lean works.

“It’s one big collaboration with a lot of people doing what they’re good at to make a singular monolith,” he said.

As the work proceeded, Scholze was a consistent presence on Zulip, answering questions and explaining points of the proof — a bit like an architect giving directions to builders on a job site. “He was always within reach,” Commelin said.

At the end of May the group finished formalizing the one part of the proof Scholze was most unsure about. Commelin entered the final keystroke at 1:10 a.m. on May 29. Lean compiled the proof, and it ran like a functioning program, verifying that Scholze’s work was 100% correct. Now Scholze and other mathematicians can apply those techniques from real functional analysis to condensed sets, knowing that they’ll definitely work in this new setting.

And while Scholze still prefers to work out proofs in his head, Lean’s abilities left him impressed. He can now foresee programs like it playing an enduring role in research mathematics.

“This experiment has changed drastically my impression of how capable [proof assistants] are,” Scholze said. “I now think it’s sensible in principle to formalize whatever you want in Lean. There’s no real obstruction.”

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.

Click here to access.

Source: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

Continue Reading

Quantum

Proof Assistant Makes Jump to Big-League Math

Published

on

Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field.

But a new result, completed in early June, has the feel of a rookie’s first hit in the big leagues: At last, a proof assistant has made a real contribution to the leading edge of mathematical research by verifying the correctness of a complicated, modern proof.

“It demonstrates that modern maths can be formalized in a theorem prover,” said Bhavik Mehta, a graduate student at the University of Cambridge who contributed to the work.

The proof in question is by Peter Scholze of the University of Bonn, one of the most widely respected mathematicians in the world. It is just one piece of a larger project called “condensed mathematics” that he and Dustin Clausen of the University of Copenhagen have been working on for several years.

Their goal is to create new foundations for topology, replacing the traditional notion of a topological space — whose examples include the sphere and the doughnut — with more versatile objects that the authors call condensed sets. In this new perspective, topological spaces are thought of as being assembled from infinite points of dust glued together.

That project includes a particularly important, difficult proof that Scholze worked out himself during a consuming week in July 2019. It establishes that an area of math called real functional analysis still works if you replace topological spaces with condensed sets.

Scholze began the proof on a Monday. He worked entirely in his head, barely writing anything down, let alone using a computer. By Thursday afternoon he’d nearly figured it out, save one piece that he just couldn’t get right. He was also feeling the strain of the intense concentration required to hold such a complicated argument in his active memory. So that night he unwound with some friends at a bar. He paid for it the next morning, Friday.

“I was completely hungover,” said Scholze.

But he also knew that he wouldn’t have time to work over the weekend, making Friday his best chance to finish the proof. The thought of losing touch with everything he’d built up in his mind over the past week, then having to start again fresh on Monday, was more than he wanted to consider.

“I didn’t think I’d have the mental capacity to rebuild this in my head again,” said Scholze.

So he powered through and finished the proof. But afterward, he wasn’t certain that what he had done was correct. The reason was more than the hazy circumstances in which he’d cleared the final hurdle. The proof was so complicated Scholze knew it was possible he had missed something.

“It’s some very convoluted thing with many moving parts. It’s hard to know which parts move by how much when you shift one of these parameters,” said Scholze.

Scholze didn’t find time to actually write down the proof until November 2019. A year later he contacted Kevin Buzzard, a mathematician at Imperial College London and a prominent evangelist for a proof assistant program called Lean. Scholze wanted to know whether it would be possible to type his proof into Lean — turning it into lines of code like a software program — so that the program could verify whether it was really true.

Buzzard shared Scholze’s inquiry with a handful of other members of the Lean community including Johan Commelin, a postdoctoral researcher at the University of Freiburg. Commelin had the perfect background for the job — he’d been using Lean for several years and was familiar with condensed mathematics — and he was convinced that verifying Scholze’s proof would do a lot to legitimize the proof assistant’s standing in the mathematical community.

“Being able to collaborate with Peter on such a project and having his name attached to it would be an enormous boost for Lean,” said Commelin.

But he also thought it could take a year or more to do it, which gave him pause. Commelin was worried he might spend all that time verifying the proof and, at the end, the rest of the math world would just shrug.

“I thought that if I spend two years working on this and I come out of my cave and say, ‘This is fine,’ the rest of the world is going to say, ‘Wow, we already knew this, Peter proved it,’” said Commelin. It wouldn’t matter that Scholze himself wasn’t entirely sure.

So Commelin asked Scholze if he’d be willing to make a public statement vouching for the importance of the work. Scholze agreed, and on Dec. 5, 2020, he wrote a post on Buzzard’s blog.

They called it the “Liquid Tensor Experiment,” a nod to mathematical objects involved in the proof called liquid real vector spaces, and to a progressive rock band he and Commelin enjoy called Liquid Tension Experiment. In the 4,400-word primer, Scholze explained some technical aspects of the result and then added a note testifying in plain language to what he saw as the importance of checking it with a computer.

“I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change,)” Scholze wrote. “Better be sure it’s correct…”

Assurance in place, Commelin set to work. After explaining to Lean the mathematical statement whose proof he ultimately wanted the program to check, he brought more mathematicians into the project. They identified a few lemmas — intermediate steps in the proof — that seemed most approachable. They formalized those first, coding them on top of the library of mathematical knowledge that Lean draws on to determine if a given statement is true or not.

Last October, Quanta wrote that the collective effort to write mathematics in Lean has the “air of a barn raising.” This project was no different. Commelin would identify discrete parts of the proof and post them to Zulip, a discussion board that serves as a hub for the Lean community. When mathematicians saw a part of the proof that fit their expertise, they’d volunteer to formalize it.

Mehta was one of about a dozen mathematicians who contributed to the work. In May he saw a post from Commelin asking for help formalizing the proof of a statement called Gordan’s lemma, which related to Mehta’s work in the area of combinatorial geometry. He spent a week coding the proof in terms that were consistent with the larger proof the mathematicians were building. It was emblematic, he said, of the way Lean works.

“It’s one big collaboration with a lot of people doing what they’re good at to make a singular monolith,” he said.

As the work proceeded, Scholze was a consistent presence on Zulip, answering questions and explaining points of the proof — a bit like an architect giving directions to builders on a job site. “He was always within reach,” Commelin said.

At the end of May the group finished formalizing the one part of the proof Scholze was most unsure about. Commelin entered the final keystroke at 1:10 a.m. on May 29. Lean compiled the proof, and it ran like a functioning program, verifying that Scholze’s work was 100% correct. Now Scholze and other mathematicians can apply those techniques from real functional analysis to condensed sets, knowing that they’ll definitely work in this new setting.

And while Scholze still prefers to work out proofs in his head, Lean’s abilities left him impressed. He can now foresee programs like it playing an enduring role in research mathematics.

“This experiment has changed drastically my impression of how capable [proof assistants] are,” Scholze said. “I now think it’s sensible in principle to formalize whatever you want in Lean. There’s no real obstruction.”

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.

Click here to access.

Source: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

Continue Reading

Quantum

Proof Assistant Makes Jump to Big-League Math

Published

on

Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field.

But a new result, completed in early June, has the feel of a rookie’s first hit in the big leagues: At last, a proof assistant has made a real contribution to the leading edge of mathematical research by verifying the correctness of a complicated, modern proof.

“It demonstrates that modern maths can be formalized in a theorem prover,” said Bhavik Mehta, a graduate student at the University of Cambridge who contributed to the work.

The proof in question is by Peter Scholze of the University of Bonn, one of the most widely respected mathematicians in the world. It is just one piece of a larger project called “condensed mathematics” that he and Dustin Clausen of the University of Copenhagen have been working on for several years.

Their goal is to create new foundations for topology, replacing the traditional notion of a topological space — whose examples include the sphere and the doughnut — with more versatile objects that the authors call condensed sets. In this new perspective, topological spaces are thought of as being assembled from infinite points of dust glued together.

That project includes a particularly important, difficult proof that Scholze worked out himself during a consuming week in July 2019. It establishes that an area of math called real functional analysis still works if you replace topological spaces with condensed sets.

Scholze began the proof on a Monday. He worked entirely in his head, barely writing anything down, let alone using a computer. By Thursday afternoon he’d nearly figured it out, save one piece that he just couldn’t get right. He was also feeling the strain of the intense concentration required to hold such a complicated argument in his active memory. So that night he unwound with some friends at a bar. He paid for it the next morning, Friday.

“I was completely hungover,” said Scholze.

But he also knew that he wouldn’t have time to work over the weekend, making Friday his best chance to finish the proof. The thought of losing touch with everything he’d built up in his mind over the past week, then having to start again fresh on Monday, was more than he wanted to consider.

“I didn’t think I’d have the mental capacity to rebuild this in my head again,” said Scholze.

So he powered through and finished the proof. But afterward, he wasn’t certain that what he had done was correct. The reason was more than the hazy circumstances in which he’d cleared the final hurdle. The proof was so complicated Scholze knew it was possible he had missed something.

“It’s some very convoluted thing with many moving parts. It’s hard to know which parts move by how much when you shift one of these parameters,” said Scholze.

Scholze didn’t find time to actually write down the proof until November 2019. A year later he contacted Kevin Buzzard, a mathematician at Imperial College London and a prominent evangelist for a proof assistant program called Lean. Scholze wanted to know whether it would be possible to type his proof into Lean — turning it into lines of code like a software program — so that the program could verify whether it was really true.

Buzzard shared Scholze’s inquiry with a handful of other members of the Lean community including Johan Commelin, a postdoctoral researcher at the University of Freiburg. Commelin had the perfect background for the job — he’d been using Lean for several years and was familiar with condensed mathematics — and he was convinced that verifying Scholze’s proof would do a lot to legitimize the proof assistant’s standing in the mathematical community.

“Being able to collaborate with Peter on such a project and having his name attached to it would be an enormous boost for Lean,” said Commelin.

But he also thought it could take a year or more to do it, which gave him pause. Commelin was worried he might spend all that time verifying the proof and, at the end, the rest of the math world would just shrug.

“I thought that if I spend two years working on this and I come out of my cave and say, ‘This is fine,’ the rest of the world is going to say, ‘Wow, we already knew this, Peter proved it,’” said Commelin. It wouldn’t matter that Scholze himself wasn’t entirely sure.

So Commelin asked Scholze if he’d be willing to make a public statement vouching for the importance of the work. Scholze agreed, and on Dec. 5, 2020, he wrote a post on Buzzard’s blog.

They called it the “Liquid Tensor Experiment,” a nod to mathematical objects involved in the proof called liquid real vector spaces, and to a progressive rock band he and Commelin enjoy called Liquid Tension Experiment. In the 4,400-word primer, Scholze explained some technical aspects of the result and then added a note testifying in plain language to what he saw as the importance of checking it with a computer.

“I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change,)” Scholze wrote. “Better be sure it’s correct…”

Assurance in place, Commelin set to work. After explaining to Lean the mathematical statement whose proof he ultimately wanted the program to check, he brought more mathematicians into the project. They identified a few lemmas — intermediate steps in the proof — that seemed most approachable. They formalized those first, coding them on top of the library of mathematical knowledge that Lean draws on to determine if a given statement is true or not.

Last October, Quanta wrote that the collective effort to write mathematics in Lean has the “air of a barn raising.” This project was no different. Commelin would identify discrete parts of the proof and post them to Zulip, a discussion board that serves as a hub for the Lean community. When mathematicians saw a part of the proof that fit their expertise, they’d volunteer to formalize it.

Mehta was one of about a dozen mathematicians who contributed to the work. In May he saw a post from Commelin asking for help formalizing the proof of a statement called Gordan’s lemma, which related to Mehta’s work in the area of combinatorial geometry. He spent a week coding the proof in terms that were consistent with the larger proof the mathematicians were building. It was emblematic, he said, of the way Lean works.

“It’s one big collaboration with a lot of people doing what they’re good at to make a singular monolith,” he said.

As the work proceeded, Scholze was a consistent presence on Zulip, answering questions and explaining points of the proof — a bit like an architect giving directions to builders on a job site. “He was always within reach,” Commelin said.

At the end of May the group finished formalizing the one part of the proof Scholze was most unsure about. Commelin entered the final keystroke at 1:10 a.m. on May 29. Lean compiled the proof, and it ran like a functioning program, verifying that Scholze’s work was 100% correct. Now Scholze and other mathematicians can apply those techniques from real functional analysis to condensed sets, knowing that they’ll definitely work in this new setting.

And while Scholze still prefers to work out proofs in his head, Lean’s abilities left him impressed. He can now foresee programs like it playing an enduring role in research mathematics.

“This experiment has changed drastically my impression of how capable [proof assistants] are,” Scholze said. “I now think it’s sensible in principle to formalize whatever you want in Lean. There’s no real obstruction.”

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.

Click here to access.

Source: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

Continue Reading

Quantum

Quantum walk-based portfolio optimisation

Published

on

N. Slate, E. Matwiejew, S. Marsh, and J. B. Wang

Department of Physics, The University of Western Australia, Perth WA 6009, Australia

Find this paper interesting or want to discuss? Scite or leave a comment on SciRate.

Abstract

This paper proposes a highly efficient quantum algorithm for portfolio optimisation targeted at near-term noisy intermediate-scale quantum computers. Recent work by Hodson et al. (2019) explored potential application of hybrid quantum-classical algorithms to the problem of financial portfolio rebalancing. In particular, they deal with the portfolio optimisation problem using the Quantum Approximate Optimisation Algorithm and the Quantum Alternating Operator Ansatz. In this paper, we demonstrate substantially better performance using a newly developed Quantum Walk Optimisation Algorithm in finding high-quality solutions to the portfolio optimisation problem.

► BibTeX data

► References

[1] P. W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM J. Sci. Comput., 26 (5): 1484–1509, 1997. 10.1137/​s0097539795293172.
https:/​/​doi.org/​10.1137/​s0097539795293172

[2] M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, Cambridge, 2010. 10.1017/​CBO9780511976667.
https:/​/​doi.org/​10.1017/​CBO9780511976667

[3] J. Preskill. Quantum computing in the NISQ era and beyond. Quantum, 2: 79, 2018. 10.22331/​q-2018-08-06-79.
https:/​/​doi.org/​10.22331/​q-2018-08-06-79

[4] P. Rebentrost and S. Lloyd. Quantum computational finance: quantum algorithm for portfolio optimization, 2018. URL https:/​/​arxiv.org/​abs/​1811.03975.
arXiv:1811.03975

[5] P. Rebentrost, B. Gupt, and T. R. Bromley. Quantum computational finance: Monte Carlo pricing of financial derivatives. Phys. Rev. A, 98: 022321, 2018. 10.1103/​PhysRevA.98.022321.
https:/​/​doi.org/​10.1103/​PhysRevA.98.022321

[6] R. Orús, S. Mugel, and E. Lizaso. Quantum computing for finance: Overview and prospects. Rev. Phys., 4: 100028, 2019. 10.1016/​j.revip.2019.100028.
https:/​/​doi.org/​10.1016/​j.revip.2019.100028

[7] S. Woerner and D. J. Egger. Quantum risk analysis. npj Quantum Inf., 5 (1), 2019. 10.1038/​s41534-019-0130-6.
https:/​/​doi.org/​10.1038/​s41534-019-0130-6

[8] M. Hodson, B. Ruck, H. Ong, D. Garvin, and S. Dulman. Portfolio rebalancing experiments using the Quantum Alternating Operator Ansatz, 2019. URL https:/​/​arxiv.org/​abs/​1911.05296.
arXiv:1911.05296

[9] H. Markowitz. Portfolio selection. J. Finance, 7 (1): 77–91, 1952. 10.1111/​j.1540-6261.1952.tb01525.x.
https:/​/​doi.org/​10.1111/​j.1540-6261.1952.tb01525.x

[10] A. Palczewski. LP algorithms for portfolio optimization: The PortfolioOptim package. R J., 10: 308–327, 2018. 10.32614/​RJ-2018-028.
https:/​/​doi.org/​10.32614/​RJ-2018-028

[11] R. Mansini and M. G. Speranza. Heuristic algorithms for the portfolio selection problem with minimum transaction lots. Eur. J. Oper. Res., 114 (2): 219–233, 1999. 10.1016/​S0377-2217(98)00252-5.
https:/​/​doi.org/​10.1016/​S0377-2217(98)00252-5

[12] T. F. Coleman, Y. Li, and J. Henniger. Minimizing tracking error while restricting the number of assets. J. Risk, 8: 33, 2006. 10.21314/​JOR.2006.134.
https:/​/​doi.org/​10.21314/​JOR.2006.134

[13] J. Cook, S. Eidenbenz, and A. Bärtschi. The Quantum Alternating Operator Ansatz on max-k vertex cover, 2019. URL https:/​/​arxiv.org/​abs/​1910.13483. 10.1109/​QCE49297.2020.00021.
https:/​/​doi.org/​10.1109/​QCE49297.2020.00021
arXiv:1910.13483

[14] E. Farhi and A. W. Harrow. Quantum supremacy through the Quantum Approximate Optimization Algorithm, 2016. URL https:/​/​arxiv.org/​abs/​1602.07674.
arXiv:1602.07674

[15] S. Marsh and J. B. Wang. Combinatorial optimization via highly efficient quantum walks. Phys. Rev. Research, 2: 023302, 2020. 10.1103/​PhysRevResearch.2.023302.
https:/​/​doi.org/​10.1103/​PhysRevResearch.2.023302

[16] M. C. Steinbach. Markowitz revisited: Mean-variance models in financial portfolio analysis. SIAM Rev., 43 (1): 31–85, 2001. 10.1137/​S0036144500376650.
https:/​/​doi.org/​10.1137/​S0036144500376650

[17] K. P. Anagnostopoulos and G. Mamanis. The mean–variance cardinality constrained portfolio optimization problem: An experimental evaluation of five multiobjective evolutionary algorithms. Expert Syst. Appl., 38 (11): 14208–14217, 2011. 10.1016/​j.eswa.2011.04.233.
https:/​/​doi.org/​10.1016/​j.eswa.2011.04.233

[18] M. Bióna. Handbook of enumerative combinatorics. CRC Press, Boca Raton, 2015. 10.1201/​b18255.
https:/​/​doi.org/​10.1201/​b18255

[19] S. Hadfield, Z. Wang, B. O’Gorman, E. Rieffel, D. Venturelli, and R. Biswas. From the Quantum Approximate Optimization Algorithm to a Quantum Alternating Operator Ansatz. Algorithms, 12 (2): 34, 2019. 10.3390/​a12020034.
https:/​/​doi.org/​10.3390/​a12020034

[20] E. Farhi and S. Gutmann. Quantum computation and decision trees. Phys. Rev. A, 58: 915–928, 1998. 10.1103/​PhysRevA.58.915.
https:/​/​doi.org/​10.1103/​PhysRevA.58.915

[21] K. Manouchehri and J. B. Wang. Physical implementation of quantum walks. Springer, Heidelberg, 2014. 10.1007/​978-3-642-36014-5.
https:/​/​doi.org/​10.1007/​978-3-642-36014-5

[22] X. Qiang, T. Loke, A. Montanaro, K. Aungskunsiri, X. Zhou, J. L. O’Brien, J. B. Wang, and J. C. F. Matthews. Efficient quantum walk on a quantum processor. Nat. Commun., 7 (1): 11511, 2016. 10.1038/​ncomms11511.
https:/​/​doi.org/​10.1038/​ncomms11511

[23] A. Mahasinghe and J. B. Wang. Efficient quantum circuits for Toeplitz and Hankel matrices. J. Phys. A, 49 (27): 275301, 2016. 10.1088/​1751-8113/​49/​27/​275301.
https:/​/​doi.org/​10.1088/​1751-8113/​49/​27/​275301

[24] S. S. Zhou, T. Loke, J. A. Izaac, and J. B. Wang. Quantum Fourier transform in computational basis. Quantum Inf. Process., 16 (3): 82, 2017. 10.1007/​s11128-017-1515-0.
https:/​/​doi.org/​10.1007/​s11128-017-1515-0

[25] S. S. Zhou and J. B. Wang. Efficient quantum circuits for dense circulant and circulant-like operators. R. Soc. Open Sci., 4 (5, May): 160906, 12, 2017. 10.1098/​rsos.160906.
https:/​/​doi.org/​10.1098/​rsos.160906

[26] T. Loke and J. B. Wang. Efficient quantum circuits for Szegedy quantum walks. Ann. Phys., 382: 64–84, 2017a. 10.1016/​j.aop.2017.04.006.
https:/​/​doi.org/​10.1016/​j.aop.2017.04.006

[27] T. Loke and J. B. Wang. Efficient quantum circuits for continuous-time quantum walks on composite graphs. J. Phys. A, 50 (5): 055303, 2017b. 10.1088/​1751-8121/​aa53a9.
https:/​/​doi.org/​10.1088/​1751-8121/​aa53a9

[28] X. Qiang, X. Zhou, J. Wang, C. M. Wilkes, T. Loke, S. O’Gara, L. Kling, G. D. Marshall, R. Santagati, T. C. Ralph, J. B. Wang, J. L. O’Brien, M. G. Thompson, and J. C. F. Matthews. Large-scale silicon quantum photonics implementing arbitrary two-qubit processing. Nat. Photonics, 12 (9): 534–539, 2018. 10.1038/​s41566-018-0236-y.
https:/​/​doi.org/​10.1038/​s41566-018-0236-y

[29] C.-H. Yu, F. Gao, C. Liu, D. Huynh, M. Reynolds, and J. Wang. Quantum algorithm for visual tracking. Phys. Rev. A, 99: 022301, 2019. 10.1103/​PhysRevA.99.022301.
https:/​/​doi.org/​10.1103/​PhysRevA.99.022301

[30] R. Cleve and J. Watrous. Fast parallel circuits for the quantum Fourier transform. In Proceedings of SFCS 41, pages 526–536, 2000. 10.1109/​SFCS.2000.892140.
https:/​/​doi.org/​10.1109/​SFCS.2000.892140

[31] G. R. Ahokas. Improved algorithms for approximate quantum Fourier transforms and sparse Hamiltonian simulations. Master’s thesis, University of Calgary, 2004. URL https:/​/​dx.doi.org/​10.11575/​PRISM/​22839.
https:/​/​doi.org/​10.11575/​PRISM/​22839

[32] E. Matwiejew. QuOp_MPI: Parallel distributed memory simulation of Quantum Approximate Optimization Algorithms, 2020. URL https:/​/​doi.org/​10.5281/​zenodo.3681801.
https:/​/​doi.org/​10.5281/​zenodo.3681801

[33] E. Matwiejew and J. B. Wang. QSW_MPI: A framework for parallel simulation of quantum stochastic walks. Comput. Phys. Commun., 260: 107724, 2021. 10.1016/​j.cpc.2020.107724.
https:/​/​doi.org/​10.1016/​j.cpc.2020.107724

[34] W. McKinney. Data Structures for Statistical Computing in Python. In Proceedings of the 9th Python in Science Conference, pages 56–61, 2010. 10.25080/​Majora-92bf1922-00a.
https:/​/​doi.org/​10.25080/​Majora-92bf1922-00a

[35] L. Han and M. Neumann. Effect of dimensionality on the Nelder–Mead simplex method. Optim. Methods Softw., 21 (1): 1–16, 2006. 10.1080/​10556780512331318290.
https:/​/​doi.org/​10.1080/​10556780512331318290

[36] C. Zalka. Grover’s quantum searching algorithm is optimal. Phys. Rev. A, 60: 2746–2751, 1999. 10.1103/​PhysRevA.60.2746.
https:/​/​doi.org/​10.1103/​PhysRevA.60.2746

[37] A. M. Childs and J. Goldstone. Spatial search by quantum walk. Phys. Rev. A, 70: 022314, 2004. 10.1103/​PhysRevA.70.022314.
https:/​/​doi.org/​10.1103/​PhysRevA.70.022314

[38] J. Roland and N. J. Cerf. Quantum-circuit model of Hamiltonian search algorithms. Phys. Rev. A, 68: 062311, 2003. 10.1103/​PhysRevA.68.062311.
https:/​/​doi.org/​10.1103/​PhysRevA.68.062311

[39] D. L. Applegate, R. E. Bixby, V. Chvatal, and W. J. Cook. The Traveling Salesman Problem: A Computational Study. Princeton University Press, USA, 2007. 10.1515/​9781400841103.
https:/​/​doi.org/​10.1515/​9781400841103

Cited by

Could not fetch Crossref cited-by data during last attempt 2021-07-28 10:24:54: Could not fetch cited-by data for 10.22331/q-2021-07-28-513 from Crossref. This is normal if the DOI was registered recently. On SAO/NASA ADS no data on citing works was found (last attempt 2021-07-28 10:24:55).

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.
Click here to access.

Source: https://quantum-journal.org/papers/q-2021-07-28-513/

Continue Reading
AR/VR5 days ago

Review: Winds & Leaves

AR/VR5 days ago

nDreams Opens Studio Orbital Focusing on Live Service Games for VR

Esports5 days ago

Pokémon Sword and Shield’s Same Double Beat online competition announced for August 13

AI5 days ago

How to Build a Powerful Shopify Chatbot

Energy5 days ago

Save money, stay cool as heat wave hits the Carolinas

Blockchain5 days ago

RUNE Technical Analysis: Look Out for the Second and Third Resistance Levels of $5.29 and $5.75

Blockchain4 days ago

Happy birthday Ethereum!

Gaming5 days ago

Resident Evil Village and Monster Hunter Rise Drive Record Q1 Profits for Capcom

Energy5 days ago

The Shaw Group Partners with Clough in the U.S. to Deliver Pipe Fabrication for Gulf Coast Petrochemical Project

Cyber Security3 days ago

Android Banking Trojan Relies on Screen Recording and Keylogging Instead of HTML

AR/VR5 days ago

Carrier Command 2 VR August Launch Date Confirmed

Cyber Security3 days ago

How to Sell Cybersecurity

Blockchain5 days ago

Cashing Out Buterin’s $1B SHIB Donation Isn’t Easy, Says COVID-Crypto Fund’s Creator

Esports3 days ago

Tribes of Midgard Berserker: How to Unlock

Investing4 days ago

How do you use top stock signals as a beginner?

Energy3 days ago

CEMIG Geracão e Transmissão S.A. Announces Early Tender Date Results of its Cash Tender Offer for its 9.250% Senior Notes due 2024

Esports3 days ago

Tribes of Midgard Berserker: How to Unlock

Energy5 days ago

Fermentation Chemicals Market Procurement Intelligence Report with COVID-19 Impact Analysis | SpendEdge

CNBC5 days ago

Rocket Lab launches US Space Force satellite after its failed mission in May

Gaming5 days ago

Resident Evil Village and Monster Hunter Rise Drive Record Q1 Profits for Capcom

Trending