Hugging Face's logo
Brando Miranda's picture
50 4 78

Brando Miranda

brando
muhtasham's profile picture simenyg's profile picture 21world's profile picture
·
https://brando90.github.io/brandomiranda/

AI & ML interests

soccer, music, dance, reading

Recent Activity

updated a model 1 day ago
brando/tfa_output_2025_m02_d07_t07h_43m_33s
published a model 1 day ago
brando/tfa_output_2025_m02_d07_t07h_43m_33s
liked a model 1 day ago
meta-llama/Llama-3.2-3B
View all activity

Organizations

Stanford AI's profile picture Stanford CRFM's profile picture Data Centric Machine Learning for Math's profile picture MAFmaticians's profile picture byndscl's profile picture The Ultimate Data Centric Alliance's profile picture The AI Alliance for Solving Mathematics for All (AI4M)'s profile picture Putnam-AXIOM & Variations's profile picture ZIP-FIT - Compression-Based Data Selection For Code's profile picture Self-Optimizing Synthetic Data for Verified Code's profile picture

brando's activity

New activity in EleutherAI/proof-pile-2 6 days ago

What version of Lean, is it Lean4?
#15 opened 6 days ago by
brando
New activity in hoskinson-center/proofnet 12 days ago

lean 4 proof net version?
#2 opened 12 days ago by
brando
New activity in internlm/internlm2-math-plus-1_8b 17 days ago

any chat template?
#2 opened 17 days ago by
brando
New activity in hoskinson-center/proofnet 18 days ago

Kind request for a prompt for autoformalization evaluations.
#1 opened 18 days ago by
brando
New activity in Putnam-AXIOM/putnam-axiom-dataset 20 days ago

~10% of the problem statements may have flaws (according to Claude Sonnet 3.6 and a tiny bit of manual checking)

4
#2 opened 20 days ago by
ArthurConmy
New activity in UDACA/Code-Mixed-Dataset 3 months ago

issue getting data set

1
#1 opened 3 months ago by
brando
New activity in Putnam-AXIOM/putnam-axiom-dataset 3 months ago

[bot] Conversion to Parquet
#1 opened 3 months ago by
parquet-converter
New activity in TIGER-Lab/WebInstructSub 3 months ago

does this data have PoT also? I can't find examples

1
#3 opened 3 months ago by
brando
New activity in GAIR/MathPile 4 months ago

Still errors with GAIR loading dataset

2
#3 opened 5 months ago by
brando
commented 2 papers 4 months ago
New activity in internlm/Lean-Workbook 4 months ago

what exact model did the autoformalization?

1
#2 opened 4 months ago by
brando
New activity in GAIR/MathPile 5 months ago

Issue with TypeError in GAIR/MathPile Dataset Loading

5
#2 opened about 1 year ago by
BaiXue
New activity in deepseek-ai/DeepSeek-Prover-V1.5-SFT 5 months ago

is this model good for autoformalization?
#5 opened 5 months ago by
brando
New activity in internlm/internlm2_5-1_8b 5 months ago

internlm-2.5 1.8B Matm model available?
#3 opened 5 months ago by
brando
New activity in deepseek-ai/deepseek-math-7b-instruct 5 months ago

If I want the model to output something in a specific format, which format do you recommend?
#3 opened 5 months ago by
brando
New activity in Iddah/llama3-8B-informalization 6 months ago

what base model was used? base or instruct?

1
#1 opened 6 months ago by
brando
New activity in deepseek-ai/DeepSeek-Prover-V1.5-RL 6 months ago

demo with vllm?

1
#4 opened 6 months ago by
brando
New activity in internlm/internlm2_5-1_8b 6 months ago

recommended max length?

1
#2 opened 6 months ago by
brando

vllm support?
#1 opened 6 months ago by
brando