Research Focus (M.Sc.)

My current academic work at Unicamp focuses on the intersection of formal logic and Large Language Models. I am investigating how to improve step-by-step mathematical reasoning without relying solely on large-scale supervised fine-tuning. Mathematical Reasoning for LLMs: Developing methods to fine-tune Gemma models using GRPO (Group Relative Policy Optimization). Formal Verification as Reward: Utilizing Lean (theorem prover) as a robust reward function to guide the model's reasoning trace, ensuring logical consistency rather than just final-answer correctness.