請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/88117完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 陳偉松 | zh_TW |
| dc.contributor.advisor | Tony Tan | en |
| dc.contributor.author | 呂侑承 | zh_TW |
| dc.contributor.author | Yu-Cheng Lu | en |
| dc.date.accessioned | 2023-08-08T16:22:30Z | - |
| dc.date.available | 2023-11-09 | - |
| dc.date.copyright | 2023-08-08 | - |
| dc.date.issued | 2023 | - |
| dc.date.submitted | 2023-07-14 | - |
| dc.identifier.citation | [1] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and the hardness of approximation problems. Journal of the ACM (JACM), 45(3):501–555, 1998.
[2] S. Arora and S. Safra. Probabilistic checking of proofs: A new characterization of NP. Journal of the ACM (JACM), 45(1):70–122, 1998. [3] L. Babai. Trading group theory for randomness. In Proceedings of the seventeenth annual ACM symposium on Theory of computing, pages 421–429, 1985. [4] L. Babai and L. Fortnow. Arithmetization: A new method in structural complexity theory. computational complexity, 1:41–66, 1991. [5] L. Babai, L. Fortnow, and C. Lund. Non-deterministic exponential time has two-prover interactive protocols. Computational complexity, 1:3–40, 1991. [6] L. Babai and S. Moran. Arthur-merlin games: a randomized proof system, and a hierarchy of complexity classes. Journal of Computer and System Sciences, 36(2):254–276, 1988. [7] S. Badrinarayanan, Y. T. Kalai, D. Khurana, A. Sahai, and D. Wichs. Succinct delegation for low-space non-deterministic computation. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, pages 709–721, 2018. [8] V. Balabanov and J. Jiang. Reducing satisfiability and reachability to DQBF. Austin, TX, USA, Sep, 2015. [9] M. Ben-Or, S. Goldwasser, J. Kilian, and A. Wigderson. Multi-prover interactive proofs: How to remove intractability assumptions. In Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, STOC ’88, page 113–131, New York, NY, USA, 1988. Association for Computing Machinery. [10] E. Ben-Sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza. SNARKs for C: Verifying program executions succinctly and in zero knowledge. In Advances in Cryptology–CRYPTO 2013: 33rd Annual Cryptology Conference, Santa Barbara, CA, USA, August 18-22, 2013. Proceedings, Part II, pages 90–108. Springer, 2013. [11] E. Ben-Sasson, A. Chiesa, M. Riabzev, N. Spooner, M. Virza, and N. P. Ward. Aurora: Transparent succinct arguments for r1cs. In Advances in Cryptology–EUROCRYPT 2019: 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Darmstadt, Germany, May 19–23, 2019, Proceedings, Part I 38, pages 103–128. Springer, 2019. [12] R. Bloem, R. Könighofer, and M. Seidl. SAT-based synthesis methods for safety specs. In Verification, Model Checking, and Abstract Interpretation: 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings 15, pages 1–20. Springer, 2014 [13] B. Bünz, J. Bootle, D. Boneh, A. Poelstra, P. Wuille, and G. Maxwell. Bulletproofs: Short proofs for confidential transactions and more. In 2018 IEEE symposium on security and privacy (SP), pages 315–334. IEEE, 2018. [14] K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis. Distributed synthesis for LTL fragments. In 2013 Formal Methods in Computer-Aided Design, pages 18–25. IEEE, 2013. [15] F.-H. Chen, S.-C. Huang, Y.-C. Lu, and T. Tan. Reducing NEXP-complete problems to DQBF. In CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN–FMCAD 2022, page 199, 2022. [16] A. Chiesa, Y. Hu, M. Maller, P. Mishra, N. Vesely, and N. Ward. Marlin: Preprocessing zksnarks with universal and updatable srs. In Advances in Cryptology-EUROCRYPT 2020: 39th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Zagreb, Croatia, May 10–14, 2020, Proceedings, Part I 39, pages 738–768. Springer, 2020. [17] S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151–158, 1971. [18] G. Cormode, M. Mitzenmacher, and J. Thaler. Practical verified computation with streaming interactive proofs. In Proceedings of the 3rd Innovations in Theoretical Computer Science Conference, pages 90–112, 2012. [19] U. Feige, S. Goldwasser, L. Lovász, S. Safra, and M. Szegedy. Interactive proofs and the hardness of approximating cliques. Journal of the ACM (JACM), 43(2):268–292, 1996. [20] L. Fortnow, J. Rompel, and M. Sipser. On the power of multi-prover interactive protocols. Theoretical Computer Science, 134(2):545–557, 1994. [21] R. Gennaro, C. Gentry, and B. Parno. Non-interactive verifiable computing: Outsourcing computation to untrusted workers. In Advances in Cryptology–CRYPTO 2010: 30th Annual Cryptology Conference, Santa Barbara, CA, USA, August 15-19, 2010. Proceedings 30, pages 465–482. Springer, 2010. [22] I. Giacomelli, J. Madsen, and C. Orlandi. Zkboo: Faster zero-knowledge for boolean circuits. In USENIX Security Symposium, volume 16, 2016. [23] K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker. Equivalence checking of partial designs using dependency quantified boolean formulae. In 2013 IEEE 31st International Conference on Computer Design (ICCD), pages 396–403. IEEE, 2013. [24] O. Goldreich. Short locally testable codes and proofs. Studies in Complexity and Cryptography. Miscellanea on the Interplay between Randomness and Computation: In Collaboration with Lidor Avigad, Mihir Bellare, Zvika Brakerski, Shafi Goldwasser, Shai Halevi, Tali Kaufman, Leonid Levin, Noam Nisan, Dana Ron, Madhu Sudan, Luca Trevisan, Salil Vadhan, Avi Wigderson, David Zuckerman, pages 333–372, 2011. [25] O. Goldreich and M. Sudan. Locally testable codes and PCPs of almost-linear length. Journal of the ACM (JACM), 53(4):558–655, 2006. [26] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proof-systems. In Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing, STOC ’85, page 291–304. Association for Computing Machinery, New York, NY, USA, 1985. [27] J. Holmgren and R. Rothblum. Delegating computations with (almost) minimal time and space overhead. In 2018 IEEE 59th Annual Symposium on Foundations of Computer Science (FOCS), pages 124–135. IEEE, 2018. [28] J.-H. R. Jiang. Quantifier elimination via functional composition. In Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26-July 2, 2009. Proceedings 21, pages 383–397. Springer, 2009. [29] A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai. Robust boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 21(12):1377–1394, 2002. [30] L. A. Levin. Universal sequential search problems. Problemy peredachi informatsii, 9(3):115–116, 1973. [31] C. Lund, L. Fortnow, H. Karloff, and N. Nisan. Algebraic methods for interactive proof systems. Journal of the ACM (JACM), 39(4):859–868, 1992. [32] S. Micali. Cs proofs. In Proceedings 35th Annual Symposium on Foundations of Computer Science, pages 436–453. IEEE, 1994. [33] C. Papadimitriou and M. Yannakakis. Optimization, approximation, and complexity classes. In Proceedings of the twentieth annual ACM symposium on Theory of computing, pages 229–234, 1988. [34] C. H. Papadimitriou and M. Yannakakis. A note on succinct representations of graphs. Inf. Control., 71:181–185, 1986. [35] B. Parno, J. Howell, C. Gentry, and M. Raykova. Pinocchio: Nearly practical verifiable computation. Communications of the ACM, 59(2):103–112, 2016. [36] G. L. Peterson and J. H. Reif. Multiple-person alternation. In 20th Annual Symposium on Foundations of Computer Science (sfcs 1979), pages 348–363. IEEE, 1979. [37] E. B. Sasson, A. Chiesa, C. Garman, M. Green, I. Miers, E. Tromer, and M. Virza. Zerocash: Decentralized anonymous payments from bitcoin. In 2014 IEEE symposium on security and privacy, pages 459–474. IEEE, 2014. [38] C. Scholl and B. Becker. Checking equivalence for partial implementations. In Proceedings of the 38th Annual Design Automation Conference, pages 238–243, 2001. [39] A. Schönhage. Schnelle multiplikation grosser zahlen. Computing, 7:281–292, 1971. [40] S. Setty, B. Braun, V. Vu, A. J. Blumberg, B. Parno, and M. Walfish. Resolving the conflict between generality and plausibility in verified computation. In Proceedings of the 8th ACM European Conference on Computer Systems, pages 71–84, 2013. [41] S. T. Setty, R. McPherson, A. J. Blumberg, and M. Walfish. Making argument systems for outsourced computation practical (sometimes). In NDSS, volume 1, page 17, 2012. [42] A. Shamir. IP=PSPACE. Journal of the ACM (JACM), 39(4):869–877, 1992. [43] Y. Tauman Kalai, R. Raz, and R. D. Rothblum. Delegation for bounded space. In Proceedings of the forty-fifth annual ACM symposium on Theory of computing, pages 565–574, 2013. [44] L. Trevisan. Inapproximability of combinatorial optimization problems. Paradigms of Combinatorial Optimization: Problems and New Approaches, pages 381–434, 2014. [45] M. Walfish and A. J. Blumberg. Verifying computations without reexecuting them. Communications of the ACM, 58(2):74–84, 2015. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/88117 | - |
| dc.description.abstract | 隨機可驗證系統 (probabilistic checkable proof) 是一種證明系統，讓驗證證明的驗證者只需隨機查看部份證明內容即可高機率確認其正確性。事實上，許多被認為困難的問題包含非確定性多項式時間計算 (non-deterministic polynomial-time computation) 和 非 確 定 性 指 數 時 間 計 算 (non-deterministic exponential-time computation) 都能使用此種證明系統，並且驗證者只須隨機查看證明中常數個位元的內容即可高機率確認證明的正確性。此結果被稱為隨機可驗證系統理論 (the PCP theorem)，在資訊理論和現實世界中都有許多應用。其中一個應用領域為可驗證計算 (verifiable computation)，此領域的研究者嘗試建立一套機制，使得人們能快速驗證其他人是否正確執行某項電腦計算。過去十年來，研究者提出各種不同的方法來實現可驗證計算，不過他們的方法和討論都集中於（非）確定性多項式時間。近幾年，研究者開始探討超過多項式時間或空間的（非）確定性計算。本論文將嘗試使用隨機可驗證系統建構非確定性指數時間計算的可驗證計算。準確來說，本論文先利用存在性二階布林運算式 (existential second-order boolean formula) 來精簡地表示任何非確定性指數時間計算的計算表，再為存在性二階布林運算式設計一隨機可驗證系統。另外，本論文也證明估計存在性二階布林運算式滿足與否為非確定性指數時間完備問題。 | zh_TW |
| dc.description.abstract | Probabilistic checkable proof (PCP) is a type of proof format that could be verified with high probability by only looking at a small portion of the proof. It turns out that problems in NP and even in NEXP have PCP proofs that could be verified in polynomial time by only looking at a constant number of bits in the proof. The result is known as the PCP theorem and has both practical and theoretical significance. One of its practical applications lies in the field of verifiable computation, which aims to provide a scheme for one to efficiently verify if a computation is carried out correctly by others. There are many different approaches in the field while most of the work are dedicated to deterministic/non-deterministic computation in polynomial time. Recently, some researchers investigate the possibility of constructing schemes for deterministic/non-deterministic computation beyond polynomial time and space. In the thesis, we try to construct a scheme for non-deterministic computation in exponential time based on PCP proofs. Specifically, we succinctly encode any non-deterministic exponential computation tableau by a logic known as ∃SOQBF and construct a PCP proofs for ∃SOQBF. In addition, we also show that it is NEXP-hard to approximate the satisfiability of ∃SOQBF within any constant factor. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2023-08-08T16:22:30Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2023-08-08T16:22:30Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 口試委員審定書 i
致謝 iii Acknowledgements v 摘要 vii Abstract ix Contents xi List of Tables xiii Chapter 1 Introduction 1 Chapter 2 Preliminary 5 2.1 Existential second-order quantified boolean formula 5 2.2 Polynomials with function symbols 8 2.3 Probabilistically checkable proof 9 Chapter 3 Encoding of NEXP computation by ∃SOQBF 11 Chapter 4 The PCP proof for SAT(∃SOQBF) 17 4.1 Arithmetization of interpretations 18 4.2 Arithmetization of ∃SOQBF formulas 19 4.3 The PCP proof for SAT(∃SOQBF) 21 Chapter 5 The PCP verifier for SAT(∃SOQBF) 25 5.1 The multilinearity test 26 5.2 The sum-check protocol 29 5.3 The PCP verifier for SAT(∃SOQBF) 32 Chapter 6 Conclusion 37 References 41 | - |
| dc.language.iso | en | - |
| dc.subject | 存在性二階布林運算式 | zh_TW |
| dc.subject | 非確定性指數時間計算 | zh_TW |
| dc.subject | 隨機可驗證系統 | zh_TW |
| dc.subject | 可驗證計算 | zh_TW |
| dc.subject | Verifiable computation | en |
| dc.subject | Probabilistic checkable proof | en |
| dc.subject | Non-deterministic exponential-time computation | en |
| dc.subject | Existential second-order quantified boolean formula | en |
| dc.title | 存在性二階布林運算式的隨機可驗證系統和其不可估計性 | zh_TW |
| dc.title | A PCP Protocol for Existential SOQBF and the Inapproximability Result | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 111-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 鐘楷閔;江介宏 | zh_TW |
| dc.contributor.oralexamcommittee | Kai-Min Chung;Jie-Hong Roland Jiang | en |
| dc.subject.keyword | 隨機可驗證系統,可驗證計算,非確定性指數時間計算,存在性二階布林運算式, | zh_TW |
| dc.subject.keyword | Probabilistic checkable proof,Verifiable computation,Non-deterministic exponential-time computation,Existential second-order quantified boolean formula, | en |
| dc.relation.page | 47 | - |
| dc.identifier.doi | 10.6342/NTU202300853 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2023-07-14 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 資訊工程學系 | - |
| 顯示於系所單位： | 資訊工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-111-2.pdf | 581.7 kB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。