LeanDojo: Theorem Proving in Lean Using LLMs
leandojo.org170 pointsby aseg53 comments
- Off‑the‑shelf LLMs can both generate code and recall domain knowledge. The “knowledge retrieval” stage may hallucinate, but—because the knowledge is expressed as code—we can execute it and validate the result against a custom evaluation function.
- Gradient descent is not an option for discrete code; a zeroth‑order optimizer—specifically evolutionary search—is required.
- During evolution we bias toward (1) _succinct_ programs and (2) _novel_ programs. Succinctness is approximated by program length; novelty is encouraged via a MAP‑Elites–style “novelty bias,” yielding a three‑dimensional Pareto frontier whose axes are _performance, simplicity,_ and _novelty_ (see e.g. OE‑Dreamer: (https://claireaoi.github.io/OE-Dreamer/).
Location: Pasadena, CA
Remote: No/Yes
Willing to relocate: Yes
Technologies: Computer Vision, Code generation, Program Synthesis, Coq, Lean, PyTorch, Julia
Résumé/CV: https://atharvas.net/cv/
Email: [email protected]
Some basics: The major challenge in flying gliders is the inherent stochasticity in the weather system. Think of it as a contextual bandit problem with high variance w.r.t local weather (i.e. Even the best planning cannot help if the weather doesn't comply). We have some observability due to forecasting tools (skysight.io) and any policy must have affordances for pilot skill and a margin of safety. A good pilot (or 'policy') starts with multiple plans, quickly modifies to plans to suit the environment, and can seamlessly switch between plans. The primary "reward signals" are duration of flight, distance covered, and (in competitions) hitting certain waypoints.
Previous WR's for longest flight were mostly in the Andes or Alps. You want to be in a mountain range to utilize either the [ridge lift](https://en.wikipedia.org/wiki/Orographic_lift) of a mountain face or [mountain wave](https://en.wikipedia.org/wiki/Lee_wave), ideally in a polar region during the summer to maximize the daylight hours so you can fly under VFR for longer.
However, while the Sierra Nevada's have great mountain wave and ridge lift, the number of daylight hours is not ``competitive''. Their main innovation was in acclimatizing themselves with using night vision goggles for long duration in a glider. There's an article on this [here](https://magazine.weglide.org/gliding-at-night-breaking-the-3...) which describes the acclimatizing flights and the 3k km flight in great detail. It doesn't get official recognition because the FAI requires the flight to be done in daylight, but still an extremely cool flight!