---
title: "Decomposing the Enigma — paper by Zhao et al. (2023)"
description: "The authors argue that the format and arrangement of the few-shot demonstrations are an… 6.6 points. 52 references, cited by 27 papers here."
authors: ["Xueliang Zhao", "Wenda Li", "Lingpeng Kong"]
year: 2023
venue: "arXiv:2305.16366"
source: "https://arxiv.org/abs/2305.16366"
doi: "10.48550/arxiv.2305.16366"
arxiv: "2305.16366"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2023](https://md.research.elamur.ai/free/en/papers/2023/page/12/) / Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

# Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

**Authors:** [Xueliang Zhao](https://md.research.elamur.ai/free/en/authors/xueliang-zhao/), [Wenda Li](https://md.research.elamur.ai/free/en/authors/wenda-li/) and [Lingpeng Kong](https://md.research.elamur.ai/free/en/authors/lingpeng-kong/) · **Year:** 2023 · **Venue:** arXiv:2305.16366 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2305.16366) · [PDF](https://arxiv.org/pdf/2305.16366v1) · [DOI 10.48550/arxiv.2305.16366](https://doi.org/10.48550/arxiv.2305.16366) · [arXiv 2305.16366](https://arxiv.org/abs/2305.16366) · [OpenAlex](https://openalex.org/W4378711566)

**Citations:** 2 citations (OpenAlex, 2026-10-14) · [27](https://md.research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Formal theorem proving with LLMs usually runs as two prompted steps. The model first drafts an informal proof of a statement, then converts it into a formal sketch that an off-the-shelf tool such as Sledgehammer verifies. The authors argue that the format and arrangement of the few-shot demonstrations are an underused lever, and they propose a two-part framework.

First, the informal proofs inside demonstrations are rewritten as chains of subgoals, an idea taken from subgoal learning in RL and robotics. These chains are refined iteratively through ChatGPT and a proof assistant, so that every subgoal can be reached both from the statement and from the completed proof.

Second, picking and ordering demonstrations for sketch generation is framed as finding a path through a graph of examples. A discrete diffusion model with a GNN denoiser solves this, trained on example arrangements that previously led to successful proofs.

On miniF2F, the approach sets a new best pass rate and needs far fewer LLM calls. This shows that prompt structure strongly affects formal reasoning.

## Key points
- Subgoal-based proofs alone raise miniF2F accuracy from 38.9% to 44.3%. Adding diffusion-based demonstration organization brings it to 45.5%, which is 6.6 points absolute and 17.0% relative above the prior state of the art.
- Diffusion-based organization matches the earlier best result (reported as 38.5%) with 20 LLM calls instead of 100, roughly a 5× gain in sampling efficiency.
- Demonstrations are long: a 3072-token context fits only about 4.79 examples on average, so selecting and ordering them is critical. Selection and ordering are handled jointly and can be inferred in parallel.
- Acknowledged limitations: ChatGPT-driven refinement may add noise, the diffusion model is computationally heavy, and evaluation covers only miniF2F.
- Code is released at github.com/HKUNLP/subgoal-theorem-prover.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 287 works · 125,174 citations
- [University of Hong Kong](https://md.research.elamur.ai/free/en/universities/university-of-hong-kong/) — University, Pok Fu Lam, China · 127 works · 13,824 citations

Also on the byline: [Lingnan University](https://ror.org/0563pg902).

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Xueliang Zhao, Wenda Li and Lingpeng Kong. 2023. Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving. arXiv:2305.16366.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{zhao2023decomposing,
  title = {{Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving}},
  author = {Xueliang Zhao, Wenda Li and Lingpeng Kong},
  year = {2023},
  doi = {10.48550/arxiv.2305.16366},
  eprint = {2305.16366},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2305.16366}
}
```

- [← previous Click: Controllable Text Generation with Sequence Likelihood Contrastive Learning](https://md.research.elamur.ai/free/en/papers/zheng-2023-click-controllable-text-generation-sequence/)
- [next → Detecting Suicidality in Arabic Tweets Using Machine Learning and Deep Learning Techniques](https://md.research.elamur.ai/free/en/papers/abdulsalam-2023-detecting-suicidality-arabic-tweets-using/)
- [↑ back to papers of 2023](https://md.research.elamur.ai/free/en/papers/2023/page/12/)

## References

52 references, 25 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Sweta Agrawal, Chunting Zhou, Mike Lewis, Luke Zettlemoyer, and Marjan Ghazvininejad. [In-context examples selection for machine translation](https://md.research.elamur.ai/free/en/papers/agrawal-2023-context-examples-selection-machine-translation/). arXiv preprint arXiv:2212.02437, 2022.
2. Jacob Austin, Daniel D Johnson, Jonathan Ho, Daniel Tarlow, and Rianne van den Berg. [Structured denoising diffusion models in discrete state-spaces](https://md.research.elamur.ai/free/en/papers/austin-2021-structured-denoising-diffusion-models-discrete/). Advances in Neural Information Processing Systems, 34:17981–17993, 2021.
3. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. [Proofnet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433, 2023.
4. Xavier Bresson and Thomas Laurent. An experimental study of neural networks for variable graphs. 2018. [find](https://scholar.google.com/scholar?q=Xavier+Bresson+and+Thomas+Laurent%2E+An+experimental+study+of+neural+networks+for+variable+graphs%2E+2018%2E)
5. Davide Castelvecchi et al. Mathematicians welcome computer-assisted proof in ‘grand unification’theory. Nature, 595(7865):18–19, 2021. [find](https://scholar.google.com/scholar?q=Davide+Castelvecchi+et+al%2E+Mathematicians+welcome+computer%2Dassisted+proof+in+%E2%80%98grand+unification%E2%80%99theory%2E+Nature%2C+595%287865%29%3A18%E2%80%9319%2C+2021%2E)
6. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer, 2015. [find](https://scholar.google.com/scholar?q=Leonardo+de+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+Van+Doorn%2C+and+Jakob+von+Raumer%2E+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction%2DCADE%2D25%3A+25th+International+Conference+on+Au)
7. Ben Eysenbach, Russ R Salakhutdinov, and Sergey Levine. Search on the replay buffer: Bridging planning and reinforcement learning. Advances in Neural Information Processing Systems, 32, 2019. [find](https://scholar.google.com/scholar?q=Ben+Eysenbach%2C+Russ+R+Salakhutdinov%2C+and+Sergey+Levine%2E+Search+on+the+replay+buffer%3A+Bridging+planning+and+reinforcement+learning%2E+Advances+in+Neural+Information+Processing+Systems%2C+32%2C+2019%2E)
8. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. [Baldur: Whole-proof generation and repair with large language models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/). arXiv preprint arXiv:2303.04910, 2023.
9. Ronan Fruit, Matteo Pirotta, Alessandro Lazaric, and Emma Brunskill. Regret minimization in mdps with options without prior knowledge. Advances in Neural Information Processing Systems, 30, 2017. [find](https://scholar.google.com/scholar?q=Ronan+Fruit%2C+Matteo+Pirotta%2C+Alessandro+Lazaric%2C+and+Emma+Brunskill%2E+Regret+minimization+in+mdps+with+options+without+prior+knowledge%2E+Advances+in+Neural+Information+Processing+Systems%2C+30%2C+2017%2E)
10. Alexandros Graikos, Nikolay Malkin, Nebojsa Jojic, and Dimitris Samaras. Diffusion models as plug-and-play priors. arXiv preprint arXiv:2206.09012, 2022. — [arXiv:2206.09012](https://arxiv.org/abs/2206.09012) [find](https://scholar.google.com/scholar?q=Alexandros+Graikos%2C+Nikolay+Malkin%2C+Nebojsa+Jojic%2C+and+Dimitris+Samaras%2E+Diffusion+models+as+plug%2Dand%2Dplay+priors%2E+arXiv+preprint+arXiv%3A2206%2E09012%2C+2022%2E+%E2%80%94+%5BarXiv%3A2206%2E09012%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F220)
11. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. [Proof artifact co-training for theorem proving with language models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). arXiv preprint arXiv:2102.06203, 2021.
12. Kristian Hartikainen, Xinyang Geng, Tuomas Haarnoja, and Sergey Levine. Dynamical distance learning for semi-supervised and unsupervised skill discovery. arXiv preprint arXiv:1907.08225, 2019. — [arXiv:1907.08225](https://arxiv.org/abs/1907.08225) [find](https://scholar.google.com/scholar?q=Kristian+Hartikainen%2C+Xinyang+Geng%2C+Tuomas+Haarnoja%2C+and+Sergey+Levine%2E+Dynamical+distance+learning+for+semi%2Dsupervised+and+unsupervised+skill+discovery%2E+arXiv+preprint+arXiv%3A1907%2E08225%2C+2019%2E+%E2%80%94+%5BarXi)
13. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. [Measuring mathematical problem solving with the math dataset](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/). arXiv preprint arXiv:2103.03874, 2021.
14. Sergey Ioffe and Christian Szegedy. Batch normalization: Accelerating deep network training by reducing internal covariate shift. In International conference on machine learning, pages 448–456. pmlr, 2015. [find](https://scholar.google.com/scholar?q=Sergey+Ioffe+and+Christian+Szegedy%2E+Batch+normalization%3A+Accelerating+deep+network+training+by+reducing+internal+covariate+shift%2E+In+International+conference+on+machine+learning%2C+pages+448%E2%80%93456%2E+pmlr%2C+)
15. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). arXiv preprint arXiv:2210.12283, 2022.
16. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. [Thor: Wielding hammers to integrate language models and automated theorem provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). Advances in Neural Information Processing Systems, 35:8360–8373, 2022.
17. Yuu Jinnai, David Abel, David Hershkowitz, Michael Littman, and George Konidaris. Finding options that minimize planning time. In International Conference on Machine Learning, pages 3120–3129. PMLR, 2019. [find](https://scholar.google.com/scholar?q=Yuu+Jinnai%2C+David+Abel%2C+David+Hershkowitz%2C+Michael+Littman%2C+and+George+Konidaris%2E+Finding+options+that+minimize+planning+time%2E+In+International+Conference+on+Machine+Learning%2C+pages+3120%E2%80%933129%2E+PMLR%2C+2)
18. Yuu Jinnai, Jee Won Park, David Abel, and George Konidaris. Discovering options for exploration by minimizing cover time. In International Conference on Machine Learning, pages 3130–3139. PMLR, 2019. [find](https://scholar.google.com/scholar?q=Yuu+Jinnai%2C+Jee+Won+Park%2C+David+Abel%2C+and+George+Konidaris%2E+Discovering+options+for+exploration+by+minimizing+cover+time%2E+In+International+Conference+on+Machine+Learning%2C+pages+3130%E2%80%933139%2E+PMLR%2C+2019%2E)
19. Tushar Khot, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. [Decomposed prompting: A modular approach for solving complex tasks](https://md.research.elamur.ai/free/en/papers/khot-2022-decomposed-prompting-modular-approach/). arXiv preprint arXiv:2210.02406, 2022.
20. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–… [find](https://scholar.google.com/scholar?q=Gerwin+Klein%2C+Kevin+Elphinstone%2C+Gernot+Heiser%2C+June+Andronick%2C+David+Cock%2C+Philip+Derrin%2C+Dhammika+Elkaduwe%2C+Kai+Engelhardt%2C+Rafal+Kolanski%2C+Michael+Norrish%2C+et+al%2E+sel4%3A+Formal+verification+of+an+os)
21. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
22. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. [Solving quantitative reasoning problems with language models](https://md.research.elamur.ai/free/en/papers/lewkowycz-2022-solving-quantitative-reasoning-problems-language/). arXiv preprint arXiv:2206.14858, 2022.
23. Alexander C Li, Mihir Prabhudesai, Shivam Duggal, Ellis Brown, and Deepak Pathak. Your diffusion model is secretly a zero-shot classifier. arXiv preprint arXiv:2303.16203, 2023. — [arXiv:2303.16203](https://arxiv.org/abs/2303.16203) [find](https://scholar.google.com/scholar?q=Alexander+C+Li%2C+Mihir+Prabhudesai%2C+Shivam+Duggal%2C+Ellis+Brown%2C+and+Deepak+Pathak%2E+Your+diffusion+model+is+secretly+a+zero%2Dshot+classifier%2E+arXiv+preprint+arXiv%3A2303%2E16203%2C+2023%2E+%E2%80%94+%5BarXiv%3A2303%2E16203%5D%28h)
24. Yunfei Li, Tian Gao, Jiaqi Yang, Huazhe Xu, and Yi Wu. Phasic self-imitative reduction for sparse-reward goal-conditioned reinforcement learning. In International Conference on Machine Learning, pages 12765–12781. PMLR, 2022. [find](https://scholar.google.com/scholar?q=Yunfei+Li%2C+Tian+Gao%2C+Jiaqi+Yang%2C+Huazhe+Xu%2C+and+Yi+Wu%2E+Phasic+self%2Dimitative+reduction+for+sparse%2Dreward+goal%2Dconditioned+reinforcement+learning%2E+In+International+Conference+on+Machine+Learning%2C+pages)
25. Jiachang Liu, Dinghan Shen, Yizhe Zhang, Bill Dolan, Lawrence Carin, and Weizhu Chen. [What makes good in-context examples for gpt-3?](https://md.research.elamur.ai/free/en/papers/liu-2022-what-makes-good-context-examples/) arXiv preprint arXiv:2101.06804, 2021.
26. Yao Lu, Max Bartolo, Alastair Moore, Sebastian Riedel, and Pontus Stenetorp. [Fantastically ordered prompts and where to find them: Overcoming few-shot prompt order sensitivity](https://md.research.elamur.ai/free/en/papers/lu-2022-fantastically-ordered-prompts-where-find/). arXiv preprint arXiv:2104.08786, 2021.
27. Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. [Magnushammer: A transformer-based approach to premise selection](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/). arXiv preprint arXiv:2303.04488, 2023.
28. Lorenzo Moro, Amarildo Likmeta, Enrico Prati, Marcello Restelli, et al. Goal-directed planning via hindsight experience replay. In International Conference on Learning Representations, pages 1–16, 2022. [find](https://scholar.google.com/scholar?q=Lorenzo+Moro%2C+Amarildo+Likmeta%2C+Enrico+Prati%2C+Marcello+Restelli%2C+et+al%2E+Goal%2Ddirected+planning+via+hindsight+experience+replay%2E+In+International+Conference+on+Learning+Representations%2C+pages+1%E2%80%9316%2C+202)
29. OpenAI. [GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv e-prints, art. arXiv:2303.08774, March 2023. doi: 10.48550/arXiv.2303.08774.
30. OpenAI OpenAI, Matthias Plappert, Raul Sampedro, Tao Xu, Ilge Akkaya, Vineet Kosaraju, Peter Welinder, Ruben D’Sa, Arthur Petron, Henrique P d O Pinto, et al. Asymmetric self-play for automatic goal discovery in robotic manipulation. arXiv preprint arXiv:2101.04882, 2021. [find](https://scholar.google.com/scholar?q=OpenAI+OpenAI%2C+Matthias+Plappert%2C+Raul+Sampedro%2C+Tao+Xu%2C+Ilge+Akkaya%2C+Vineet+Kosaraju%2C+Peter+Welinder%2C+Ruben+D%E2%80%99Sa%2C+Arthur+Petron%2C+Henrique+P+d+O+Pinto%2C+et+al%2E+Asymmetric+self%2Dplay+for+automatic+goal+d)
31. Giambattista Parascandolo, Lars Buesing, Josh Merel, Leonard Hasenclever, John Aslanides, Jessica B Hamrick, Nicolas Heess, Alexander Neitz, and Theophane Weber. Divide-and-conquer monte carlo tree search for goal-directed planning. arXiv preprint arXiv:2004.11410, 2020. — [arXiv:2004.11410](https://arxiv.org/abs/2004.11410) [find](https://scholar.google.com/scholar?q=Giambattista+Parascandolo%2C+Lars+Buesing%2C+Josh+Merel%2C+Leonard+Hasenclever%2C+John+Aslanides%2C+Jessica+B+Hamrick%2C+Nicolas+Heess%2C+Alexander+Neitz%2C+and+Theophane+Weber%2E+Divide%2Dand%2Dconquer+monte+carlo+tree+se)
32. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulson%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2C+1994%2E)
33. Lawrence C Paulson. [Isabelle: The next 700 theorem provers](https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/). arXiv preprint cs/9301106, 2000.
34. Lawrence C Paulsson and Jasmin C Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC, volume 2, 2012. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulsson+and+Jasmin+C+Blanchette%2E+Three+years+of+experience+with+sledgehammer%2C+a+practical+link+between+automatic+and+interactive+theorem+provers%2E+In+Proceedings+of+the+8th+International+Wo)
35. Silviu Pitis, Harris Chan, Stephen Zhao, Bradly Stadie, and Jimmy Ba. Maximum entropy gain exploration for long horizon multi-goal reinforcement learning. In International Conference on Machine Learning, pages 7750–7761. PMLR, 2020. [find](https://scholar.google.com/scholar?q=Silviu+Pitis%2C+Harris+Chan%2C+Stephen+Zhao%2C+Bradly+Stadie%2C+and+Jimmy+Ba%2E+Maximum+entropy+gain+exploration+for+long+horizon+multi%2Dgoal+reinforcement+learning%2E+In+International+Conference+on+Machine+Learni)
36. Stanislas Polu and Ilya Sutskever. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv preprint arXiv:2009.03393, 2020.
37. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). arXiv preprint arXiv:2202.01344, 2022.
38. Ohad Rubin, Jonathan Herzig, and Jonathan Berant. [Learning to retrieve prompts for in-context learning](https://md.research.elamur.ai/free/en/papers/rubin-2021-learning-retrieve-prompts-context-learning/). arXiv preprint arXiv:2112.08633, 2021.
39. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484–489, 2016. [find](https://scholar.google.com/scholar?q=David+Silver%2C+Aja+Huang%2C+Chris+J+Maddison%2C+Arthur+Guez%2C+Laurent+Sifre%2C+George+Van+Den+Driessche%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Veda+Panneershelvam%2C+Marc+Lanctot%2C+et+al%2E+Mastering+the+game+)
40. Taylor Sorensen, Joshua Robinson, Christopher Michael Rytting, Alexander Glenn Shaw, Kyle Jeffrey Rogers, Alexia Pauline Delorey, Mahmoud Khalil, Nancy Fulda, and David Wingate. [An information-theoretic approach to prompt engineering without ground truth labels](https://md.research.elamur.ai/free/en/papers/sorensen-2022-information-theoretic-approach-prompt-engineering/). arXiv preprint arXiv:2203.11364, 2022…
41. Hongjin Su, Jungo Kasai, Chen Henry Wu, Weijia Shi, Tianlu Wang, Jiayi Xin, Rui Zhang, Mari Ostendorf, Luke Zettlemoyer, Noah A Smith, et al. Selective annotation makes language models better few-shot learners. arXiv preprint arXiv:2209.01975, 2022. [find](https://scholar.google.com/scholar?q=Hongjin+Su%2C+Jungo+Kasai%2C+Chen+Henry+Wu%2C+Weijia+Shi%2C+Tianlu+Wang%2C+Jiayi+Xin%2C+Rui+Zhang%2C+Mari+Ostendorf%2C+Luke+Zettlemoyer%2C+Noah+A+Smith%2C+et+al%2E+Selective+annotation+makes+language+models+better+few%2Dshot)
42. Zhiqing Sun and Yiming Yang. Difusco: Graph-based diffusion solvers for combinatorial optimization. arXiv preprint arXiv:2302.08224, 2023. — [arXiv:2302.08224](https://arxiv.org/abs/2302.08224) [find](https://scholar.google.com/scholar?q=Zhiqing+Sun+and+Yiming+Yang%2E+Difusco%3A+Graph%2Dbased+diffusion+solvers+for+combinatorial+optimization%2E+arXiv+preprint+arXiv%3A2302%2E08224%2C+2023%2E+%E2%80%94+%5BarXiv%3A2302%2E08224%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2302%2E08224%29)
43. OpenAI Team. Chatgpt: Optimizing language models for dialogue, 2022. [find](https://scholar.google.com/scholar?q=OpenAI+Team%2E+Chatgpt%3A+Optimizing+language+models+for+dialogue%2C+2022%2E)
44. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. [Attention is all you need](https://md.research.elamur.ai/free/en/papers/vaswani-2017-attention-all-need/). Advances in neural information processing systems, 30, 2017.
45. Zheng Wen, Doina Precup, Morteza Ibrahimi, Andre Barreto, Benjamin Van Roy, and Satinder Singh. On efficiency in hierarchical reinforcement learning. Advances in Neural Information Processing Systems, 33:6708–6718, 2020. [find](https://scholar.google.com/scholar?q=Zheng+Wen%2C+Doina+Precup%2C+Morteza+Ibrahimi%2C+Andre+Barreto%2C+Benjamin+Van+Roy%2C+and+Satinder+Singh%2E+On+efficiency+in+hierarchical+reinforcement+learning%2E+Advances+in+Neural+Information+Processing+Systems%2C)
46. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in Neural Information Processing Systems, 35:32353–32368, 2022.
47. Zhiyong Wu, Yaoxiang Wang, Jiacheng Ye, and Lingpeng Kong. Self-adaptive in-context learning. arXiv preprint arXiv:2212.[10375, 2022](https://md.research.elamur.ai/free/en/papers/wu-2022-self-adaptive-context-learning-information/).
48. Yuexiang Zhai, Christina Baek, Zhengyuan Zhou, Jiantao Jiao, and Yi Ma. Computational benefits of intermediate rewards for goal-reaching policy learning. Journal of Artificial Intelligence Research, 73:847–896, 2022. [find](https://scholar.google.com/scholar?q=Yuexiang+Zhai%2C+Christina+Baek%2C+Zhengyuan+Zhou%2C+Jiantao+Jiao%2C+and+Yi+Ma%2E+Computational+benefits+of+intermediate+rewards+for+goal%2Dreaching+policy+learning%2E+Journal+of+Artificial+Intelligence+Research%2C+7)
49. Tianjun Zhang, Benjamin Eysenbach, Ruslan Salakhutdinov, Sergey Levine, and Joseph E Gonzalez. C-planning: An automatic curriculum for learning goal-reaching tasks. arXiv preprint arXiv:2110.12080, 2021. [find](https://scholar.google.com/scholar?q=Tianjun+Zhang%2C+Benjamin+Eysenbach%2C+Ruslan+Salakhutdinov%2C+Sergey+Levine%2C+and+Joseph+E+Gonzalez%2E+C%2Dplanning%3A+An+automatic+curriculum+for+learning+goal%2Dreaching+tasks%2E+arXiv+preprint+arXiv%3A2110%2E12080%2C+20)
50. Yunzhi Zhang, Pieter Abbeel, and Lerrel Pinto. Automatic curriculum learning through value disagreement. Advances in Neural Information Processing Systems, 33:7648–7659, 2020. [find](https://scholar.google.com/scholar?q=Yunzhi+Zhang%2C+Pieter+Abbeel%2C+and+Lerrel+Pinto%2E+Automatic+curriculum+learning+through+value+disagreement%2E+Advances+in+Neural+Information+Processing+Systems%2C+33%3A7648%E2%80%937659%2C+2020%2E)
51. Zihao Zhao, Eric Wallace, Shi Feng, Dan Klein, and Sameer Singh. [Calibrate before use: Improving few-shot performance of language models](https://md.research.elamur.ai/free/en/papers/zhao-2021-calibrate-before-use-improving-few/). In International Conference on Machine Learning, pages 12697–12706. PMLR, 2021.
52. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [Minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv preprint arXiv:2109.00110, 2021.

*Updated 3 November 2026*