Skip to content

Implemented Optimization with additive scoring and RL for selection policy learning - #1

Merged
jpbrooks merged 3 commits into
jpbrooks:masterfrom
samuelpaulgyamfi:sam-rl-update
Feb 26, 2026
Merged

Implemented Optimization with additive scoring and RL for selection policy learning #1
jpbrooks merged 3 commits into
jpbrooks:masterfrom
samuelpaulgyamfi:sam-rl-update

Conversation

@samuelpaulgyamfi

Copy link
Copy Markdown

This PR introduces an optimization framework using additive scoring, along with a reinforcement learning–based policy for expression selection.

Key updates:

Implemented additive scoring combining error, complexity, and constraint penalties.
Integrated an RL-driven selection mechanism to guide pool updates.
Refined reward structure to improve stability and reduce premature swap plateaus.
These changes aim to improve learning efficiency and expression quality within the conjecturing framework.

Comment thread c/expressions.c Outdated
{"output", required_argument, NULL, 'o'},
{"property", no_argument, NULL, 'p'},
{"theory", no_argument, NULL, 't'}
{"theory", no_argument, NULL, 't'},

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't we need to remove the trailing comma for the code to compile?

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No i found out that it compile with or without the commas.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And plus the original code has it so I figured I'll just keep them.

Comment thread c/expressions.c Outdated
heuristicPostProcessing();
/* If RL episodic loop ran, postProcessing already executed inside the loop */
if (!(doConjecturing && selectedHeuristic == RL_HEURISTIC)) {
if (heuristicPostProcessing) heuristicPostProcessing();

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the selectedHeuristic is not RL_HEURISTIC, we still need to call heuristicPostProcessing. Please test the code to ensure that the Dalmatian heuristic works as before.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The non-RL branch already calls heuristicPostProcessing() immediately after conjecture(), so the additional conditional block at the end was redundant and could result in duplicate execution.
I removed that extra block and confirmed that the Dalmatian heuristic behaves exactly as before (single initialization, single conjecture pass, single post-processing call).

@jpbrooks jpbrooks left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are in addition to a few individual comments.

Comment thread c/expressions.c Outdated
} samConjecture;

/* Globals with defaults (you can wire CLI options later) */
static int sam_top_k = 9; /* --sam-top-k <int> */

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can these be removed now that they are command line options?

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes it can, those are just default like the complexity_limit.

Comment thread c/expressions.c Outdated
double avgTightness = (n_feasible ? sumTight / (double)n_feasible : 0.0);

double complexityPenalty = (double)(targetUnary + 2 * targetBinary);
double score = avgViolation + sam_beta * avgTightness + sam_lambda * complexityPenalty;

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are we using alpha for the violation weight?

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes I have included it now

Comment thread c/expressions.c
#endif

/*------------ Tunables -----------------------------------------------------*/
static double rl_alpha_viol = 1.0;

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should these be command-line options?

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes all parameters are command line options with the defaults as fall back incase they are not provided.

Comment thread c/expressions.c

/* ------------------------------- Utils ---------------------------------- */
static inline int is_finite(double x){ return isfinite(x); }
static inline double clamp(double x, double lo, double hi){

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please add a comment for each function with a brief description of what it does?

samuelpaulgyamfi and others added 2 commits February 25, 2026 22:39
Removed unnecessary blank lines to improve code readability.

@jpbrooks jpbrooks left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Adding SAM and RL

@jpbrooks
jpbrooks merged commit 4327610 into jpbrooks:master Feb 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants