PLDI '21論文読み会: Cyclic Program Synthesis

Transcript

1. 
   ୲౰
   ߐޱ
   $ZDMJD
   1SPHSBN
   4ZOUIFTJT 1-%*ಡΈձ!*EFJO
   
2. EFEVDUJWF
   QSPHSBN
   TZOUIFTJT ༩͑ΒΕͨ࢓༷Λຬͨ͢ϓϩάϥϜΛࣗಈͰߏ੒͢ΔλεΫ ਖ਼͕͠͞ূ໌͞Ε͍ͯΔ
3. ݚڀ֓ཁ ࠶ؼతͳิॿؔ਺ΛؚΉIFBQNBOJQVMBUJOH
   QSPHSBNͷࣗಈੜ੒
   w $ZDMJD
   1SPPGͷٕज़ΛϓϩάϥϜ߹੒ʹԠ༻
4. എܠ
5. ϓϩάϥϜͷ࢓༷ 4FQBSBUJPO
   MPHJD
   w ϙΠϯλɺࢀরͳͲΛ൐͏ϓϩάϥϜͷঢ়ଶมԽΛදݱͰ͖Δ࿦ཧ
   w ࠶ؼతͳड़ޠΛ࢖ͬͯɺ༷ʑͳσʔλߏ଄ΛදݱͰ͖Δ
6. طଘݚڀ
   4VT-JD
   4USVDUVSJOH
   UIF
   TZOUIFTJT
   PG
   IFBQNBOJQVMBUJOH
   QSPHSBNT<101-> w 4FQBSBUJPO
   MPHJDΛ࢓༷ʹ$MJLFͳ࠶ؼؔ਺Λੜ੒
   w 4ZOUIFUJD
   4FQBSBUJPO
   -PHJD ͱ͍͏ϓϩάϥϜੜ੒༻ͷਪ࿦ମܥΛ࡞੒ SSL ˎϒϥ΢β্ͰࢼͤΔ 
 ɹIUUQDPNDPNDTBJMNJUFEVDPNDPN4V4-JL
7. طଘݚڀ
   4VT-JD
   ͷݶք ิॿؔ਺෇͖ϓϩάϥϜΛੜ੒Ͱ͖ͳ͍
   
   ྫ
   ҎԼͷੜ੒͸ࣦഊ͢Δ ˎ
   MJTU
   BQQFOEΛߦ͏࠶ؼతͳؔ਺͕ඞཁʹͳΔҝ Ұൠతʹɺิॿؔ਺ͷ࢓༷ΛࣗಈͰݟ͚ͭΔͷ͸೉͍͠໰୊
   ɹূ໌୳ࡧͷ؍఺Ͱ͸ɺؼೲ๏͕ճΔΑ͏ʹద੾ʹิ୊Λੜ੒͢Δ͜ͱʹରԠ
8. ఏҊख๏
9. ఏҊख๏ w DZDMJD
   QSPPGΛ༻͍ͯ ͱ͍͏ਪ࿦ମܥΛߟҊ
   w 4VT-J,ͷ Λ֦ு
   w ্Ͱূ໌Λ୳ࡧ͠ɺϓϩάϥϜΛੜ੒͢Δ
   w ิॿؔ਺෇͖ϓϩάϥϜͷੜ੒͕Մೳʹ SSL↺ SSL SSL↺
10. $ZDMJD
    QSPPG "O
    *OUSPEVDUJPO
    UP
    $ZDMJD
    1SPPGT
    ΑΓ
    IUUQXXXDTVDMBDVLTUB ff +#SPUIFSTUPOTMJEFT 1"3*4@'-P$@@@QBSUQEG
    ॥؀Λڐ͢ূ໌ମܥ
    ূ໌໦ͷ-FBG෦෼ͱผͷOPEF΁ͷzCBDLMJOLz͕࡞ΕΔ w
    ॥؀ͷ࢓ํʹ͸੍໿Λ՝͢
    ɹɹʮ॥؀ͷதͰূ໌͕lਐΜͰ͍ΔzʯΈ͍ͨͳ੍໿ ˎࣗ༝ʹ॥؀Λڐͤ͹ԿͰ΋ূ໌Ͱ͖ͯ͠·͏ w ূ໌୳ࡧͱͷ૬ੑ͕ྑ͍෦෼͕͋Δ
    w PO
    EFNBOEʹؼೲ๏͕ճͤΔ
11. SSL↺ w ͷ֦ு
    w ҎԼͷ߲̐ؔ܎Λಋग़͢Δূ໌ମܥ SSL Γ; 𝒫 ⇝ 𝒬 ∣ c ࣄલ৚݅ ࣄޙ৚݅ ม਺؀ڥ
    ͔ Ͱଋറ ∀ ∃ ϓϩάϥϜ w ྫ
    
    w ߏจৄࡉ
    ࿦จͷ'JHVSF
     ∀r, s, x∃y; {r ↦ x * tree(x, s)} ⇝ {r ↦ y * sll(y, s)} ∣ fl BUUFO S
12. ͷಋग़نଇൈਮ SSL↺ ʹ΋ಉ༷ͳ΋ͷ͋Δ΋ͷ SSL
13. ͷಋग़نଇൈਮ SSL↺ ಠࣗͷ΋ͷ ؔ਺ݺͼग़͠पΓ ͜Ε͸ؔ਺ݺͼग़͠ͷ४උͷͨΊͷSVMFɹ 8SJUFϧʔϧ͸ Λ௚઀ಋ༷͘ʹ͔͠࢖͑ͳ͍ͷͰඞཁ Q ؔ਺ݺͼग़͠
    ࣗମ͕ੜ੒ͷର৅ʹͳ͍ͬͯΔ f(¯ x)
14. USFF'MBUUFOͷಋग़ w   
    fl BUUFOͷ࠶ؼݺͼग़͠ʹରԠ
    w  
    ิॿؔ਺BQQFOE಺ͷ࠶ؼʹରԠ
    w BQQFOE͸ҎԼͷΑ͏ʹൃݟ͞ΕΔ
     ೋͭͷ Λͨ͠ޙ
    B
     Λ͞Βʹల։3FBEͨ͠ޙ
    
    C
     C ͔Β B ΁ͷ$BMM͕ద༻Ͱ͖Δ͜ͱʹؾ෇͘
     D ͷ༷ʹQSPDΛૠೖ͠CBDLMJOLΛ࡞Δ flatten() sll(yl, sl )
15. ؔ਺ݺͼग़͠ͷੜ੒ ީิΛ fi Y͞Ε্ͨͰɺҎԼͷඇܾఆੑ͕͋Δ
    w ୅ೖ
    w ࢒Γύʔτ ͷબ୒
    w TFUVQ෦෼ ͷੜ੒ σ R c1 
    ީิͱͳΔCBDL
    MJOLઌ DPNQBOJPO શͯΛࢼ͢
16. ؔ਺ݺͼग़͠ͷੜ੒ S`
    Y`͸GSFTIͳ ଋറ͞Εͨม਺ ∃ 
    ͷTVCTFU QSFIFBQ͕࢒ͬͯ΋ྑ͍WFSTJPOͷFNQنଇ Ͱผ్ੜ੒໰୊Λղ͘ SSL↺ ྫ
    ࠨਤͷ  ͷ෦෼ͷੜ੒ ͷಋग़͔Β
    FNQنଇͰ࢒ͬͨ෦෼͕
    TFUVQϓϩάϥϜ
    ͕ಘΒΕΔ ∃ σ R c
17. ධՁ
18. ࣮ݧ݁Ռ w ࠶ؼతͳิॿؔ਺෇͖ͷϓϩάϥϜ
    w ࠨਤͷͱҎ֎
    w zDPNQMFY
    UFSNJOBUJPO
    NFUSJDzΛඞཁͱ ͢Δ΋ͷ
    w ͱ
    w ૬ޓ࠶ؼతͳϓϩάϥϜ
    w 
    
    
    
    w ͱ͕૬ޓ࠶ؼʹͳΔͷ͸ਓؒͷ ײ֮ͱ͸ͣΕΔʣ ༷ʑͳlෳࡶͳzϓϩάϥϜͷੜ੒ʹ੒ޭ
