22 Commits

Author	SHA1	Message	Date
Simon	0ba6927a1e	fix: Set verbosity to False on MCTS tests	2024-11-02 19:17:36 +00:00
Simon	bafb5944b2	Merge branch 'main' into add-mcts-agent	2024-11-02 10:38:15 +00:00
Simon	2e377d2a7e	feat: Tactic feedback per state	2024-11-02 10:35:57 +00:00
Leni Aniva	6d9cb9cd3d	Merge branch 'main' into feat/search	2024-10-30 18:30:46 -07:00
Simon	b89f3a19bf	feat: add state specific tactic feedback	2024-10-30 17:08:44 -07:00
Leni Aniva	de93309393	feat: Add linage info to tree search	2024-10-28 10:34:09 -07:00
Simon	c6358056fe	Add mcts agent	2024-10-21 17:36:20 +01:00
Leni Aniva	35f093821d	chore: Update upstream to fix bugs	2024-10-08 17:59:48 -07:00
Leni Aniva	76eb57b22e	fix: Prompt Lean code extraction	2024-10-07 18:58:35 -07:00
Leni Aniva	0d773e256b	feat: Remove the goal count restriction on initial state	2024-10-05 00:58:27 -07:00
Leni Aniva	cd5cf51970	feat: Improve feedback and provide default options	2024-10-05 00:58:27 -07:00
Leni Aniva	01ec8fa22a	refactor: Update the experiment repo Lean version, use new load_sorry API	2024-09-13 18:18:53 -07:00
Leni Aniva	8abe689a0a	fix: Make search work with automatic mode	2024-09-13 17:54:11 -07:00
Leni Aniva	20b19c8e6c	feat: Handle max trials per goal and theorem formatting	2024-06-05 15:20:36 -07:00
Leni Aniva	7b9829e3d2	feat: Add limit on goal tactic trials	2024-06-05 14:36:51 -07:00
Leni Aniva	ce633fecda	feat: Add ablation testing	2024-06-05 14:19:18 -07:00
Leni Aniva	4e678c7b97	feat: Use aesop to solve for goals	2024-06-05 14:02:12 -07:00
Chuyue Sun	9c672562a9	update	2024-06-05 13:58:32 -07:00
Chuyue Sun	6d60651ed1	add informal hints for search agent	2024-06-05 11:39:08 -07:00
Chuyue Sun	0bb8d55de2	search llm passed	2024-06-04 19:59:59 -07:00
Leni Aniva	860b3c2134	chore: Code cleanup	2024-06-03 23:57:48 -07:00
Leni Aniva	07597c0ce6	feat: Add tree search	2024-06-03 21:52:43 -07:00