Building production-grade AI agents and researching mathematical reasoning in LLMs.
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.