19. ϕϯνϚʔΫྫ
    MJTU
    JOQMBDF
    TPSU
20. ϕϯνϚʔΫྫ
    MJTU
    JOQMBDF
    TPSU ༨ஊ
    TPSUͷఆ͕ٛΑ͘෼͔Βͳ͍ ˣͳͲͰ͸μϝͳͷ͔ 5FDIOJDBM
    QBQFSͷ"QQFOEJOH
    $
    ʹҎԼͷهࡌ
21. ϕϯνϚʔΫྫ
    VOJRVF
    MJTU
    JOUFSTFDUJPO ҎԼͷΑ͏ͳTJNQMFͳ࢓༷Ͱ͸ੜ੒ʹࣦഊ͢Δ ҎԼͷΑ͏ͳFMFNؔ਺͕ੜ੒Ͱ͖Ε͹ྑ͍͕ɺ
    ख๏ͷݶքΛ௒͑Δ ͜ͷ࣌఺ͰɺZ͸EFTUSVDUͯ͠ΔͷͰYΛSʹՃ͑ͯྑ͍͔஌Δखஈ͕ͳ͍ ҎԼͷΑ͏ʹ୳ࡧ͸͢Δ͕ɺɺ
22. ϕϯνϚʔΫྫ
    VOJRVF
    MJTU
    JOUFSTFDUJPO ZΛEFTUSVDU͠ͳ͍Α͏QPTU
    DPOEJUJPOʹڧΊΕ͹੒ޭ͢Δ ͕ɺҎԼͷΑ͏ͳzී௨ͷz࣮૷͸ੜ੒͞Εͳ͍ʢͰ͖ͳ͍ʣ ͜͜Ͱิॿؔ਺ͷ࢓༷ͷQSFDPOEJUJPOͷ৚݅Λ؇ΊΔඞཁ͕͋ΓɺఏҊख๏Ͱ͸Ͱ͖ͳ͍ ୅ΘΓʹɺzී௨ͱ͸ఔԕ͍zϓϩάϥϜ͕ੜ੒͞ΕΔ ஶऀୡͰ͢ΒผͷϓϩάϥϜݕূػΛ࢖ͬͯਖ਼͠͞Λ͔֬ΊΔఔ
23. MJNJUBUJPO w ੜ੒Ͱ͖Δิॿؔ਺ʹ੍ݶ͋Γ
    w ৽ͨͳEBUBߏ଄Λ࢖͏΋ͷ΍ɺBDDVNVMBUPSͳͲ௥ՃҾ਺Λ࢖͏Α͏ͳ΋ͷ͸ੜ ੒Ͱ͖ͳ͍
    w ิॿؔ਺ͷ࢓༷Λద੾ʹzҰൠԽzͰ͖ͳ͍ʢJOUFSTFDUͷྫʹ༷͋ͬͨʹʣ
    w ੜ੒ίʔυͷύϑΥʔϚϯε͸อূ͞Εͳ͍
    w MPPQͷαϙʔτ͕ͳ͍
    w ຤ඌ࠶ؼΛੜ੒͢Δ࢓૊ΈΛ࡞Ε͹ྑ͍͕ɺద੾ͳBDDVNVMBUPSΛੜ੒͢Δඞཁ͕ ͋Δͷ͕೉͍͠
24. ·ͱΊ w ࠶ؼతͳิॿؔ਺ΛؚΉIFBQNBOJQVMBUJOH
    QSPHSBNͷࣗಈੜ੒
    w $ZDMJD
    1SPPGͷٕज़ΛϓϩάϥϜ߹੒ʹԠ༻
    w ϓϩάϥϜ߹੒πʔϧʢ$ZQSFTTʣΛ࣮૷
    w ૬ޓ࠶ؼؚΉิॿؔ਺෇͖ϓϩάϥϜͷੜ੒ʹ੒ޭ