Chris Pollett > Students >
Rohan
    ( Print View)

    [Bio]

    [Blog]

    [C297 Proposal]

    [LoRA: Low Rank Adaptation of Matrix (.pdf)]

    [DoRA: Weight Decomposed Low-rank Adaptation (.pdf)]

    [Deliverable 1 - MATH Dataset]

    [Deliverable 1 - GSM8k Dataset]

    [Deliverable_2 - Integrate mathics tool]

    [Deliverable_3 - Prove Infinite primes theorm using LEAN]

    [Chain-of-Thought Prompting in LLMs(.pdf)]

    [LeanDojo - Theorem Proving with RAG(.pdf)]

    [Deliverable 4 - Solving word problems using LEAN and Mathics]

    [CS297 Report(.pdf)]

    [C298 Proposal]

Project Blog

Apr 14, 2025

Meeting Summary

  • Discussed challenges scaling up GPUs

To-Do List

  • Give lambda cloud's H100 GPUs a try

Apr 08, 2025

Meeting Summary

  • Discussed the various MoE implementations that were tried, but in vain

To-Do List

  • Make use of bigger GPUs for implmenting MoE models

Mar 25, 2025

Meeting Summary

  • Displayed the results of X E Nat -> S(X) E Nat. Sn(0) E Nat. with n=10 for LEAN expert
  • Presented a slide deck on MoE

To-Do List

  • Start implementing MoE architecture on math expert models

Mar 18, 2025

Meeting Summary

  • Reviewed experiment results of the proof : X E Nat -> S(X) E Nat. Sn(0) E Nat.

To-Do List

  • As the experiment results were not promising for n=99, experiment with n=10. Also experiment with LEAN expert model
  • Start reading on MoEs

Mar 11, 2025

Meeting Summary

  • Reviewed the results of GRPO finetuned llama-3.2-8b model and its imporovements over base model
  • Discussed few scenarios to test the context length capacity of the model

To-Do List

  • Experiment with the finetuned model by trying to prove : X E Nat -> S(X) E Nat. Sn(0) E Nat.

Mar 4, 2025

Meeting Summary

  • Presented slides deck on Deepseek prover v1
  • Discussed challenges in GRPO finetuning of llama-3.1-8b model

To-Do List

  • Explore GRPO finetuning on smaller models like llama-3.2-3b model

Feb 25, 2025

Meeting Summary

  • Displayed evaluation results of SFT fintetuned model

To-Do List

  • continue GRPO finetuning on math model and start working on LEAN model

Feb 18, 2025

Meeting Summary

  • Discussed evaluations to be run on finetuned model

To-Do List

  • Prepare a report of evaluations run on finetuned model

Feb 11, 2025

Meeting Summary

  • Presented deepseek's r1 paper

To-Do List

  • Update GPT-3 with llama 3.1 in the project proposal as GPT-3 is not open sourced

Nov 26, 2024

Meeting Summary

  • Presented a working example of theorm proving using LEANDojo without repository boilerplate

To-Do List

  • Create a dummy dataset of mathematics word problems that can be proved using Mathics and LEAN tools

Nov 19, 2024

Meeting Summary

  • Presented LEANDojo paper to professor
  • Professor explained propositional logic and formal logic

To-Do List

  • Find a workaround for theorm proving with LEANDojo without having a repository setup

Nov 12, 2024

Meeting Summary

  • Presented [Wei2022] to professor and we discussed more on Chain of through prompting

To-Do List

  • Explore LEAN Dojo to enable interaction of LLMs with LEAN
  • Prepare a slide deck on LEANDojo

Nov 5, 2024

Meeting Summary

  • Demonstrated infinite primes thoerm using LEAN

To-Do List

  • Prepare slide deck on [Wei2022]
  • Formulate a LEAN proof using LLM

Oct 29, 2024

Meeting Summary

  • Presented Tutorials I prepared on LEAN and HOL

To-Do List

  • Continue exploring LEAN and prove infinite primes theorm

Oct 22, 2024

Meeting Summary

  • Presented Deliverable 2: Integrating Mathics tool with LLM to compute sin^2(x)
  • Professor and I discussed various alternatives to LEAN: HOL, ISABELLE, Coq

To-Do List

  • Create a tutorial on LEAN to prove adding 1 x times = adding x
  • Contrast LEAN with HOL

Oct 15, 2024

Meeting Summary

  • Presented Deliverable 1: Results of fine-tuning on MATH and GSM8k dataset
  • Discussed on how an agentic architecture works, specifically ReAct

To-Do List

  • Add slides on how to use mathics
  • Present Deliverable 2

Oct 8, 2024

Meeting Summary

  • Took a closer look at how weight decomposition works in LoRA

To-Do List

  • Prepare slides on Mathics
  • Read up how a RAG architecture works and its working.
  • Measure the impact of fine-tuning by comparing vanilla GPT-2 and its finetuned version

Oct 1, 2024

Meeting Summary

  • Presented a slides deck on DoRA.
  • Finalized the expected results' format for Deliverable 1

To-Do List

Sep 24, 2024

Meeting Summary

  • Presented the research paper on LoRA.
  • Deeper look into working of LoRA.
  • Talked about variants of LoRA (DoRA).

To-Do List

  • Complete deliverable 1 and furnish the results.
  • Explore alternatives to LoRA (e.g., DoRA) and prepare slides.

Sep 16, 2024

Meeting Summary

  • Presented a paper that describes MATH dataset
  • Discussed approaches on how to fine-tune models. LoRA looked promising

To-Do List

  • Make slides on the Math dataset research paper.
  • Make slides on fine-tuning using LoRA.
  • Start fine-tuning on GPT-2.
  • Update deliverable 1 to submit fine-tuned results.

Sep 10, 2024

To-Do List

  • Update my blog, proposal, and bio on the website.