-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Kaiyu Yang
committed
Jun 25, 2023
1 parent
07fd499
commit 722b370
Showing
1 changed file
with
114 additions
and
33 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -49,11 +49,13 @@ | |
href="https://cdn.jsdelivr.net/gh/jpswalsh/academicons@1/css/academicons.min.css"> | ||
<link rel="stylesheet" href="./static/css/index.css"> | ||
|
||
<!-- | ||
<script src="https://ajax.googleapis.com/ajax/libs/jquery/3.5.1/jquery.min.js"></script> | ||
<script defer src="./static/js/fontawesome.all.min.js"></script> | ||
<script src="./static/js/bulma-carousel.min.js"></script> | ||
<script src="./static/js/bulma-slider.min.js"></script> | ||
<script src="./static/js/index.js"></script> | ||
--> | ||
</head> | ||
<body> | ||
|
||
|
@@ -304,6 +306,7 @@ <h2 class="title is-3">Abstract</h2> | |
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">Theorem Proving in Lean</span></h2> | ||
<img src="images/LeanDojo.jpg" class="interpolation-image" | ||
alt="" style="display: block; margin-left: auto; margin-right: auto"/> | ||
<br> | ||
|
@@ -314,6 +317,91 @@ <h2 class="title is-3">Abstract</h2> | |
</div> | ||
</section> | ||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">Data Extraction</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">LeanDojo Benchmark</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">Interacting with Lean</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">ReProver: Retrieval-Augmented Theorem Prover</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">Experiments</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">Discovering New Proofs</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
<div class="rows"> | ||
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">ChatGPT for Theorem Proving</span></h2> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
</section> | ||
|
||
<!-- | ||
<section class="section"> | ||
<div class="container is-max-widescreen"> | ||
|
@@ -639,16 +727,6 @@ <h3 class="title is-4"><span | |
<h2 class="title is-3"><span | ||
class="dvima">Conclusion</span></h2> | ||
<p style="font-size: 125%"> | ||
In this work, we introduce a novel <i>multimodal</i> prompting formulation that converts diverse | ||
robot manipulation tasks into a uniform sequence modeling problem. We instantiate this | ||
formulation in VIMA-Bench, a diverse benchmark with multimodal tasks and systematic evaluation | ||
protocols for generalization. We propose VIMA, a conceptually simple transformer-based agent | ||
capable of solving tasks such as visual goal reaching, one-shot video imitation, and novel | ||
concept grounding with a single model. Through comprehensive experiments, we show that VIMA | ||
exhibits strong model scalability and zero-shot generalization. Therefore, we recommend our | ||
agent design as a solid starting point for future work. | ||
</p> | ||
</div> | ||
</div> | ||
|
@@ -664,52 +742,55 @@ <h2 class="title is-3"><span | |
<div class="rows is-centered "> | ||
<div class="row is-full-width"> | ||
<h2 class="title is-3"><span class="dvima">Team</span></h2> | ||
<ul> | ||
<li><a href="https://yangky11.github.io/" target="_blank" style="border-bottom: none"> | ||
<table style="border-collapse: collapse; border: none;"> | ||
<tr style="border: none;"> | ||
<td style="border: none;"><a href="https://yangky11.github.io/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Kaiyu.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Kaiyu Yang <a class="fas fa-envelope" href="mailto:[email protected]" style="font-size: 75%"></a></h4> | ||
</a></li> | ||
<li><a href="https://aidanswope.com/about" target="_blank" style="border-bottom: none"> | ||
</a></td> | ||
|
||
<td style="border: none;"><a href="https://aidanswope.com/about" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Aidan.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Aidan Swope</h4> | ||
</a></li> | ||
<li><a href="https://minimario.github.io/" target="_blank" style="border-bottom: none"> | ||
</a></td> | ||
|
||
<td style="border: none;"><a href="https://minimario.github.io/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Alex.jpg" alt="" style="width:100%;"/></span> | ||
<h4>Alex Gu</h4> | ||
</a></li> | ||
</a></td> | ||
|
||
<li><a href="(https://www.linkedin.com/in/rchalamala" target="_blank" style="border-bottom: none"> | ||
<td style="border: none;"><a href="(https://www.linkedin.com/in/rchalamala" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Rahul.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Rahul Chalamala</h4> | ||
</a></li> | ||
</a></td> | ||
|
||
<li><a href="https://www.linkedin.com/in/peiyang-song-3279b3251/" target="_blank" style="border-bottom: none"> | ||
<td style="border: none;"><a href="https://www.linkedin.com/in/peiyang-song-3279b3251/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Peiyang.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Peiyang Song</h4> | ||
</a></li> | ||
|
||
<li><a href="https://billysx.github.io/" target="_blank" style="border-bottom: none"> | ||
</a></td> | ||
</tr> | ||
<tr style="border: none;"> | ||
<td style="border: none;"><a href="https://billysx.github.io/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Shixing.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Shixing Yu</h4> | ||
</a></li> | ||
</a></td> | ||
|
||
<li><a href="https://www.linkedin.com/in/saad-godil-9728353/" target="_blank" style="border-bottom: none"> | ||
<td style="border: none;"><a href="https://www.linkedin.com/in/saad-godil-9728353/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Saad.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Saad Godil</h4> | ||
</a></li> | ||
</a></td> | ||
|
||
<li><a href="https://www.linkedin.com/in/ryan-prenger-18797ba1/" target="_blank" style="border-bottom: none"> | ||
<td style="border: none;"><a href="https://www.linkedin.com/in/ryan-prenger-18797ba1/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Ryan.jpg" alt="" style="width:100%;" /></span> | ||
<h4>Ryan Prenger</h4> | ||
</a></li> | ||
</a></td> | ||
|
||
<li><a href="http://tensorlab.cms.caltech.edu/users/anima/" target="_blank" style="border-bottom: none"> | ||
<td style="border: none;"><a href="http://tensorlab.cms.caltech.edu/users/anima/" target="_blank" style="border-bottom: none"> | ||
<span class="image"><img src="images/Anima.png" alt="" style="width:100%;" /></span> | ||
<h4>Anima Anandkuma</h4> | ||
</a></li> | ||
</ul> | ||
</a></td> | ||
</tr> | ||
</table> | ||
</div> | ||
</div> | ||
|
||
|