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

Brando Miranda

brando
muhtasham's profile picture Mr-aio's profile picture roseking's profile picture
·
https://brando90.github.io/brandomiranda/

AI & ML interests

soccer, music, dance, reading

Recent Activity

updated a dataset 1 day ago
zipfit/leandojo_benchmark_4_random_splits
published a dataset 1 day ago
zipfit/leandojo_benchmark_4_random_splits
updated a dataset 1 day ago
zipfit/leandojo_benchmark_4_corpus
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

brando's activity

New activity in EleutherAI/proof-pile-2 1 day ago

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

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

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

Kind request for a prompt for autoformalization evaluations.
#1 opened 14 days ago by
brando
New activity in Putnam-AXIOM/putnam-axiom-dataset 15 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 15 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 3 months ago

Still errors with GAIR loading dataset

2
#3 opened 4 months ago by
brando
commented 2 papers 3 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 4 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