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.

Technical Philosophy

Languages: Python (Advanced), Lean (Research). Stack: PyTorch, Google Cloud (Vertex AI), AWS, Docker.
Libraries: Pydantic, Polars, Apache Beam, MLFlow.